awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
h : HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ (p ^ HAdd.hAdd (α := ℕ) 0 1) / 2)
h₁ :
  HPow.hPow (α := K) (↑p : K) (p - 2) =
    HPow.hPow (α := K) (↑p : K) (HPow.hPow (β := ℕ) p 0 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))
⊢ discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim) → L) =
    HPow.hPow (α := K) (-1) ((p - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p - 2)

Tactic:
convert! discr_prime_pow_ne_two hζ' (by simpa [hirr]) (by simp [hodd]) using 2

Premises used: IsCyclotomicExtension.discr_prime_pow_ne_two
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
h : HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ (HPow.hPow (β := ℕ) p 1) / 2)
h₁ : HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ p / 2)
h₂ h₃ : HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) ((p - 1) / 2)
⊢ HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ (p ^ HAdd.hAdd (α := ℕ) 0 1) / 2)

Tactic:
rw [zero_add, pow_one, totient_prime hp.out]

Premises used: Nat.totient_prime, zero_add, pow_one, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
h : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) (1 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))
h₁ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1)
h₂ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) ((p - 1) * 1 - 1)
h₃ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) (p - 1 - 1)
h₄ h₅ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) (p - HAdd.hAdd (α := ℕ) 1 1)
⊢ HPow.hPow (α := K) (↑p : K) (p - 2) =
    HPow.hPow (α := K) (↑p : K) (HPow.hPow (β := ℕ) p 0 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))

Tactic:
rw [_root_.pow_zero, one_mul, zero_add, mul_one, Nat.sub_sub]

Premises used: Nat.sub_sub, zero_add, pow_zero, mul_one, one_mul
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
h :
  Eq (α := L) (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
⊢ (↑f : L →ₐ[K] L) = (↑g : L →ₐ[K] L)

Tactic:
apply (hμ.powerBasis K).algHom_ext

Premises used: IsPrimitiveRoot.powerBasis, PowerBasis.algHom_ext
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
h :
  Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
h₁ :
  Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    ((g : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
h₂ : Eq (α := L) ((f : (a : L) → L) μ : L) ((g : (a : L) → L) μ : L)
h₃ :
  (f : (a : L) → L) μ =
    μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g) : ZMod n)
h₄ :
  μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f) : ZMod n) =
    μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g) : ZMod n)
h₅ h₆ :
  μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g) : ZMod n) =
    μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g) : ZMod n)
⊢ Eq (α := L) (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)

Tactic:
rw [AlgEquiv.coe_algHom, AlgEquiv.coe_algHom, powerBasis_gen,
      ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg]

Premises used: IsPrimitiveRoot.powerBasis_gen, AlgEquiv.coe_algHom, IsPrimitiveRoot.autToPow_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
⊢ (↑f : L →ₐ[K] L) = (↑g : L →ₐ[K] L)

Tactic:
have : f.toAlgHom = g.toAlgHom := by
    apply (hμ.powerBasis K).algHom_ext
    rw [AlgEquiv.coe_algHom, AlgEquiv.coe_algHom, powerBasis_gen,
      ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg]
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
this : (↑f : L →ₐ[K] L) = (↑g : L →ₐ[K] L)
⊢ f = g

Tactic:
AlgEquiv.coe_algHom_injective this

Premises used: AlgEquiv.coe_algHom_injective
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
this : (↑f : L →ₐ[K] L) = (↑g : L →ₐ[K] L)
⊢ f = g

Tactic:
exact AlgEquiv.coe_algHom_injective this

Premises used: AlgEquiv.coe_algHom_injective
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
t : (ZMod n)ˣ
⊢ NeZero.{u_1} (R := K) (↑n : K)

Tactic:
haveI := IsCyclotomicExtension.neZero' n K L
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
t : (ZMod n)ˣ
this : NeZero.{u_1} (R := K) (↑n : K)
simp : Eq (α := K[X]) (minpoly K (zeta n K L)) (minpoly K (zeta n K L ^ (↑t : ZMod n).val))
⊢ Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)))

Tactic:
simp only [IsPrimitiveRoot.powerBasis_gen]

Premises used: IsPrimitiveRoot.powerBasis_gen
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
t : (ZMod n)ˣ
this : NeZero.{u_1} (R := K) (↑n : K)
⊢ Eq (α := K[X]) (cyclotomic n K) (minpoly K (zeta n K L ^ (↑t : ZMod n).val))

Tactic:
have hr :=
            IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible
              ((zeta_spec n K L).pow_of_coprime _ (ZMod.val_coe_unit_coprime t)) h
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
t : (ZMod n)ˣ
this : NeZero.{u_1} (R := K) (↑n : K)
hr : Eq (α := K[X]) (cyclotomic n K) (minpoly K (zeta n K L ^ (↑t : ZMod n).val))
⊢ Eq (α := K[X]) (minpoly K (zeta n K L)) (minpoly K (zeta n K L ^ (↑t : ZMod n).val))

Tactic:
((zeta_spec n K L).minpoly_eq_cyclotomic_of_irreducible h).symm.trans hr

