diff --git a/ZFLean/Basic.lean b/ZFLean/Basic.lean index e770eb2..6e99f16 100644 --- a/ZFLean/Basic.lean +++ b/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 diff --git a/ZFLean/Integers.lean b/ZFLean/Integers.lean index b02d1c8..edd83a4 100644 --- a/ZFLean/Integers.lean +++ b/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 diff --git a/ZFLean/Naturals.lean b/ZFLean/Naturals.lean index 49beff9..599aefe 100644 --- a/ZFLean/Naturals.lean +++ b/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 diff --git a/ZFLean/Rationals.lean b/ZFLean/Rationals.lean index d786c22..e2503ba 100644 --- a/ZFLean/Rationals.lean +++ b/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 diff --git a/lakefile.toml b/lakefile.toml index 13af78c..819228d 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -12,6 +12,7 @@ maxSynthPendingDepth = 3 [[require]] name = "mathlib" scope = "leanprover-community" +rev = "v4.27.0" [[lean_lib]] name = "ZFLean" diff --git a/lean-toolchain b/lean-toolchain index 4bd92b6..2bb276a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.25.1 +leanprover/lean4:v4.27.0 \ No newline at end of file