bump

Author: riccardobrasca

FltRegular.lean

@@ -30,5 +30,3 @@ public import FltRegular.SmallNumbers.Seven.Seven
 public import FltRegular.SmallNumbers.SmallNumbers
 public import FltRegular.SmallNumbers.Thirteen.FLT13
 public import FltRegular.SmallNumbers.Thirteen.Thirteen
-import Mathlib.Tactic.NormNum.NatFactorial
-import Mathlib.Tactic.NormNum.Prime

FltRegular/CaseI/AuxLemmas.lean

@@ -54,6 +54,7 @@ theorem auxf0k₁ (hp5 : 5 ≤ p) (b : ℤ) : ∃ i : Fin p, f0k₁ b p (i : ℕ
   apply hpred
   simp [h2]
 
+set_option backward.isDefEq.respectTransparency false in
 include hpri in
 theorem aux0k₁ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p)
     (caseI : ¬↑p ∣ a * b * c) {k₁ k₂ : Fin p} (hcong : k₂ ≡ k₁ - 1 [ZMOD p])
@@ -93,6 +94,7 @@ theorem aux_cong0k₂ {k : Fin p} (hcong : k ≡ 1 [ZMOD p]) : k = ⟨1, hpri.on
 theorem auxf0k₂ (hp5 : 5 ≤ p) (a b : ℤ) : ∃ i : Fin p, f0k₂ a b (i : ℕ) = 0 :=
   ⟨⟨2, two_lt hp5⟩, rfl⟩
 
+set_option backward.isDefEq.respectTransparency false in
 include hpri in
 theorem aux0k₂ {a b : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (hab : ¬a ≡ b [ZMOD p])
     {k₁ k₂ : Fin p} (hcong : k₂ ≡ k₁ - 1 [ZMOD p])
@@ -167,6 +169,7 @@ include hpri in
 theorem auxf1k₂ (a : ℤ) : ∃ i : Fin p, f1k₂ a i = 0 :=
   ⟨⟨1, hpri.one_lt⟩, rfl⟩
 
+set_option backward.isDefEq.respectTransparency false in
 include hpri in
 theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p)
     (caseI : ¬↑p ∣ a * b * c) {k₁ k₂ : Fin p} (hcong : k₂ ≡ k₁ - 1 [ZMOD p])

FltRegular/CaseI/Statement.lean

@@ -143,6 +143,7 @@ theorem is_principal_aux {K' : Type*} [Field K'] [CharZero K'] [IsCyclotomicExte
 
 variable [hpri : Fact p.Prime]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem exists_ideal {a b c : ℤ} (h5p : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p)
     (hgcd : ({ a, b, c } : Finset ℤ).gcd id = 1)
     (caseI : ¬↑p ∣ a * b * c) {ζ : R} (hζ : ζ ∈ nthRootsFinset p 1) :
@@ -160,6 +161,7 @@ theorem exists_ideal {a b c : ℤ} (h5p : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p)
   · exact hpri.out
   · exact h5p
 
+set_option backward.isDefEq.respectTransparency false in
 theorem is_principal {a b c : ℤ} {ζ : R} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p)
     (hgcd : ({ a, b, c } : Finset ℤ).gcd id = 1) (caseI : ¬↑p ∣ a * b * c)
     (H : a ^ p + b ^ p = c ^ p) (hζ : IsPrimitiveRoot ζ p) :
@@ -168,6 +170,7 @@ theorem is_principal {a b c : ℤ} {ζ : R} (hreg : IsRegularPrime p) (hp5 : 5 
   obtain ⟨I, hI⟩ := exists_ideal hp5 H hgcd caseI hζ
   exact is_principal_aux hreg hI
 
+set_option backward.isDefEq.respectTransparency false in
 theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime p)
     (hζ : IsPrimitiveRoot ζ p) (hgcd : ({a, b, c} : Finset ℤ).gcd id = 1) (caseI : ¬↑p ∣ a * b * c)
     (H : a ^ p + b ^ p = c ^ p) :
@@ -211,6 +214,7 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
     simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd,
       Int.cast_sub, ZMod.intCast_mod, Int.cast_mul, Int.cast_one, sub_self]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Case I with additional assumptions. -/
 theorem caseI_easier {a b c : ℤ} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p)
     (hgcd : ({a, b, c} : Finset ℤ).gcd id = 1) (hab : ¬a ≡ b [ZMOD p]) (caseI : ¬↑p ∣ a * b * c) :