Premises used: IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible, IsCyclotomicExtension.zeta_spec, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
t : (ZMod n)ˣ
this : NeZero.{u_1} (R := K) (↑n : K)
hr : Eq (α := K[X]) (cyclotomic n K) (minpoly K (zeta n K L ^ (↑t : ZMod n).val))
⊢ Eq (α := K[X]) (minpoly K (zeta n K L)) (minpoly K (zeta n K L ^ (↑t : ZMod n).val))

Tactic:
exact ((zeta_spec n K L).minpoly_eq_cyclotomic_of_irreducible h).symm.trans hr

Premises used: IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible, IsCyclotomicExtension.zeta_spec, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
f : L ≃ₐ[K] L
simp :
  PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
      (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
        zeta n K L ^
          ZMod.val (n := n)
            (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                    (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                  f) :
              ZMod n))
        ⋯)
      ⋯ =
    f
⊢ (fun (t : (ZMod n)ˣ) ↦
        (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) ⋯ : L ≃ₐ[K] L))
      (OneHom.toFun (↑(IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯) : OneHom (L ≃ₐ[K] L) (ZMod n)ˣ) f) =
    f

Tactic:
simp only [MonoidHom.toFun_eq_coe]

Premises used: MonoidHom.toFun_eq_coe
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
f : L ≃ₐ[K] L
a :
  (↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
            zeta n K L ^
              ZMod.val (n := n)
                (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                        (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                      f) :
                  ZMod n))
            ⋯)
          ⋯) :
      L →ₐ[K] L) =
    (↑f : L →ₐ[K] L)
⊢ PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
      (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
        zeta n K L ^
          ZMod.val (n := n)
            (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                    (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                  f) :
              ZMod n))
        ⋯)
      ⋯ =
    f

Tactic:
apply AlgEquiv.coe_algHom_injective

Premises used: AlgEquiv.coe_algHom_injective
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
f : L ≃ₐ[K] L
a :
  Eq (α := L)
    (((↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
                (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
                  zeta n K L ^
                    ZMod.val (n := n)
                      (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                              (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                            f) :
                        ZMod n))
                  ⋯)
                ⋯) :
            L →ₐ[K] L) :
          (a : L) → L)
        (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) :
      L)
    (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) : L)
⊢ (↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
            zeta n K L ^
              ZMod.val (n := n)
                (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                        (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                      f) :
                  ZMod n))
            ⋯)
          ⋯) :
      L →ₐ[K] L) =
    (↑f : L →ₐ[K] L)

Tactic:
apply (hζ.powerBasis K).algHom_ext

Premises used: IsPrimitiveRoot.powerBasis, PowerBasis.algHom_ext
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
f : L ≃ₐ[K] L
a :
  Eq (α := L)
    ((PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
            (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
              zeta n K L ^
                ZMod.val (n := n)
                  (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                          (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                        f) :
                    ZMod n))
              ⋯)
            ⋯ :
          (a : L) → L)
        (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) :
      L)
    ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) : L)
⊢ Eq (α := L)
    (((↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
                (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
                  zeta n K L ^
                    ZMod.val (n := n)
                      (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                              (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                            f) :
                        ZMod n))
                  ⋯)
                ⋯) :
            L →ₐ[K] L) :
          (a : L) → L)
        (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) :
      L)
    (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) : L)

Tactic:
simp only [AlgEquiv.coe_algHom]

Premises used: AlgEquiv.coe_algHom
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
f : L ≃ₐ[K] L
a :
  PowerBasis.gen
      (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
        zeta n K L ^
          ZMod.val (n := n)
            (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                    (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                  f) :
              ZMod n))
        ⋯) =
    (f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))
⊢ Eq (α := L)
    ((PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
            (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
              zeta n K L ^
                ZMod.val (n := n)
                  (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                          (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                        f) :
                    ZMod n))
              ⋯)
            ⋯ :
          (a : L) → L)
        (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) :
      L)
    ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) : L)

Tactic:
rw [PowerBasis.equivOfMinpoly_gen]

Premises used: PowerBasis.equivOfMinpoly_gen
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
f : L ≃ₐ[K] L
⊢ PowerBasis.gen
      (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
        zeta n K L ^
          ZMod.val (n := n)
            (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                    (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                  f) :
              ZMod n))
        ⋯) =
    (f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))

Tactic:
simp only [IsPrimitiveRoot.powerBasis_gen, IsPrimitiveRoot.autToPow_spec]

Premises used: IsPrimitiveRoot.powerBasis_gen, IsPrimitiveRoot.autToPow_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
simp :
  ((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) ⋯) =
    x
⊢ OneHom.toFun (M := L ≃ₐ[K] L) (↑(IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯) : OneHom (L ≃ₐ[K] L) (ZMod n)ˣ)
      ((fun (t : (ZMod n)ˣ) ↦
          (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) ⋯ : L ≃ₐ[K] L))
        x) =
    x

Tactic:
simp only [MonoidHom.toFun_eq_coe]

Premises used: MonoidHom.toFun_eq_coe
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
generalize_proofs :
  ∀ (pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n)
    (h :
      Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
        (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))),
    ((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
        (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K pf) h) =
      x
⊢ ((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) ⋯) =
    x

Tactic:
generalize_proofs _ h
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
⊢ zeta n K L ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L)

Tactic:
have key := hζ.autToPow_spec K ((hζ.powerBasis K).equivOfMinpoly ((hμ x).powerBasis K) h)