bump

FltRegular/CaseI/AuxLemmas.lean

@@ -16,7 +16,6 @@ local notation "K" => CyclotomicField P ℚ
 
 local notation "R" => 𝓞 K
 
-
 namespace CaseI
 
 theorem two_lt (hp5 : 5 ≤ p) : 2 < p := by linarith
@@ -188,8 +187,9 @@ theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
       rwa [this]
     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]
+    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]
     ring
   rw [sum_range] at key
   refine caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right ?_ _) _)

FltRegular/CaseII/AuxLemmas.lean

@@ -138,7 +138,8 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD
     {x : R} (hx : Prime x) (I J : Ideal R)
     (hI : ¬ (Ideal.span <| singleton x) ∣ I) (hJ : ¬ (Ideal.span <| singleton x) ∣ J)
     (h : Submodule.IsPrincipal ((I / J : FractionalIdeal R⁰ K) : Submodule R K)) :
-    ∃ a b : R, ¬(x ∣ a) ∧ ¬(x ∣ b) ∧ spanSingleton R⁰ (algebraMap R K a / algebraMap R K b) = I / J := by
+    ∃ 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, coeIdeal_inj]; rintro rfl; exact hI (dvd_zero _)

FltRegular/CaseII/InductionStep.lean

@@ -5,21 +5,14 @@ import FltRegular.NumberTheory.Cyclotomic.Factoring
 open scoped BigOperators nonZeroDivisors NumberField
 open Polynomial
 
-variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K]
-variable (hp : p ≠ 2) [Fintype (ClassGroup (𝓞 K))] (hreg : (p : ℕ).Coprime <| Fintype.card <| ClassGroup (𝓞 K))
+variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [NumberField K]
+  [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup (𝓞 K))]
+  (hreg : (p : ℕ).Coprime <| Fintype.card <| ClassGroup (𝓞 K))
 
-variable {ζ : K} (hζ : IsPrimitiveRoot ζ p)
+variable {ζ : K} (hζ : IsPrimitiveRoot ζ p) {x y z : 𝓞 K} {ε : (𝓞 K)ˣ}
 
-variable {x y z : 𝓞 K} {ε : (𝓞 K)ˣ}
-
-attribute [local instance 2000] Algebra.toModule Module.toDistribMulAction AddMonoid.toZero
-  DistribMulAction.toMulAction MulAction.toSMul NumberField.inst_ringOfIntegersAlgebra
-  Ideal.Quotient.commRing CommRing.toRing Ring.toSemiring
-  Semiring.toNonUnitalSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring
-  NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocSemiring.toMulZeroClass
-  MulZeroClass.toMul Submodule.idemSemiring IdemSemiring.toSemiring
-  Submodule.instIdemCommSemiring
-  IdemCommSemiring.toCommSemiring CommSemiring.toCommMonoid
+attribute [local instance 2000] CommRing.toRing Semiring.toNonUnitalSemiring
+  NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid
 
 set_option quotPrecheck false
 local notation3 "π" => Units.val (IsPrimitiveRoot.unit' hζ) - 1
@@ -313,8 +306,9 @@ lemma p_pow_dvd_c_eta_zero_aux [DecidableEq (𝓞 K)] :
 /- all the powers of 𝔭 have to be in 𝔠 η₀-/
 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]
+  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]
   apply dvd_mul_of_dvd_right
   rw [pow_mul]
 
@@ -553,7 +547,8 @@ lemma exists_solution' :
       add_comm _ (p - 1 : ℕ), pow_add, mul_assoc] at e'
     apply_fun Ideal.Quotient.mk (Ideal.span <| singleton (p : 𝓞 K)) at e'
     rw [map_mul, (Ideal.Quotient.eq_zero_iff_dvd _ _).mpr
-      (associated_zeta_sub_one_pow_prime hζ).symm.dvd, zero_mul, Ideal.Quotient.eq_zero_iff_dvd] at e'
+      (associated_zeta_sub_one_pow_prime hζ).symm.dvd, zero_mul,
+      Ideal.Quotient.eq_zero_iff_dvd] at e'
     obtain ⟨a, ha⟩ := exists_solution'_aux hp hζ hx' e'
     obtain ⟨b, hb⟩ := exists_dvd_pow_sub_Int_pow hp a
     have := dvd_add ha hb

FltRegular/CaseII/Statement.lean

@@ -3,8 +3,9 @@ import FltRegular.CaseII.InductionStep
 open scoped BigOperators nonZeroDivisors NumberField
 open Polynomial
 
-variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K]
-variable (hp : p ≠ 2) [Fintype (ClassGroup (𝓞 K))] (hreg : (p : ℕ).Coprime <| Fintype.card <| ClassGroup (𝓞 K))
+variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [NumberField K]
+  [IsCyclotomicExtension {p} ℚ K]  (hp : p ≠ 2) [Fintype (ClassGroup (𝓞 K))]
+  (hreg : (p : ℕ).Coprime <| Fintype.card <| ClassGroup (𝓞 K))
 
 variable {ζ : K} (hζ : IsPrimitiveRoot ζ p)
 
@@ -42,8 +43,8 @@ lemma not_exists_solution' :
   refine not_exists_solution hp hreg hζ hm ⟨x, y, z, 1, hy, hz'', ?_⟩
   rwa [Units.val_one, one_mul]
 
-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
+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 : Fact (PNat.Prime ⟨p, hpri.out.pos⟩) := hpri
   haveI := CyclotomicField.isCyclotomicExtension ⟨p, hpri.out.pos⟩ ℚ
   obtain ⟨ζ, hζ⟩ := IsCyclotomicExtension.exists_prim_root
@@ -61,8 +62,9 @@ lemma not_exists_Int_solution {p : ℕ} [hpri : Fact (Nat.Prime p)] (hreg : IsRe
   · dsimp
     simp_rw [← Int.cast_pow, ← Int.cast_add, e]
 
-lemma not_exists_Int_solution' {p : ℕ} [hpri : Fact (Nat.Prime p)] (hreg : IsRegularPrime p) (hodd : p ≠ 2) :
-  ¬∃ (x y z : ℤ), ({x, y, z} : Finset ℤ).gcd id = 1 ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p := by
+lemma not_exists_Int_solution' {p : ℕ} [hpri : Fact (Nat.Prime p)] (hreg : IsRegularPrime p)
+    (hodd : p ≠ 2) :
+    ¬∃ (x y z : ℤ), ({x, y, z} : Finset ℤ).gcd id = 1 ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p := by
   rintro ⟨x, y, z, hgcd, hz, hz', e⟩
   refine not_exists_Int_solution hreg hodd ⟨x, y, z, ?_, hz, hz', e⟩
   intro hy

FltRegular/NumberTheory/AuxLemmas.lean

@@ -215,8 +215,8 @@ lemma Polynomial.irreducible_taylor_iff {R} [CommRing R] {r} {p : R[X]} :
 -- Generalizes (and should follow) `Separable.map`
 open Polynomial in
 attribute [local instance] Ideal.Quotient.field in
-lemma Polynomial.separable_map' {R S} [Field R] [CommRing S] [Nontrivial S] (f : R →+* S) (p : R[X]) :
-    (p.map f).Separable ↔ p.Separable :=  by
+lemma Polynomial.separable_map' {R S} [Field R] [CommRing S] [Nontrivial S] (f : R →+* S)
+    (p : R[X]) : (p.map f).Separable ↔ p.Separable :=  by
   refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩
   obtain ⟨m, hm⟩ := Ideal.exists_maximal S
   have := Separable.map H (f := Ideal.Quotient.mk m)

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -22,8 +22,6 @@ instance {K : Type*} [Field K] : Module (𝓞 K) (𝓞 K) := Semiring.toModule
 
 open Ideal IsCyclotomicExtension
 
--- TODO can we make a relative version of this with another base ring instead of ℤ ?
--- A version of flt_facts_3 indep of the ring
 theorem exists_int_sub_pow_prime_dvd {A : Type _} [CommRing A] [IsCyclotomicExtension {p} ℤ A]
     [hp : Fact (p : ℕ).Prime] (a : A) : ∃ m : ℤ, a ^ (p : ℕ) - m ∈ span ({(p : A)} : Set A) := by
   have : a ∈ Algebra.adjoin ℤ _ := @adjoin_roots {p} ℤ A _ _ _ _ a
@@ -346,7 +344,8 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L}
     by_contra! habs
     simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt i))] at H
   obtain ⟨y, hy⟩ := hdiv
-  rw [← Equiv.sum_comp (Fin.castOrderIso (succ_pred_prime hp.out)).toEquiv, Fin.sum_univ_castSucc] at hy
+  rw [← Equiv.sum_comp (Fin.castOrderIso (succ_pred_prime hp.out)).toEquiv,
+    Fin.sum_univ_castSucc] at hy
   simp only [hlast, h, RelIso.coe_fn_toEquiv, Fin.val_mk] at hy
   rw [hζ.pow_sub_one_eq hp.out.one_lt, ← sum_neg_distrib, smul_sum, sum_range, ← sum_add_distrib,
     ← (Fin.castOrderIso hdim).toEquiv.sum_comp] at hy

FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean

@@ -141,11 +141,13 @@ theorem IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one {p i j : ℕ} {ζ : A}
 end CyclotomicUnit
 
 lemma IsPrimitiveRoot.associated_sub_one {A : Type*} [CommRing A] [IsDomain A]
-    {p : ℕ} (hp : p.Prime) {ζ : A} (hζ : IsPrimitiveRoot ζ p) {η₁ : A} (hη₁ : η₁ ∈ nthRootsFinset p A)
-    {η₂ : A} (hη₂ : η₂ ∈ nthRootsFinset p A) (e : η₁ ≠ η₂) :
+    {p : ℕ} (hp : p.Prime) {ζ : A} (hζ : IsPrimitiveRoot ζ p) {η₁ : A}
+    (hη₁ : η₁ ∈ nthRootsFinset p A) {η₂ : A} (hη₂ : η₂ ∈ nthRootsFinset p A) (e : η₁ ≠ η₂) :
     Associated (ζ - 1) (η₁ - η₂) := by
-  obtain ⟨i, ⟨hi, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos).1 hη₁) hp.pos
-  obtain ⟨j, ⟨hj, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos).1 hη₂) hp.pos
+  obtain ⟨i, ⟨hi, rfl⟩⟩ :=
+    hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos).1 hη₁) hp.pos
+  obtain ⟨j, ⟨hj, rfl⟩⟩ :=
+    hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos).1 hη₂) hp.pos
   have : i ≠ j := ne_of_apply_ne _ e
   obtain ⟨u, h⟩ := CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one A
     hp.two_le hp hi hj this hζ

FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean

@@ -4,7 +4,8 @@ import FltRegular.NumberTheory.Cyclotomic.CyclRat
 import Mathlib.RingTheory.Ideal.Norm
 import Mathlib.RingTheory.NormTrace
 
-variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K]
+variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [CharZero K]
+  [IsCyclotomicExtension {p} ℚ K]
 
 variable {ζ : K} (hζ : IsPrimitiveRoot ζ p)
 
@@ -13,12 +14,13 @@ open Polynomial
 
 variable (hp : p ≠ 2)
 
