Bump to v4.27.0

ZFLean/Basic.lean

@@ -173,11 +173,9 @@ theorem prod_inj {A B C D : ZFSet} (h : A.prod B = C.prod D) (hA : A ≠ ∅) (h
     A = C ∧ B = D := by
   obtain ⟨a, ha⟩ := nonempty_exists_iff.mp hA
   obtain ⟨b, hb⟩ := nonempty_exists_iff.mp hB
-
   obtain ⟨aC, bD⟩ : a ∈ C ∧ b ∈ D := by
     rw [←pair_mem_prod, ←h, pair_mem_prod]
     exact ⟨ha, hb⟩
-
   rw [ZFSet.ext_iff, ZFSet.ext_iff]
   suffices ∀ x y, (x ∈ A ↔ x ∈ C) ∧ (y ∈ B ↔ y ∈ D) by
     and_intros

ZFLean/Integers.lean

@@ -599,21 +599,16 @@ instance : IsOrderedAddMonoid ZFInt where
     · change x₁ + y₂ < x₂ + y₁ at h
       simp_rw [add_eq]
       left
-      change z₁ + x₁ + (z₂ + y₂) < z₂ + x₂ + (z₁ + y₁)
-      conv_lhs => rw [← ZFNat.add_assoc, ZFNat.add_comm z₁, ZFNat.add_comm z₂, ZFNat.add_assoc,
-        ←ZFNat.add_assoc, ZFNat.add_comm z₂]
-      conv_rhs => rw [ZFNat.add_comm z₂, ←ZFNat.add_assoc, ZFNat.add_comm z₂, ZFNat.add_comm z₁,
-        ZFNat.add_assoc, ZFNat.add_assoc, ←ZFNat.add_assoc]
-      exact ZFNat.add_lt_add_iff_right.mpr h
+      change (x₁ + z₁) + (y₂ + z₂) < (x₂ + z₂) + (y₁ + z₁)
+      ac_change (x₁ + y₂) + (z₁ + z₂) <  (x₂ + y₁) + (z₁ + z₂)
+      rwa [ZFNat.add_lt_add_iff_right]
     · rw [eq, ZFSet.zrel] at h
       dsimp at h
       right
       rw [add_eq, add_eq, eq, ZFSet.zrel]
       dsimp
-      conv_lhs => rw [← ZFNat.add_assoc, ZFNat.add_comm z₁, ZFNat.add_comm z₂, ZFNat.add_assoc,
-        ←ZFNat.add_assoc, ZFNat.add_comm z₂, h]
-      conv_rhs => rw [ZFNat.add_comm z₂, ←ZFNat.add_assoc, ZFNat.add_comm z₂, ZFNat.add_comm z₁,
-        ZFNat.add_assoc, ZFNat.add_assoc, ←ZFNat.add_assoc]
+      ac_change (x₁ + y₂) + (z₁ + z₂) =  (x₂ + y₁) + (z₁ + z₂)
+      rw [h]
 
 end Inequalities
 
@@ -923,29 +918,29 @@ theorem mul_eq_zero_iff {a b : ZFInt} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
     induction a using Quotient.ind
     induction b using Quotient.ind
     rename_i a b
-    let ⟨a₁, a₂⟩ := a
-    let ⟨b₁, b₂⟩ := b
     simp_rw [mk_eq, mul_eq, zero_eq, eq, ZFSet.zrel, ZFNat.add_zero] at h ⊢
-    rcases ZFNat.instIsStrictTotalOrderLt.trichotomous b₁ b₂ with h' | rfl | h'
+    rcases ZFNat.instIsStrictTotalOrderLt.trichotomous b.1 b.2 with h' | eq | h'
     · have := ZFNat.add_eq_add_sub_eq_sub h.symm
       rw [←ZFNat.left_distrib_mul_sub, ←ZFNat.left_distrib_mul_sub] at this
-      have b₁b₂_ne_0 : b₂ - b₁ ≠ 0 := by
+      have b₁b₂_ne_0 : b.2 - b.1 ≠ 0 := by
         intro contr
         rw [ZFNat.sub_eq_zero_imp_le] at contr
-        rcases contr with contr | rfl
+        rcases contr with contr | eq
         · nomatch ZFNat.lt_irrefl <| ZFNat.lt_trans contr h'
-        · nomatch ZFNat.lt_irrefl h'
+        · rw [eq] at h'
+          nomatch ZFNat.lt_irrefl h'
       left
       exact ZFNat.mul_right_cancel_iff b₁b₂_ne_0 |>.mp this
-    · right; rfl
+    · right; assumption
     · have := ZFNat.add_eq_add_sub_eq_sub h
       rw [←ZFNat.left_distrib_mul_sub, ←ZFNat.left_distrib_mul_sub] at this
-      have b₁b₂_ne_0 : b₁ - b₂ ≠ 0 := by
+      have b₁b₂_ne_0 : b.1 - b.2 ≠ 0 := by
         intro contr
         rw [ZFNat.sub_eq_zero_imp_le] at contr
-        rcases contr with contr | rfl
+        rcases contr with contr | eq
         · nomatch ZFNat.lt_irrefl <| ZFNat.lt_trans contr h'
-        · nomatch ZFNat.lt_irrefl h'
+        · rw [eq] at h'
+          nomatch ZFNat.lt_irrefl h'
       left
       exact ZFNat.mul_right_cancel_iff b₁b₂_ne_0 |>.mp this
   · rintro (h | h)
@@ -994,7 +989,7 @@ instance : PartialOrder ZFInt where
   lt_iff_le_not_ge := @lt_iff_le_not_ge
 
 instance : IsOrderedRing ZFInt where
-  add_le_add_left _ _ h z := (add_le_add_iff_left z).mpr h
+  add_le_add_left _ _ h z := add_le_add_left h z
   zero_le_one := Or.inl zero_lt_one
   mul_le_mul_of_nonneg_left a b := fun _ _ ↦ (mul_le_mul_left a · b)
   mul_le_mul_of_nonneg_right a h b c h' := by

ZFLean/Naturals.lean

@@ -327,8 +327,8 @@ theorem induction {P : ZFNat → Prop} (n : ZFNat)
     simpa [hn, zero_in_Nat, nat_zero_eq] using zero
   · intro m hm hm'
     unfold P' at *
-    simp [hm] at hm'
-    simp [succ_mem_Nat' hm]
+    rw [dif_pos hm] at hm'
+    rw [dif_pos <| succ_mem_Nat' hm]
     exact succ ⟨m, hm⟩ hm'
 
 @[cases_eliminator]
@@ -654,8 +654,8 @@ def rec.{u} {motive : ZFNat → Sort u} (n : ZFNat)
     simpa [hn, zero_in_Nat, nat_zero_eq] using zero
   · intro m hm hm'
     unfold motive' at *
-    simp [hm] at hm'
-    simp [succ_mem_Nat' hm]
+    rw [dif_pos hm] at hm'
+    rw [dif_pos <| succ_mem_Nat' hm]
     exact succ ⟨m, hm⟩ hm'
 
 /--
@@ -790,7 +790,7 @@ theorem add_left_cancel {n m k : ZFNat} : n + m = n + k ↔ m = k := by
   induction n with
   | zero => simp only [zero_add]
   | succ n ih =>
-    simp [add_succ]
+    simp_rw [add_succ]
     apply Iff.intro
     · intro h
       exact ih.mp (succ_inj h)
@@ -1496,7 +1496,6 @@ theorem ZFNat.ofNat_inj {n m : ℕ} : (n : ZFNat) = (m : ZFNat) ↔ n = m where
       conv_rhs at h =>
         unfold Nat.cast NatCast.natCast
       unfold_projs at h
-      simp at h
       unfold Nat.unaryCast at h
       split at h
       · rfl

ZFLean/Rationals.lean

@@ -242,7 +242,7 @@ theorem neg_add_cancel_right (a b : ZFRat) : a + -b + b = a := by
 
 theorem add_left_cancel {a b c : ZFRat} (h : a + b = a + c) : b = c := by
   have h₁ : -a + (a + b) = -a + (a + c) := by rw [h]
-  simp [add_assoc, add_left_neg, zero_add] at h₁
+  simp only [add_assoc, add_left_neg, zero_add] at h₁
   exact h₁
 
 @[simp]
@@ -533,7 +533,7 @@ noncomputable instance : DivisionRing ZFRat where
           _root_.mul_one] at hk
         dsimp
         have : n = Int.ofNat n.natAbs := by
-          rw [Int.ofNat_eq_coe, ←Int.eq_natAbs_of_nonneg hk]
+          rw [Int.ofNat_eq_natCast, ←Int.eq_natAbs_of_nonneg hk]
         rw [this]
         rfl
     dsimp [NNRat.cast, NNRatCast.nnratCast, NNRat.castRec]
@@ -542,57 +542,6 @@ noncomputable instance : DivisionRing ZFRat where
 
 noncomputable instance : Field ZFRat := {}
 
-section Order
-
-def lt (x y : ZFRat) : Prop :=
-  Quotient.liftOn₂ x y (fun ⟨a, b⟩ ⟨c, d⟩ ↦ a * d < c * b)
-    fun ⟨x₁, x₂, hx₂⟩ ⟨y₁, y₂, hy₂⟩ ⟨u₁, u₂, hu₂⟩ ⟨v₁, v₂, hv₂⟩ hxu hyv ↦ by
-      have h1 : x₁ * u₂ = x₂ * u₁ := hxu
-      have h2 : y₁ * v₂ = y₂ * v₁ := hyv
-      dsimp
-      ext
-      obtain u₂_neg | u₂_pos : u₂ < 0 ∨ 0 < u₂ := by
-        rcases lt_trichotomy u₂ 0 with h | rfl | h
-        · left; exact h
-        · contradiction
-        · right; exact h
-      all_goals
-        obtain v₂_neg | v₂_pos : v₂ < 0 ∨ 0 < v₂ := by
-          rcases lt_trichotomy v₂ 0 with h | rfl | h
-          · left; exact h
-          · contradiction
-          · right; exact h
-      all_goals
-        obtain x₂_neg | x₂_pos : x₂ < 0 ∨ 0 < x₂ := by
-          rcases lt_trichotomy x₂ 0 with h | rfl | h
-          · left; exact h
-          · contradiction
-          · right; exact h
-      all_goals
-        obtain y₂_neg | y₂_pos : y₂ < 0 ∨ 0 < y₂ := by
-          rcases lt_trichotomy y₂ 0 with h | rfl | h
-          · left; exact h
-          · contradiction
-          · right; exact h
-      all_goals constructor <;> intro h
-      · have : (x₁ * u₂) * (y₂ * v₂) < (y₁ * v₂) * (x₂ * u₂) := by
-          ac_change (x₁ * y₂) * (u₂ * v₂) < (y₁ * x₂) * (u₂ * v₂)
-          exact ZFInt.mul_lt_mul_of_pos_right h (ZFInt.mul_neg_neg_pos u₂ v₂ u₂_neg v₂_neg)
-        rw [h1, h2] at this
-        convert_to u₁ * v₂ * (y₂ * x₂) <  v₁ * u₂ * (y₂ * x₂) at this
-        · ac_rfl
-        · ac_rfl
-        · have mul_pos : 0 < y₂ * x₂ := ZFInt.mul_neg_neg_pos y₂ x₂ y₂_neg x₂_neg
-          rwa [mul_lt_mul_iff_of_pos_right mul_pos] at this
-      · sorry
-
-
-
-instance : LT ZFRat where lt := lt
-instance : LE ZFRat where le x y := x < y ∨ x = y
-
-end Order
-
 end Arithmetic
 end ZFRat
 end Rationals

lakefile.toml

@@ -12,6 +12,7 @@ maxSynthPendingDepth = 3
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
+rev = "v4.27.0"
 
 [[lean_lib]]
 name = "ZFLean"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.25.1
+leanprover/lean4:v4.27.0