these are now in mathlib

FltRegular/CaseI/Statement.lean

@@ -7,7 +7,7 @@ import Mathlib.NumberTheory.FLT.Three
 
 open Finset Nat IsCyclotomicExtension Ideal Polynomial Int Basis FltRegular.CaseI
 
-open scoped BigOperators NumberField
+open scoped NumberField
 
 namespace FltRegular
 

FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean

@@ -1,27 +1,17 @@
 import Mathlib.NumberTheory.Cyclotomic.Gal
 import Mathlib.NumberTheory.NumberField.Units.Basic
 
-universe u
-
 open FiniteDimensional
 
 open scoped NumberField
 
-theorem PowerBasis.rat_hom_ext {S S' : Type _} [CommRing S] [hS : Algebra ℚ S] [Ring S']
-    [hS' : Algebra ℚ S'] (pb : PowerBasis ℚ S) ⦃f g : S →+* S'⦄ (h : f pb.gen = g pb.gen) : f = g :=
-  let f' := f.toRatAlgHom
-  let g' := g.toRatAlgHom
-  DFunLike.ext f g <| by
-    convert DFunLike.ext_iff.mp (pb.algHom_ext (show f' pb.gen = g' pb.gen from h))
 
-variable (K : Type _) (p : ℕ+) [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K]
+variable (K : Type*) (p : ℕ+) [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K]
 
 variable {ζ : K} (hζ : IsPrimitiveRoot ζ p)
 
 local notation "RR" => 𝓞 K
 
--- @Chris: you mentioned "checking automorphisms agree only on a generator" -
--- what you want is `power_basis.alg_hom_ext`
 open scoped NumberField Cyclotomic
 
 open IsCyclotomicExtension Polynomial
@@ -37,8 +27,7 @@ variable {K p}
 theorem ZMod.val_neg_one' : ∀ {n : ℕ}, 0 < n → (-1 : ZMod n).val = n - 1
   | _ + 1, _ => ZMod.val_neg_one _
 
-theorem galConj_zeta : galConj K p (zeta p ℚ K) = (zeta p ℚ K)⁻¹ :=
-  by
+theorem galConj_zeta : galConj K p (zeta p ℚ K) = (zeta p ℚ K)⁻¹ := by
   let hζ := zeta_spec p ℚ K
   simp only [galConj, Units.coe_neg_one, autEquivPow_symm_apply, AlgEquiv.coe_algHom,
     PowerBasis.equivOfMinpoly_apply]
@@ -48,8 +37,7 @@ theorem galConj_zeta : galConj K p (zeta p ℚ K) = (zeta p ℚ K)⁻¹ :=
 
 include hζ in
 @[simp]
-theorem galConj_zeta_runity : galConj K p ζ = ζ⁻¹ :=
-  by
+theorem galConj_zeta_runity : galConj K p ζ = ζ⁻¹ := by
   obtain ⟨t, _, rfl⟩ := (zeta_spec p ℚ K).eq_pow_of_pow_eq_one hζ.pow_eq_one p.pos
   rw [map_pow, galConj_zeta, inv_pow]
 
@@ -66,25 +54,21 @@ theorem conj_norm_one (x : ℂ) (h : Complex.abs x = 1) : conj x = x⁻¹ := by
 include hζ in
 @[simp]
 theorem embedding_conj (x : K) (φ : K →+* ℂ) : conj (φ x) = φ (galConj K p x) := by
-  change RingHom.comp conj φ x = (φ.comp <| ↑(galConj K p)) x
+  change RingHom.comp conj φ x = (φ.comp (galConj K p)) x
   revert x
-  suffices φ (galConj K p ζ) = conj (φ ζ)
-    by
-    rw [← funext_iff]
-    rw [DFunLike.coe_fn_eq]
-    apply (hζ.powerBasis ℚ).rat_hom_ext
+  suffices φ (galConj K p ζ) = conj (φ ζ) by
+    rw [← funext_iff, DFunLike.coe_fn_eq, ← ((starRingEnd ℂ).comp φ).toRatAlgHom_toRingHom,
+      ← (φ.comp ↑(galConj K p)).toRatAlgHom_toRingHom (R := K)]
+    congr 1
+    apply (hζ.powerBasis ℚ).algHom_ext
     exact this.symm
   rw [conj_norm_one, galConj_zeta_runity hζ, map_inv₀]
   exact Complex.norm_eq_one_of_pow_eq_one (by rw [← map_pow, hζ.pow_eq_one, map_one]) p.ne_zero
 
 variable (p)
 
---generalize this
-theorem gal_map_mem {x : K} (hx : IsIntegral ℤ x) (σ : K →ₐ[ℚ] K) : IsIntegral ℤ (σ x) :=
-  map_isIntegral_int (σ.restrictScalars ℤ) hx
-
 theorem gal_map_mem_subtype (σ : K →ₐ[ℚ] K) (x : RR) : IsIntegral ℤ (σ x) :=
-  gal_map_mem x.2 _
+  map_isIntegral_int _ x.2
 
 /-- Restriction of `σ : K →ₐ[ℚ] K` to the ring of integers.  -/
 def intGal (σ : K →ₐ[ℚ] K) : RR →ₐ[ℤ] RR :=