Merge pull request #103 from leanprover-community/v4.8.0

wip

Author: riccardobrasca

FltRegular/CaseI/AuxLemmas.lean

@@ -46,8 +46,8 @@ theorem auxf0k₁ (hp5 : 5 ≤ p) (b : ℤ) : ∃ i : Fin P, f0k₁ b p (i : ℕ
     intro h
     simp only [Fin.ext_iff, Fin.val_mk] at h
     replace h := h.symm
-    rw [Nat.pred_eq_succ_iff] at h
-    linarith
+    rw [Nat.pred_eq_sub_one] at h
+    omega
   simp only [f0k₁, OfNat.ofNat_ne_one, ite_false, ite_eq_right_iff, neg_eq_zero]
   intro h2
   exfalso
@@ -65,9 +65,9 @@ theorem aux0k₁ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
   have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₁ b p j • ζ ^ j := by
     convert hdiv using 1
     have h : 1 ≠ p.pred := fun h => by linarith [pred_eq_succ_iff.1 h.symm]
-    simp_rw [f0k₁, ite_smul, sum_ite, filter_filter, ← Ne.def, ne_and_eq_iff_right h,
+    simp_rw [f0k₁, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right h,
       Finset.range_filter_eq]
-    simp [hpri.one_lt, pred_lt hpri.ne_zero, sub_eq_add_neg]
+    simp [hpri.one_lt, Nat.sub_lt hpri.pos, sub_eq_add_neg]
   rw [sum_range] at key
   refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_left _ _) _)
   replace hpri : (P : ℕ).Prime := hpri
@@ -112,10 +112,10 @@ theorem aux0k₂ {a b : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ
     ← sub_mul, add_sub_right_comm, show ζ = ζ ^ ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) by simp] at hdiv
   have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₂ a b j • ζ ^ j := by
     convert hdiv using 1
-    simp_rw [f0k₂, ite_smul, sum_ite, filter_filter, ← Ne.def, ne_and_eq_iff_right zero_ne_one,
+    simp_rw [f0k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right zero_ne_one,
       Finset.range_filter_eq]
     simp only [hpri.pos, hpri.one_lt, if_true, zsmul_eq_mul, Int.cast_sub, sum_singleton,
-      _root_.pow_zero, mul_one, pow_one, Ne.def, zero_smul, sum_const_zero, add_zero, Fin.val_mk]
+      _root_.pow_zero, mul_one, pow_one, Ne, zero_smul, sum_const_zero, add_zero, Fin.val_mk]
   rw [sum_range] at key
   refine' hab _
   symm
@@ -194,7 +194,7 @@ theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
   have key : ↑(p : ℤ) ∣ ∑ j in range p, f1k₂ a j • ζ ^ j := by
     suffices ∑ j in range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2 by
       rwa [this]
-    simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.def, ne_and_eq_iff_right
+    simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right
       (show 0 ≠ 2 by norm_num), Finset.range_filter_eq]
     simp only [hpri.pos, ite_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero, mul_one, two_lt hp5, neg_smul,
   sum_neg_distrib, ne_eq, mem_range, not_and, not_not, zero_smul, sum_const_zero, add_zero]

FltRegular/CaseI/Statement.lean

@@ -237,11 +237,11 @@ theorem caseI_easier {a b c : ℤ} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p)
     have h1k₁ := aux1k₁ hpri.out hp5 hζ hab hcong hdiv
     have h1k₂ := aux1k₂ hpri.out hp5 hζ caseI hcong hdiv
     have hk₁k₂ : (k₁ : ℕ) ≠ (k₂ : ℕ) := auxk₁k₂ hpri.out hcong