FltRegular/CaseII/AuxLemmas.lean

@@ -13,6 +13,7 @@ lemma WfDvdMonoid.multiplicity_finite_iff [WfDvdMonoid M] {x y : M} :
     FiniteMultiplicity x y ↔ ¬IsUnit x ∧ y ≠ 0 :=
   ⟨fun h => ⟨h.not_unit, h.ne_zero⟩, and_imp.mpr FiniteMultiplicity.of_not_isUnit⟩
 
+set_option backward.isDefEq.respectTransparency false in
 lemma dvd_iff_emultiplicity_le [UniqueFactorizationMonoid M] {a b : M} (ha : a ≠ 0) :
     a ∣ b ↔ ∀ p : M, Prime p → emultiplicity p a ≤ emultiplicity p b := by
   constructor
@@ -43,6 +44,7 @@ lemma dvd_iff_emultiplicity_le [UniqueFactorizationMonoid M] {a b : M} (ha : a 
           (FiniteMultiplicity.of_not_isUnit hq.not_unit hq.ne_zero).emultiplicity_self,
           add_comm, add_le_add_iff_right_of_ne_top (ENat.coe_ne_top _), Nat.one_le_cast] at this
 
+set_option backward.isDefEq.respectTransparency false in
 lemma pow_dvd_pow_iff_dvd [UniqueFactorizationMonoid M] {a b : M} {x : ℕ} (h' : x ≠ 0) :
     a ^ x ∣ b ^ x ↔ a ∣ b := by
   classical

FltRegular/CaseII/InductionStep.lean

@@ -91,6 +91,7 @@ lemma x_plus_y_mul_ne_zero : x + y * η ≠ 0 := by
 
 variable [IsCyclotomicExtension {p} ℚ K]
 
+set_option backward.isDefEq.respectTransparency false in
 include e hp in
 /- Let π = ζ -1, then π divides x+yη with η a primivite root of unity. -/
 lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
@@ -140,6 +141,7 @@ lemma div_zeta_sub_one_sub (η₁ η₂) (hη : η₁ ≠ η₂) :
   rw [Ne, ← Subtype.ext_iff.not]
   exact hη
 
+set_option backward.isDefEq.respectTransparency false in
 include hy in
 /- sending η to (x+yη)/(ζ-1) mod (π) = 𝔭 is injective. -/
 lemma div_zeta_sub_one_Injective :
@@ -159,6 +161,7 @@ instance : Finite (𝓞 K ⧸ 𝔭) := by
   rw [← Ideal.absNorm_ne_zero_iff, Ne, Ideal.absNorm_eq_zero_iff, Ideal.span_singleton_eq_bot]
   exact hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt
 
+set_option backward.isDefEq.respectTransparency false in
 include hy in
 /- sending η to (x+yη)/(ζ-1) mod (π) = 𝔭 is bijective. -/
 lemma div_zeta_sub_one_Bijective :
@@ -331,8 +334,8 @@ lemma p_dvd_a_iff : 𝔭 ∣ 𝔞 η ↔ η = η₀ := by
 lemma p_pow_dvd_c_eta_zero : 𝔭 ^ (m * p) ∣ 𝔠 η₀ := by
   classical
   rw [← one_mul (𝔠 η₀), ← p_pow_dvd_c_eta_zero_aux hp hζ e hy, dvd_gcd_mul_iff_dvd_mul,
-    mul_comm _ (𝔠 η₀), ← Finset.prod_eq_mul_prod_diff_singleton (Finset.mem_attach _ η₀) 𝔠,
-    prod_c, mul_pow]
+    mul_comm _ (𝔠 η₀)]
+  rw [← Finset.prod_eq_mul_prod_diff_singleton_of_mem (Finset.mem_attach _ η₀) 𝔠,prod_c, mul_pow]
   apply dvd_mul_of_dvd_right
   rw [pow_mul]
 
@@ -560,6 +563,7 @@ lemma exists_solution :
       (a_div_a_zero_denom_spec hp hζ e hy hz η₁ hreg hη₁)
       (a_div_a_zero_denom_spec hp hζ e hy hz η₂ hreg hη₂)
 