-lemma IsPrimitiveRoot.prime_span_sub_one : Prime (Ideal.span <| singleton <| (hζ.unit' - 1 : 𝓞 K)) := by
+lemma IsPrimitiveRoot.prime_span_sub_one :
+    Prime (Ideal.span <| singleton <| (hζ.unit' - 1 : 𝓞 K)) := by
   haveI : Fact (Nat.Prime p) := hpri
   letI := IsCyclotomicExtension.numberField {p} ℚ K
   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'
+  · exact hζ.zeta_sub_one_prime'
   · rw [Ne, Ideal.span_singleton_eq_bot]
     exact hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt
 
@@ -92,8 +94,8 @@ lemma zeta_sub_one_dvd_Int_iff {n : ℤ} : (hζ.unit' : 𝓞 K) - 1 ∣ n ↔ 
     exact hpri.1
 
 lemma IsPrimitiveRoot.sub_one_dvd_sub {A : Type*} [CommRing A] [IsDomain A]
-    {p : ℕ} (hp : p.Prime) {ζ : A} (hζ : IsPrimitiveRoot ζ p) {η₁ : A} (hη₁ : η₁ ∈ nthRootsFinset p A)
-    {η₂ : A} (hη₂ : η₂ ∈ nthRootsFinset p A) :
+    {p : ℕ} (hp : p.Prime) {ζ : A} (hζ : IsPrimitiveRoot ζ p) {η₁ : A}
+    (hη₁ : η₁ ∈ nthRootsFinset p A) {η₂ : A} (hη₂ : η₂ ∈ nthRootsFinset p A) :
     ζ - 1 ∣ η₁ - η₂ := by
   by_cases h : η₁ = η₂
   · rw [h, sub_self]; exact dvd_zero _

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -288,8 +288,8 @@ lemma map_two {S T F: Type*} [NonAssocSemiring S] [NonAssocSemiring T] [FunLike
   rw [← one_add_one_eq_two, map_add, map_one]
   exact one_add_one_eq_two
 
-lemma neg_one_eq_one_iff_two_eq_zero {M : Type*} [AddGroupWithOne M] : (-1 : M) = 1 ↔ (2 : M) = 0 := by
-  rw [neg_eq_iff_add_eq_zero, one_add_one_eq_two]
+lemma neg_one_eq_one_iff_two_eq_zero {M : Type*} [AddGroupWithOne M] :
+    (-1 : M) = 1 ↔ (2 : M) = 0 := by rw [neg_eq_iff_add_eq_zero, one_add_one_eq_two]
 
 lemma Units.coe_map_inv' {M N F : Type*} [Monoid M] [Monoid N] [FunLike F M N]
     [MonoidHomClass F M N] (f : F) (m : Mˣ) :
@@ -316,7 +316,6 @@ lemma unit_inv_conj_not_neg_zeta_runity_aux (u : Rˣ) (hp : (p : ℕ).Prime) :
     ext x
     congr 1
     rw [map_zsmul]
-      -- todo: probably swap `is_primitive_root.inv` and `is_primitive_root.inv'`.
   have : ∀ x : Fin φn, intGal ((galConj K p)) (⟨ζ, hζ.isIntegral p.pos⟩ ^ (x : ℕ)) =
       ⟨ζ⁻¹, hζ.inv.isIntegral p.pos⟩ ^ (x : ℕ) := by
     intro x

FltRegular/NumberTheory/Different.lean

@@ -20,7 +20,7 @@ import Mathlib.NumberTheory.KummerDedekind
 -/
 universe u
 
-attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
+attribute [local instance] FractionRing.liftAlgebra
 
 variable (A K L B) [CommRing A] [Field K] [CommRing B] [Field L]
 variable [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L]

FltRegular/NumberTheory/Finrank.lean

@@ -41,7 +41,8 @@ lemma FiniteDimensional.finrank_add_finrank_quotient_le (N : Submodule R M) :
   obtain ⟨s, hs, hs'⟩ := exists_finset_card_eq_finrank_and_linearIndependent R N
   obtain ⟨t, ht, ht'⟩ := exists_finset_card_eq_finrank_and_linearIndependent R (M ⧸ N)
   obtain ⟨f, hf⟩ := N.mkQ_surjective.hasRightInverse
-  have H : Disjoint (Submodule.span R (Subtype.val '' (s : Set N))) (Submodule.span R (f '' t)) := by
+  have H :
+      Disjoint (Submodule.span R (Subtype.val '' (s : Set N))) (Submodule.span R (f '' t)) := by
     apply Disjoint.mono_left (Submodule.span_le.mpr Set.image_val_subset)
     rw [disjoint_iff, eq_bot_iff, ← @Subtype.range_val (M ⧸ N) t, ← Set.range_comp,
       ← Finsupp.range_total]

FltRegular/NumberTheory/Hilbert90.lean

@@ -127,7 +127,8 @@ lemma Hilbert90 : ∃ ε : L, η = ε / σ ε := by
   simp only [map_inv₀, div_inv_eq_mul]
   specialize hε σ
   nth_rewrite 2 [← inv_inv ε] at hε
-  rw [div_inv_eq_mul, cocycle_spec hσ hη hone, mul_inv_eq_iff_eq_mul, mul_comm, ← Units.eq_iff] at hε
+  rw [div_inv_eq_mul, cocycle_spec hσ hη hone, mul_inv_eq_iff_eq_mul, mul_comm,
+    ← Units.eq_iff] at hε
   simp only [AlgEquiv.smul_units_def, Units.coe_map, MonoidHom.coe_coe, Units.val_mul] at hε
   symm
   rw [inv_mul_eq_iff_eq_mul₀ ε.ne_zero, hε]

FltRegular/NumberTheory/Hilbert92.lean

@@ -23,7 +23,6 @@ variable
   (σ : H) (hσ : Subgroup.zpowers σ = ⊤) (r : ℕ)
   [DistribMulAction H G] [Module.Free ℤ G] [Module.Finite ℤ G] (hf : finrank ℤ G = r * (p - 1))
 
--- TODO maybe abbrev
 local notation3 "A" => CyclotomicIntegers p
 
 abbrev systemOfUnits.IsMaximal {r} {p : ℕ+} {G} [AddCommGroup G] [Module (CyclotomicIntegers p) G]
@@ -167,7 +166,8 @@ lemma lemma2 [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental) (i :
   have hS' : S'.units ∘ Fin.succAbove i = S.units ∘ Fin.succAbove i := by
     ext; simp only [Function.comp_apply, ne_eq, Fin.succAbove_ne, not_false_eq_true,
       Function.update_noteq]
-  have ha' : Finsupp.total _ G A (S'.units ∘ Fin.succAbove i) a' + S.units i = (1 - zeta p) • g := by
+  have ha' :
+      Finsupp.total _ G A (S'.units ∘ Fin.succAbove i) a' + S.units i = (1 - zeta p) • g := by
     rw [hS', Finsupp.total_comp, LinearMap.comp_apply, Finsupp.lmapDomain_apply,
       ← one_smul A (S.units i), hg, ← ha, ← Finsupp.total_single, ← map_add]
     congr 1
@@ -242,10 +242,6 @@ def RelativeUnits (k K : Type*) [Field k] [Field K] [Algebra k K] :=
 
 instance : CommGroup (RelativeUnits k K) := by delta RelativeUnits; infer_instance
 
-attribute [local instance] IsCyclic.commGroup
-
-attribute [local instance 2000] inst_ringOfIntegersAlgebra Algebra.toSMul Algebra.toModule
-
 instance : IsScalarTower (𝓞 k) (𝓞 K) K := IsScalarTower.of_algebraMap_eq (fun _ ↦ rfl)
 
 instance : IsIntegralClosure (𝓞 K) (𝓞 k) K := by
@@ -277,7 +273,7 @@ def relativeUnitsMapHom : (K →ₐ[k] K) →* (Monoid.End (RelativeUnits k K))
     refine DFunLike.ext _ _ (fun x ↦ ?_)
     obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
     rw [relativeUnitsMap]
-    erw [QuotientGroup.lift_mk'] -- why?
+    erw [QuotientGroup.lift_mk']
     simp only [map_one, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
       Monoid.coe_one, id_eq]
     rfl
@@ -398,15 +394,13 @@ lemma NumberField.Units.finrank_eq : finrank ℤ (Additive (𝓞 k)ˣ) = NumberF
   rw [← Submodule.torsion_int]
   exact (FiniteDimensional.finrank_quotient_of_le_torsion _ le_rfl).symm
 
-local instance : Module.Finite ℤ (Additive <| RelativeUnits k K) := by
-  delta RelativeUnits
-  show Module.Finite ℤ (Additive (𝓞 K)ˣ ⧸ AddSubgroup.toIntSubmodule (Subgroup.toAddSubgroup
-    (MonoidHom.range <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K)))))
-  infer_instance
+local instance : Module.Finite ℤ (Additive <| RelativeUnits k K) :=
+  inferInstanceAs
+    (Module.Finite ℤ (Additive (𝓞 K)ˣ ⧸ AddSubgroup.toIntSubmodule (Subgroup.toAddSubgroup
+    (MonoidHom.range <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K))))))
 
-local instance : Module.Finite ℤ (Additive <| relativeUnitsWithGenerator p hp hKL σ hσ) := by
-  delta relativeUnitsWithGenerator
-  infer_instance
+local instance : Module.Finite ℤ (Additive <| relativeUnitsWithGenerator p hp hKL σ hσ) :=
+  inferInstanceAs (Module.Finite ℤ (Additive (RelativeUnits k K)))
 
 local instance : Module.Finite ℤ G := Module.Finite.of_surjective
   (M := Additive (relativeUnitsWithGenerator p hp hKL σ hσ))

FltRegular/NumberTheory/Hilbert94.lean

@@ -13,7 +13,7 @@ variable [Fintype (ClassGroup (𝓞 K))]
 open Polynomial
 
 variable {L} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
-variable (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (hKL : FiniteDimensional.finrank K L = p)
+  (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (hKL : FiniteDimensional.finrank K L = p)
 
 variable {A B} [CommRing A] [CommRing B] [Algebra A B] [Algebra A L] [Algebra A K]
     [Algebra B L] [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K]
@@ -69,10 +69,6 @@ theorem exists_not_isPrincipal_and_isPrincipal_map_aux
   · rw [hβ']
     exact ⟨⟨_, rfl⟩⟩
 
-attribute [local instance 2000] NumberField.inst_ringOfIntegersAlgebra Algebra.toSMul Algebra.toModule
-
-attribute [local instance] FractionRing.liftAlgebra
-
 open FiniteDimensional (finrank)
 
 theorem Ideal.isPrincipal_pow_finrank_of_isPrincipal_map [IsDedekindDomain A] (I : Ideal A)