-    simp_rw [f, ite_smul, sum_ite, filter_filter, ← Ne.def, ne_and_eq_iff_right h01, and_assoc,
+    simp_rw [f, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right h01, and_assoc,
       ne_and_eq_iff_right h1k₁, ne_and_eq_iff_right h0k₁, ne_and_eq_iff_right hk₁k₂,
       ne_and_eq_iff_right h1k₂, ne_and_eq_iff_right h0k₂, Finset.range_filter_eq]
     simp only [hpri.out.pos, hpri.out.one_lt, if_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero,
-      mul_one, pow_one, Fin.is_lt, neg_smul, sum_neg_distrib, Ne.def, zero_smul, sum_const_zero,
+      mul_one, pow_one, Fin.is_lt, neg_smul, sum_neg_distrib, Ne, zero_smul, sum_const_zero,
       add_zero]
     ring
   rw [sum_range] at key

FltRegular/CaseII/AuxLemmas.lean

@@ -44,7 +44,7 @@ lemma WfDvdMonoid.multiplicity_finite_iff {M : Type*} [CancelCommMonoidWithZero
     {x y : M} :
   multiplicity.Finite x y ↔ ¬IsUnit x ∧ y ≠ 0 := by
   constructor
-  · rw [← not_imp_not, Ne.def, ← not_or, not_not]
+  · rw [← not_imp_not, Ne, ← not_or, not_not]
     rintro (hx|hy)
     · exact fun ⟨n, hn⟩ ↦ hn (hx.pow _).dvd
     · simp [hy]
@@ -135,7 +135,7 @@ theorem isPrincipal_of_isPrincipal_pow_of_Coprime'
   by_cases Izero : I = 0
   · rw [Izero, FractionalIdeal.coe_zero]
     exact bot_isPrincipal
-  rw [← Ne.def, ← isUnit_iff_ne_zero] at Izero
+  rw [← Ne, ← isUnit_iff_ne_zero] at Izero
   show Submodule.IsPrincipal (Izero.unit' : FractionalIdeal A⁰ K)
   rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← H, Nat.dvd_gcd_iff]
   refine ⟨?_, orderOf_dvd_card⟩
@@ -153,9 +153,9 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD
     ∃ a b : R, ¬(x ∣ a) ∧ ¬(x ∣ b) ∧ spanSingleton R⁰ (algebraMap R K a / algebraMap R K b) = I / J := by
   by_contra H1
   have hI' : (I : FractionalIdeal R⁰ K) ≠ 0 :=
-    by rw [← coeIdeal_bot, Ne.def, coeIdeal_inj]; rintro rfl; exact hI (dvd_zero _)
+    by rw [← coeIdeal_bot, Ne, coeIdeal_inj]; rintro rfl; exact hI (dvd_zero _)
   have hJ' : (J : FractionalIdeal R⁰ K) ≠ 0 :=
-    by rw [← coeIdeal_bot, Ne.def, coeIdeal_inj]; rintro rfl; exact hJ (dvd_zero _)
+    by rw [← coeIdeal_bot, Ne, coeIdeal_inj]; rintro rfl; exact hJ (dvd_zero _)
   have : ∀ n : ℕ, (1 ≤ n) → ¬∃ a b : R, ¬(x ^ n ∣ a) ∧ ¬(x ^ n ∣ b) ∧
     spanSingleton R⁰ (algebraMap R K a / algebraMap R K b) = I / J := by
     intro n hn
@@ -169,7 +169,7 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD
         ← mul_div_right_comm, eq_div_iff hJ', ← coeIdeal_span_singleton, ← coeIdeal_span_singleton,
         ← coeIdeal_mul, ← coeIdeal_mul, coeIdeal_inj] at e
       on_goal 2 =>
-        rw [Ne.def, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero,
+        rw [Ne, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero,
           (IsFractionRing.injective R K).eq_iff]
         rintro rfl
         apply hb (dvd_zero _)
@@ -180,7 +180,7 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD
             rwa [Irreducible.gcd_eq_one_iff]
             · rwa [irreducible_iff_prime, Ideal.prime_iff_isPrime, Ideal.span_singleton_prime]
               · exact hx.ne_zero
-              · rw [Ne.def, Ideal.span_singleton_eq_bot]
+              · rw [Ne, Ideal.span_singleton_eq_bot]
                 exact hx.ne_zero
           rw [← Ideal.mem_span_singleton, ← Ideal.dvd_span_singleton] at ha' ⊢
           replace h := ha'.trans (dvd_mul_right _ J)
@@ -190,7 +190,7 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD
         rw [pow_succ', mul_dvd_mul_iff_left hx.ne_zero] at ha hb
         rw [_root_.map_mul, _root_.map_mul, mul_div_mul_left] at e₀
         · exact IH ⟨a', b', ha, hb, e₀⟩
-        · rw [Ne.def, ← (algebraMap R K).map_zero, (IsFractionRing.injective R K).eq_iff]
+        · rw [Ne, ← (algebraMap R K).map_zero, (IsFractionRing.injective R K).eq_iff]
           exact hx.ne_zero
       · refine IH ⟨a, b, h, ?_, e₀⟩
         intro hb
@@ -202,7 +202,7 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD
             IsCoprime.pow_left_iff, Ideal.isCoprime_iff_gcd, Irreducible.gcd_eq_one_iff]
           · rwa [irreducible_iff_prime, Ideal.prime_iff_isPrime, Ideal.span_singleton_prime]
             · exact hx.ne_zero
-            · rw [Ne.def, Ideal.span_singleton_eq_bot]
+            · rw [Ne, Ideal.span_singleton_eq_bot]
               exact hx.ne_zero
           · rwa [Nat.pos_iff_ne_zero, ← Nat.one_le_iff_ne_zero]
         rwa [← e, mul_comm, ← dvd_gcd_mul_iff_dvd_mul, this, one_mul] at hb

FltRegular/CaseII/InductionStep.lean

@@ -17,7 +17,7 @@ attribute [local instance 2000] Algebra.toModule Module.toDistribMulAction AddMo
   Semiring.toNonUnitalSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring
   NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocSemiring.toMulZeroClass
   MulZeroClass.toMul Submodule.idemSemiring IdemSemiring.toSemiring
-  Submodule.instIdemCommSemiringSubmoduleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToModule
+  Submodule.instIdemCommSemiring
   IdemCommSemiring.toCommSemiring CommSemiring.toCommMonoid
 
 set_option quotPrecheck false
@@ -80,7 +80,7 @@ lemma div_zeta_sub_one_sub (η₁ η₂) (hη : η₁ ≠ η₂) :
     ring
   apply Associated.mul_left
   apply hζ.unit'_coe.associated_sub_one hpri.out η₁.prop η₂.prop
-  rw [Ne.def, ← Subtype.ext_iff.not]
+  rw [Ne, ← Subtype.ext_iff.not]
   exact hη
 
 set_option synthInstance.maxHeartbeats 40000 in
@@ -98,7 +98,7 @@ lemma div_zeta_sub_one_Injective :
 instance : Finite (𝓞 K ⧸ 𝔭) := by
   haveI : Fact (Nat.Prime p) := hpri
   letI := IsCyclotomicExtension.numberField {p} ℚ K
-  rw [← Ideal.absNorm_ne_zero_iff, Ne.def, Ideal.absNorm_eq_zero_iff, Ideal.span_singleton_eq_bot]
+  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
 
 lemma div_zeta_sub_one_Bijective :
@@ -155,14 +155,14 @@ lemma m_mul_c_mul_p : 𝔪 * 𝔠 η * 𝔭 = 𝔦 η := by
 
 set_option synthInstance.maxHeartbeats 40000 in
 lemma m_ne_zero : 𝔪 ≠ 0 := by
-  simp_rw [Ne.def, gcd_eq_zero_iff, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
+  simp_rw [Ne, gcd_eq_zero_iff, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
   rintro ⟨rfl, rfl⟩
   exact hy (dvd_zero _)
 
 set_option synthInstance.maxHeartbeats 40000 in
 lemma p_ne_zero : 𝔭 ≠ 0 := by
   letI := IsCyclotomicExtension.numberField {p} ℚ K
-  rw [Ne.def, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
+  rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
   exact hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt
 
 lemma coprime_c_aux (η₁ η₂ : nthRootsFinset p (𝓞 K)) (hη : η₁ ≠ η₂) : (𝔦 η₁) ⊔ (𝔦 η₂) ∣ 𝔪 * 𝔭 := by
@@ -232,7 +232,7 @@ lemma prod_c : ∏ η in Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = (
 
 lemma exists_ideal_pow_eq_c : ∃ I : Ideal (𝓞 K), (𝔠 η) = I ^ (p : ℕ) := by
   letI inst1 : @IsDomain (Ideal (𝓞 K)) CommSemiring.toSemiring := @Ideal.isDomain (𝓞 K) _ _
-  letI inst2 := @Ideal.instNormalizedGCDMonoidIdealToSemiringToCommSemiringCancelCommMonoidWithZero (𝓞 K) _ _
+  letI inst2 := @Ideal.instNormalizedGCDMonoid (𝓞 K) _ _
   letI inst3 := @NormalizedGCDMonoid.toGCDMonoid _ _ inst2
   exact @Finset.exists_eq_pow_of_mul_eq_pow_of_coprime (nthRootsFinset p (𝓞 K)) (Ideal (𝓞 K)) _
     (by convert inst1) (by convert inst3) _ _ _ _ _
@@ -401,7 +401,7 @@ lemma a_mul_denom_eq_a_zero_mul_num (hη : η ≠ η₀) :
     apply not_p_div_a_zero hp hζ e hy hz
     rw [ha]
     exact dvd_zero _
-  · rw [Ne.def, FractionalIdeal.spanSingleton_eq_zero_iff, ← (algebraMap (𝓞 K) K).map_zero,
+  · rw [Ne, FractionalIdeal.spanSingleton_eq_zero_iff, ← (algebraMap (𝓞 K) K).map_zero,
       (IsFractionRing.injective (𝓞 K) K).eq_iff]
     intro hβ
     apply a_div_a_zero_denom_spec hp hreg hζ e hy hz η hη
@@ -469,20 +469,20 @@ lemma exists_solution :
   have hη₁ : η₁ ≠ η₀ := by
     rw [← Subtype.coe_injective.ne_iff]
     show (η₀ * hζ.unit' : 𝓞 K) ≠ η₀
-    rw [Ne.def, mul_right_eq_self₀, not_or]
+    rw [Ne, mul_right_eq_self₀, not_or]
     exact ⟨hζ.unit'_coe.ne_one hpri.out.one_lt,
       ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩
   have hη₂ : η₂ ≠ η₀ := by
     rw [← Subtype.coe_injective.ne_iff]
     show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀
-    rw [Ne.def, mul_assoc, ← pow_two, mul_right_eq_self₀, not_or]
+    rw [Ne, mul_assoc, ← pow_two, mul_right_eq_self₀, not_or]
     exact ⟨hζ.unit'_coe.pow_ne_one_of_pos_of_lt zero_lt_two
       (hpri.out.two_le.lt_or_eq.resolve_right (PNat.coe_injective.ne hp.symm)),
       ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩
   have hη : η₂ ≠ η₁ := by
     rw [← Subtype.coe_injective.ne_iff]
     show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀ * hζ.unit'
-    rw [Ne.def, mul_right_eq_self₀, not_or]
+    rw [Ne, mul_right_eq_self₀, not_or]
     exact ⟨hζ.unit'_coe.ne_one hpri.out.one_lt,
       mul_ne_zero (ne_zero_of_mem_nthRootsFinset (η₀ : _).prop)
       (hζ.unit'_coe.ne_zero hpri.out.ne_zero)⟩

FltRegular/FltThree/Edwards.lean

@@ -198,7 +198,7 @@ theorem OddPrimeOrFour.factors' {a : ℤ√(-3)} (h2 : a.norm ≠ 1) (hcoprime :
   obtain ⟨u, huvcoprime, huv, huvdvd⟩ := step1_2 hcoprime hpdvd hp hd
   use u
   cases' huv with huv huv <;> [(use q'); (use star q')] <;>
-    simp only [IsCoprime, Zsqrtd.star_re, Zsqrtd.star_im, Ne.def, neg_eq_zero, Zsqrtd.norm_conj] <;>
+    simp only [IsCoprime, Zsqrtd.star_re, Zsqrtd.star_im, Ne, neg_eq_zero, Zsqrtd.norm_conj] <;>
     use hc, hd, hp, huv, huvcoprime <;>
     · rw [huvdvd, lt_mul_iff_one_lt_left (Spts.pos_of_coprime' huvcoprime), ← Zsqrt3.norm_natAbs,
         Nat.one_lt_cast]
@@ -324,7 +324,7 @@ theorem no_conj (s : Multiset (ℤ√(-3))) {p : ℤ√(-3)} (hp : ¬IsUnit p)
     rw [← Int.isUnit_iff_abs_eq]
     apply IsCoprime.isUnit_of_dvd' hcoprime <;> apply dvd_mul_right
   · have : star p ≠ p := by
-      rw [Ne.def, Zsqrtd.ext_iff]
+      rw [Ne, Zsqrtd.ext_iff]
       rintro ⟨-, H⟩
       apply him
       apply eq_zero_of_neg_eq

FltRegular/FltThree/FltThree.lean

@@ -212,7 +212,7 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity :
     by
     intro d hdprime hdleft hdright
     by_contra hne3
-    rw [← Ne.def] at hne3
+    rw [← Ne] at hne3
     apply (Nat.prime_iff_prime_int.mp hdprime).not_unit
     have hne2 : d ≠ 2 := by
       rintro rfl
@@ -457,8 +457,7 @@ theorem descent_gcd1 (a b c p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q)
       simp only [‹¬ Even (3 : ℤ)›, false_or_iff, iff_not_self, parity_simps] at huvodd
     · intro H
       rw [add_eq_zero_iff_eq_neg] at H
-      apply iff_not_self
-      simpa [‹¬ Even (3 : ℤ)›, H, parity_simps] using huvodd
+      simp [‹¬ Even (3 : ℤ)›, H, parity_simps] at huvodd
     · apply Int.gcd1_coprime12 u v <;> assumption
     · apply Int.gcd1_coprime13 u v <;> assumption
     · apply Int.gcd1_coprime23 u v <;> assumption
@@ -627,12 +626,10 @@ theorem descent_gcd3 (a b c p q : ℤ) (hp : p ≠ 0) (hq : q ≠ 0) (hcoprime :
     · exact mul_ne_zero two_ne_zero hv
     · intro H
       rw [sub_eq_zero] at H
-      apply iff_not_self
-      simpa [H, parity_simps] using huvodd
+      simp [H, parity_simps] at huvodd
     · intro H
       rw [add_eq_zero_iff_eq_neg] at H
-      apply iff_not_self
-      simpa [H, parity_simps] using huvodd
+      simp [H, parity_simps] at huvodd
     · exact hsubcoprime
     · exact haddcoprime
     · exact haddsubcoprime

FltRegular/FltThree/Spts.lean

@@ -13,9 +13,9 @@ theorem Zsqrtd.exists {d : ℤ} (a : ℤ√d) (him : a.im ≠ 0) :
   cases' le_or_lt a.re 0 with hre hre
   · use -a
     simp only [hre, him, Zsqrtd.norm_neg, eq_self_iff_true, Zsqrtd.neg_im, Zsqrtd.neg_re,
-      and_self_iff, neg_nonneg, Ne.def, not_false_iff, neg_eq_zero]
+      and_self_iff, neg_nonneg, Ne, not_false_iff, neg_eq_zero]
   · use a
-    simp only [hre.le, him, eq_self_iff_true, and_self_iff, Ne.def, not_false_iff]
+    simp only [hre.le, him, eq_self_iff_true, and_self_iff, Ne, not_false_iff]
 
 -- Edwards p49 step (2')
 theorem factors2 {a : ℤ√(-3)} (heven : Even a.norm) : ∃ b : ℤ√(-3), a.norm = 4 * b.norm :=
@@ -248,7 +248,7 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod
   have hneg1 : 1 ≤ a.norm := by
     rw [← Int.sub_one_lt_iff, sub_self]
     apply lt_of_le_of_ne (Zsqrtd.norm_nonneg (by norm_num) a)
-    rw [Ne.def, eq_comm, Zsqrtd.norm_eq_zero_iff (by norm_num : (-3 : ℤ) < 0)]
+    rw [Ne, eq_comm, Zsqrtd.norm_eq_zero_iff (by norm_num : (-3 : ℤ) < 0)]
     rintro rfl
     rw [Zsqrtd.zero_im, Zsqrtd.zero_re] at hcoprime
     exact not_isCoprime_zero_zero hcoprime
@@ -261,7 +261,7 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod
     refine' ⟨⟨1, 0⟩, _⟩
     norm_num [Zsqrtd.norm_def]
   obtain ⟨c', m, rfl, -, h1, ⟨y, hy, h3⟩⟩ := Zqrtd.factor_div' a hodd h hcoprime hfactor
-  have h4 : c'.norm ≠ 0 := by rwa [Ne.def, Zsqrtd.norm_eq_zero_iff (by norm_num) c']
+  have h4 : c'.norm ≠ 0 := by rwa [Ne, Zsqrtd.norm_eq_zero_iff (by norm_num) c']
   set g := Int.gcd c'.re c'.im with hg
   have hgpos : 0 < g := by rwa [hg, Zsqrtd.gcd_pos_iff]
   obtain ⟨C', HC', HCDcoprime⟩ := Zsqrtd.exists_coprime_of_gcd_pos hgpos

FltRegular/MayAssume/Lemmas.lean

@@ -88,7 +88,7 @@ theorem a_not_cong_b {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp5 : 5 ≤ p) (h
         · simp only [mem_insert, mem_singleton] at hx
           rcases hx with (H | H | H) <;> simp [H]
     rw [this]
-    simp only [gcd_insert, id.def, gcd_singleton, normalize_apply, neg_mul]
+    simp only [gcd_insert, id, gcd_singleton, normalize_apply, neg_mul]
     congr 1
     rw [← coe_gcd, ← coe_gcd, Int.gcd_eq_natAbs, Int.gcd_eq_natAbs]
     simp only [natAbs_neg, Nat.cast_inj]

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -291,7 +291,7 @@ lemma fltIdeals_coprime2_lemma [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {x y : ℤ}
   rw [← eq_top_iff_one] at hone
   have hcontra := IsPrime.ne_top hPrime
   rw [hone] at hcontra
-  simp only [Ne.def, eq_self_iff_true, not_true] at hcontra
+  simp only [Ne, eq_self_iff_true, not_true] at hcontra
   apply HC hprime3
   apply HC hprime2
 
@@ -349,9 +349,9 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L}
   set b := hζ'.integralPowerBasis' with hb
   have hdim : b.dim = (p : ℕ).pred := by rw [hζ'.power_basis_int'_dim, totient_prime hp.out,
     pred_eq_sub_one]
-  by_cases H : i = ⟨(p : ℕ).pred, pred_lt hp.out.ne_zero⟩
+  by_cases H : i = ⟨(p : ℕ) - 1, pred_lt hp.out.ne_zero⟩
   · simp [H.symm, Hi]
-  have hi : ↑i < (p : ℕ).pred := by
+  have hi : ↑i < (p : ℕ) - 1 := by
     by_contra! habs
     simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt i))] at H
   obtain ⟨y, hy⟩ := hdiv
@@ -383,7 +383,8 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L}
   rw [hn] at hy
   simp only [Fin.castIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Hi, zero_sub,
     neg_eq_iff_eq_neg] at hy
-  simp [hy, dvd_neg]
+  erw [hy] -- pred vs - 1
+  simp [dvd_neg]
 
 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 : ℕ)) :
@@ -401,9 +402,9 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri
     pred_eq_sub_one]
   have last_dvd := dvd_last_coeff_cycl_integer hζ hf hdiv
   intro j
-  by_cases H : j = ⟨(p : ℕ).pred, pred_lt hp.ne_zero⟩
+  by_cases H : j = ⟨(p : ℕ) - 1, pred_lt hp.ne_zero⟩
   · simpa [H] using last_dvd
-  have hj : ↑j < (p : ℕ).pred := by
+  have hj : ↑j < (p : ℕ) - 1 := by
     by_contra! habs
     simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt j))] at H
   obtain ⟨y, hy⟩ := hdiv