+set_option backward.isDefEq.respectTransparency false in
 include hp hreg e hy hz in
 lemma exists_solution' :
     ∃ (x' y' z' : 𝓞 K) (ε₃ : (𝓞 K)ˣ),

FltRegular/CaseII/Statement.lean

@@ -33,6 +33,7 @@ lemma not_exists_solution {m : ℕ} (hm : 1 ≤ m) :
       rintro ⟨x, y, z, ε₃, hy, hz, e⟩
       exact IH (exists_solution' hp hζ e hy hz hreg)
 
+set_option backward.isDefEq.respectTransparency false in
 include hp hreg in
 lemma not_exists_solution' :
   ¬∃ (x y z : 𝓞 K), ¬(hζ.unit' : 𝓞 K) - 1 ∣ y ∧ (hζ.unit' : 𝓞 K) - 1 ∣ z ∧ z ≠ 0 ∧
@@ -58,6 +59,7 @@ lemma not_exists_solution' :
   refine not_exists_solution hp hreg hζ hm ⟨x, y, z, 1, hy, hz'', ?_⟩
   rwa [Units.val_one, one_mul]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma not_exists_Int_solution {p : ℕ} [hpri : Fact (Nat.Prime p)] (hreg : IsRegularPrime p)
     (hodd : p ≠ 2) : ¬∃ (x y z : ℤ), ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p := by
   haveI := CyclotomicField.isCyclotomicExtension p ℚ

FltRegular/MayAssume/Lemmas.lean

@@ -99,7 +99,6 @@ theorem a_not_cong_b {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp5 : 5 ≤ p) (h
     ring
   · convert hprod using 1
     ring
-  · ring_nf at caseI ⊢
-    exact caseI
+  · grind
 
 end FltRegular

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -108,17 +108,21 @@ section NeZero
 
 variable [NeZero p]
 
+set_option backward.isDefEq.respectTransparency false in
 instance : IsGalois ℚ (CyclotomicField p ℚ) :=
   IsCyclotomicExtension.isGalois {p} _ _
 
+set_option backward.isDefEq.respectTransparency false in
 instance : FiniteDimensional ℚ (CyclotomicField p ℚ) :=
   IsCyclotomicExtension.finiteDimensional {p} _ _
 
+set_option backward.isDefEq.respectTransparency false in
 instance : NumberField (CyclotomicField p ℚ) :=
   IsCyclotomicExtension.numberField {p} ℚ _
 
 end NeZero
 
+set_option backward.isDefEq.respectTransparency false in
 theorem zeta_sub_one_dvb_p [Fact p.Prime] {η : R} (hη : η ∈ nthRootsFinset p 1)
     (hne1 : η ≠ 1) : 1 - η ∣ (p : R) := by
   have hη : IsPrimitiveRoot (η : CyclotomicField p ℚ) (p ^ 1) := by
@@ -130,6 +134,7 @@ theorem zeta_sub_one_dvb_p [Fact p.Prime] {η : R} (hη : η ∈ nthRootsFinset
   ext
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 theorem one_sub_zeta_prime [Fact p.Prime] {η : R} (hη : η ∈ nthRootsFinset p 1)
     (hne1 : η ≠ 1) : Prime (1 - η) := by
   have h := prim_coe η (isPrimitiveRoot_of_mem_nthRootsFinset Fact.out hη hne1)
@@ -282,6 +287,7 @@ theorem fltIdeals_coprime (hpri : p.Prime) (p5 : 5 ≤ p) {x y z : ℤ}
 
 variable {L}
 
+set_option backward.isDefEq.respectTransparency false in
 theorem dvd_last_coeff_cycl_integer [hp : Fact p.Prime] {ζ : 𝓞 L}
     (hζ : IsPrimitiveRoot ζ p) {f : Fin p → ℤ}
     (hf : ∃ i, f i = 0) {m : ℤ} (hdiv : ↑m ∣ ∑ j, f j • ζ ^ (j : ℕ)) :
@@ -329,6 +335,7 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact p.Prime] {ζ : 𝓞 L}
   rw [hy]
   simp [dvd_neg]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem dvd_coeff_cycl_integer (hp : p.Prime) {ζ : 𝓞 L} (hζ : IsPrimitiveRoot ζ p)
     {f : Fin p → ℤ} (hf : ∃ i, f i = 0) {m : ℤ} (hdiv : ↑m ∣ ∑ j, f j • ζ ^ (j : ℕ)) :
     ∀ j, m ∣ f j := by

FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean

@@ -51,6 +51,7 @@ lemma isCoprime_of_not_zeta_sub_one_dvd {x : 𝓞 K} (hx : ¬ (hζ.unit' : 𝓞
     Ideal.mem_span_singleton]
   · simpa only [ge_iff_le, tsub_pos_iff_lt] using hpri.out.one_lt
 
+set_option backward.isDefEq.respectTransparency false in
 lemma exists_zeta_sub_one_dvd_sub_Int (a : 𝓞 K) : ∃ b : ℤ, (hζ.unit' - 1 : 𝓞 K) ∣ a - b := by
   letI : Fact (Nat.Prime p) := hpri
   simp_rw [← Ideal.Quotient.eq_zero_iff_dvd, ← Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_sub,
@@ -109,6 +110,7 @@ lemma IsPrimitiveRoot.sub_one_dvd_sub {A : Type*} [CommRing A] [IsDomain A]
   · rw [h, sub_self]; exact dvd_zero _
   · exact (hζ.ntRootsFinset_pairwise_associated_sub_one_sub_of_prime hp hη₁ hη₂ h).dvd
 
+set_option backward.isDefEq.respectTransparency false in
 lemma quotient_zero_sub_one_comp_aut (σ : 𝓞 K →+* 𝓞 K) :
     (Ideal.Quotient.mk (Ideal.span {(hζ.unit' : 𝓞 K) - 1})).comp σ = Ideal.Quotient.mk _ := by
   have : Fact (Nat.Prime p) := hpri
@@ -128,8 +130,7 @@ lemma quotient_zero_sub_one_comp_aut (σ : 𝓞 K →+* 𝓞 K) :
   · rw [mem_nthRootsFinset (NeZero.pos p), ← map_pow, hζ.unit'_coe.pow_eq_one, map_one]
   · rw [mem_nthRootsFinset (NeZero.pos p), hζ.unit'_coe.pow_eq_one]
 
-set_option synthInstance.maxHeartbeats 80000 in
--- Needed for `AddMonoidHomClass (𝓞 K →+* 𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) ? ?`
+set_option backward.isDefEq.respectTransparency false in
 open NumberField.RingOfIntegers in
 lemma zeta_sub_one_dvd_trace_sub_smul (x : 𝓞 K) :
     (hζ.unit' - 1 : 𝓞 K) ∣ Algebra.trace ℤ _ x - (p - 1) • x := by
@@ -149,6 +150,7 @@ lemma zeta_sub_one_dvd_trace_sub_smul (x : 𝓞 K) :
     IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat (NeZero.pos p)),
     Nat.totient_prime hpri.out]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma zeta_sub_one_pow_dvd_norm_sub_pow (x : 𝓞 K) :
     (hζ.unit' - 1 : 𝓞 K) ^ p ∣ (Algebra.norm ℤ (1 + p • x) : 𝓞 K) - 1 + p • x := by
   letI := IsCyclotomicExtension.numberField {p} ℚ K
@@ -171,6 +173,7 @@ lemma zeta_sub_one_pow_dvd_norm_sub_pow (x : 𝓞 K) :
     zify [(Nat.Prime.one_lt hpri.out).le]
     linarith only [Nat.Prime.two_le hpri.out]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma norm_add_one_smul_of_isUnit {K} [Field K] [NumberField K] {p : ℕ} (hpri : p.Prime)
     (hp : p ≠ 2) (x : 𝓞 K)
     (hx : IsUnit (1 + p • x)) : Algebra.norm ℤ (1 + p • x) = 1 := by

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -48,6 +48,7 @@ theorem IsPrimitiveRoot.unit'_coe : IsPrimitiveRoot hζ.unit'.1 p := by
   rw [← this] at z1
   exact z1.of_map_of_injective (IsFractionRing.injective _ _)
 
+set_option backward.isDefEq.respectTransparency false in
 theorem eq_one_mod_one_sub {A : Type*} [CommRing A] {t : A} :
     algebraMap A (A ⧸ Ideal.span ({t - 1} : Set A)) t = 1 :=
   by
@@ -56,13 +57,15 @@ theorem eq_one_mod_one_sub {A : Type*} [CommRing A] {t : A} :
   apply Ideal.subset_span
   exact Set.mem_singleton _
 
+set_option backward.isDefEq.respectTransparency false in
 theorem IsPrimitiveRoot.eq_one_mod_sub_of_pow {A : Type*} [CommRing A] [IsDomain A] {ζ : A}
     (hζ : IsPrimitiveRoot ζ p) {μ : A} (hμ : μ ^ p = 1) :
     (@DFunLike.coe _ A (fun _ => A ⧸ Ideal.span {ζ - 1}) _
       (algebraMap A (A ⧸ Ideal.span {ζ - 1})) μ) = 1 := by
   obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ
   rw [map_pow, eq_one_mod_one_sub, one_pow]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem aux {t} {l : 𝓞 K} {f : Fin t → ℤ} {μ : K} (hμ : IsPrimitiveRoot μ p)
     (h : ∑ x : Fin t, f x • (⟨μ, hμ.isIntegral (NeZero.pos p)⟩ : 𝓞 K) ^ (x : ℕ) = l) :
     algebraMap (𝓞 K) (𝓞 K ⧸ I) l = ∑ x : Fin t, (f x : 𝓞 K ⧸ I) := by
@@ -92,6 +95,7 @@ theorem IsPrimitiveRoot.p_mem_one_sub_zeta [hp : Fact p.Prime] : (p : 𝓞 K) 
 
 variable [IsCyclotomicExtension {p} ℚ K]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem roots_of_unity_in_cyclo_aux {x : K} {l : ℕ} (hl : l ≠ 0) (hx : IsIntegral ℤ x)
     (hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩) {ζ : K} (hζ : IsPrimitiveRoot ζ p) : l ∣ 2 * p := by
   by_contra h
@@ -136,7 +140,7 @@ theorem roots_of_unity_in_cyclo_aux {x : K} {l : ℕ} (hl : l ≠ 0) (hx : IsInt
     simp_rw [pdivlcm_h] at this
     apply absurd this h
 
---do more generally
+set_option backward.isDefEq.respectTransparency false in
 theorem roots_of_unity_in_cyclo (hpo : Odd p) (x : K)
     (h : ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1) :
     ∃ (m k : ℕ), x = (-1) ^ k * (hζ.unit'.1 : K) ^ m :=  by
@@ -228,6 +232,7 @@ theorem IsCyclotomicExtension.IsCMField (hp : 2 < p) :
   haveI := nrRealPlaces_eq_zero_iff.1 (Rat.nrRealPlaces_eq_zero K hp)
   ⟨⟩
 
+set_option backward.isDefEq.respectTransparency false in
 lemma unit_inv_conj_not_neg_zeta_runity_aux (u : (𝓞 K)ˣ) [Fact (p.Prime)] (hp : 2 < p) :
     haveI := IsCyclotomicExtension.IsCMField K hp
     algebraMap (𝓞 K) (𝓞 K ⧸ I) (unitsMulComplexConjInv K u).1 = 1 := by
@@ -272,6 +277,7 @@ lemma unit_inv_conj_not_neg_zeta_runity_aux (u : (𝓞 K)ˣ) [Fact (p.Prime)] (h
     rw [this a]
   exact (aux hζ hζ hu).trans (aux hζ hζ.inv hu').symm
 
+set_option backward.isDefEq.respectTransparency false in
 theorem unit_inv_conj_not_neg_zeta_runity (u : (𝓞 K)ˣ) (n : ℕ) [Fact (p.Prime)] (hp : 2 < p) :
     haveI := IsCyclotomicExtension.IsCMField K hp
     u * (unitsComplexConj K u)⁻¹ ≠ -hζ.unit' ^ n := by
@@ -316,6 +322,7 @@ theorem unit_inv_conj_is_root_of_unity (u : (𝓞 K)ˣ) [H : Fact (p.Prime)] (hp
     · exact NumberField.RingOfIntegers.isIntegral_coe _
   · simp
 
+set_option backward.isDefEq.respectTransparency false in
 lemma IsPrimitiveRoot.eq_one_mod_one_sub' {A : Type*} [CommRing A] [IsDomain A]
     {n : ℕ} [NeZero n] {ζ : A} (hζ : IsPrimitiveRoot ζ n) {η : A} (hη : η ∈ nthRootsFinset n 1) :
     Ideal.Quotient.mk (Ideal.span ({ζ - 1} : Set A)) η = 1 := by