From cafcac5eea35c5d76e8f654e40231a2b8f7224ef Mon Sep 17 00:00:00 2001 From: riccardobrasca Date: Mon, 11 Mar 2024 19:52:26 +0100 Subject: [PATCH] bump --- FltRegular/CaseI/Statement.lean | 8 ++++---- FltRegular/MayAssume/Lemmas.lean | 16 ++++++++-------- FltRegular/NumberTheory/Hilbert92.lean | 9 +++++---- lake-manifest.json | 14 +++++++------- lean-toolchain | 2 +- 5 files changed, 25 insertions(+), 24 deletions(-) diff --git a/FltRegular/CaseI/Statement.lean b/FltRegular/CaseI/Statement.lean index 766e2790..fb235243 100644 --- a/FltRegular/CaseI/Statement.lean +++ b/FltRegular/CaseI/Statement.lean @@ -238,10 +238,10 @@ theorem auxf' (hp5 : 5 ≤ p) (a b : ℤ) (k₁ k₂ : Fin p) : exact Nat.sub_pos_of_lt (lt_of_lt_of_le this hp5) obtain ⟨i, hi⟩ := hcard refine' ⟨i, sdiff_subset _ _ hi, _⟩ - have hi0 : i ≠ 0 := fun h => by simp [h] at hi - have hi1 : i ≠ 1 := fun h => by simp [h] at hi - have hik₁ : i ≠ k₁ := fun h => by simp [h] at hi - have hik₂ : i ≠ k₂ := fun h => by simp [h] at hi + have hi0 : i ≠ 0 := fun h => by simp [h, s] at hi + have hi1 : i ≠ 1 := fun h => by simp [h, s] at hi + have hik₁ : i ≠ k₁ := fun h => by simp [h, s] at hi + have hik₂ : i ≠ k₂ := fun h => by simp [h, s] at hi simp [f, hi0, hi1, hik₁, hik₂] theorem auxf (hp5 : 5 ≤ p) (a b : ℤ) (k₁ k₂ : Fin p) : ∃ i : Fin p, f a b k₁ k₂ (i : ℕ) = 0 := diff --git a/FltRegular/MayAssume/Lemmas.lean b/FltRegular/MayAssume/Lemmas.lean index 1a474edc..e231633f 100644 --- a/FltRegular/MayAssume/Lemmas.lean +++ b/FltRegular/MayAssume/Lemmas.lean @@ -27,24 +27,24 @@ theorem coprime {a b c : ℤ} {n : ℕ} (H : a ^ n + b ^ n = c ^ n) (hprod : a * have hc : c ≠ 0 := fun hc => by simp [hc] at hprod let s : Finset ℤ := {a, b, c} set d : ℤ := s.gcd id - have hadiv : d ∣ a := gcd_dvd (by simp) - have hbdiv : d ∣ b := gcd_dvd (by simp) - have hcdiv : d ∣ c := gcd_dvd (by simp) + have hadiv : d ∣ a := gcd_dvd (by simp [s]) + have hbdiv : d ∣ b := gcd_dvd (by simp [s]) + have hcdiv : d ∣ c := gcd_dvd (by simp [s]) have hdzero : d ≠ 0 := fun hdzero => by - simpa [ha] using Finset.gcd_eq_zero_iff.1 hdzero a (by simp) + simpa [ha] using Finset.gcd_eq_zero_iff.1 hdzero a (by simp [s]) have hdp : d ^ n ≠ 0 := fun hdn => hdzero (pow_eq_zero hdn) refine' ⟨_, _, fun habs => _⟩ · obtain ⟨na, hna⟩ := hadiv; obtain ⟨nb, hnb⟩ := hbdiv; obtain ⟨nc, hnc⟩ := hcdiv rwa [← mul_left_inj' hdp, add_mul, ← mul_pow, ← mul_pow, ← mul_pow, hna, hnb, hnc, Int.mul_ediv_cancel_left _ hdzero, Int.mul_ediv_cancel_left _ hdzero, Int.mul_ediv_cancel_left _ hdzero, mul_comm, ← hna, mul_comm, ← hnb, mul_comm, ← hnc] - · simpa [gcd_eq_gcd_image] using + · simpa [gcd_eq_gcd_image, d] using Finset.Int.gcd_div_id_eq_one (show a ∈ ({a, b, c} : Finset ℤ) by simp) ha · simp only [mul_eq_zero] at habs rcases habs with ((Ha | Hb) | Hc) - · exact ha (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp)) Ha) - · exact hb (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp)) Hb) - · exact hc (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp)) Hc) + · exact ha (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Ha) + · exact hb (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Hb) + · exact hc (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Hc) end MayAssume diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 211ef790..6014ce0c 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -221,7 +221,7 @@ lemma corollary [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental) (a ← sum_add_distrib, Finsupp.total_apply, Finsupp.sum_fintype] congr · ext j - simp only [smul_smul, Finsupp.ofSupportFinite_coe, add_smul] + simp only [smul_smul, Finsupp.ofSupportFinite_coe, add_smul, b', b] congr 1 · rw [mul_comm] · rw [← intCast_smul (k := A), smul_smul] @@ -871,9 +871,10 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) : intro i induction i using Fin.lastCases with | last => - simp only [Fin.snoc_last, toMul_ofMul, Units.coe_map, RingOfIntegers.norm_apply_coe] + simp only [Fin.snoc_last, toMul_ofMul, Units.coe_map, RingOfIntegers.norm_apply_coe, NE, η, H2] | cast i => - simp only [Fin.snoc_castSucc, toMul_ofMul, Units.coe_map, RingOfIntegers.norm_apply_coe] + simp only [Fin.snoc_castSucc, toMul_ofMul, Units.coe_map, RingOfIntegers.norm_apply_coe, NE, + η, H2, J, N, H] · intro ε hε refine hS.corollary p hp _ _ (finrank_G p hp hKL σ hσ) _ (ι ∘ Fin.castSucc) ?_ (mkG ε) ?_ · by_contra hε' @@ -921,7 +922,7 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) : Fin.sum_univ_castSucc] simp only [Fin.snoc_castSucc, toMul_zsmul, unit_to_U_zpow, unitlifts_spec, Fin.snoc_last, toMul_ofMul, RingHom.toMonoidHom_eq_coe, zpow_neg, unit_to_U_inv, Function.comp_apply, - unit_to_U_map, smul_zero, neg_zero, add_zero, add_right_eq_self] + unit_to_U_map, smul_zero, neg_zero, add_zero, add_right_eq_self, NE, η, H2, J, N, H] apply_fun mkG at NE_p_pow simp only [RingHom.toMonoidHom_eq_coe, unit_to_U_map, unit_to_U_neg, unit_to_U_pow] at NE_p_pow diff --git a/lake-manifest.json b/lake-manifest.json index b13bff0f..a209ffcb 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,10 +4,10 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "a7543d1a6934d52086971f510e482d743fe30cf3", + "rev": "ff9850c4726f6b9fb8d8e96980c3fcb2900be8bd", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/quote4", @@ -22,19 +22,19 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b", + "rev": "056ca0fa8f5585539d0b940f532d9750c3a2270f", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "16cae05860b208925f54e5581ec5fd264823440c", + "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.29", + "inputRev": "v0.0.30", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "1095e9af4d1f75960ab5485a6c5b3a851f48b5f4", + "rev": "f884087a041da7998696e87352f6f06e2e5f5713", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index 50262040..e35881ce 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.6.0 +leanprover/lean4:v4.7.0-rc2