FltRegular/NumberTheory/Cyclotomic/Factoring.lean

@@ -36,7 +36,7 @@ theorem pow_sub_pow_eq_prod_sub_zeta_runity_mul {K : Type _} [CommRing K] [IsDom
   -- the homogenization of the identity is also true
   have := congr_arg (homogenization 1) this
   -- simplify to get the result we want
-  simpa [homogenization_prod, algebraMap_eq, hpos]
+  simpa [homogenization_prod, Polynomial.algebraMap_eq, hpos]
 
 /-- If there is a primitive `n`th root of unity in `K` and `n` is odd, then
 `X ^ n + Y ^ n = ∏ (X + μ Y)`, where `μ` varies over the `n`-th roots of unity. -/

FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean

@@ -1,6 +1,6 @@
 import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits
 import Mathlib.NumberTheory.Cyclotomic.Gal
-import Mathlib.NumberTheory.NumberField.Units
+import Mathlib.NumberTheory.NumberField.Units.Basic
 
 universe u
 

FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean

@@ -24,7 +24,7 @@ lemma IsPrimitiveRoot.prime_span_sub_one : Prime (Ideal.span <| singleton <| (h
   rw [Ideal.prime_iff_isPrime,
     Ideal.span_singleton_prime (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)]
   exact hζ.zeta_sub_one_prime'
-  · rw [Ne.def, Ideal.span_singleton_eq_bot]
+  · rw [Ne, Ideal.span_singleton_eq_bot]
     exact hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt
 
 lemma norm_Int_zeta_sub_one : Algebra.norm ℤ (↑(IsPrimitiveRoot.unit' hζ) - 1 : 𝓞 K) = p := by