-- Mathlib/NumberTheory/Cyclotomic/Gal.lean
theorem fromZetaAut_spec : fromZetaAut hμ h (zeta n K L) = μ

Proof state:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic (↑n) K)
⊢ (fromZetaAut hμ h) (zeta n K L) = μ

Tactic:
simp_rw [fromZetaAut, autEquivPow_symm_apply]

Result:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic (↑n) K)
⊢ ((IsPrimitiveRoot.powerBasis K ⋯).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) (zeta n K L) = μ

Proof state:
case h.e'_2.h.e'_6
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic (↑n) K)
hζ : IsPrimitiveRoot (zeta n K L) ↑n
h : ∃ i < ↑n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime ↑n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val = h.choose

Tactic:
exact ZMod.val_cast_of_lt h.choose_spec.1

Result:
no goals

Proof state:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic (↑n) K)
⊢ ((IsPrimitiveRoot.powerBasis K ⋯).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) (zeta n K L) = μ

Tactic:
generalize_proofs hζ h _ hμ _

Result:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic (↑n) K)
hζ : IsPrimitiveRoot (zeta n K L) ↑n
h : ∃ i < ↑n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime ↑n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K hμ) pf✝) (zeta n K L) = μ

Proof state:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic (↑n) K)
hζ : IsPrimitiveRoot (zeta n K L) ↑n
h : ∃ i < ↑n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime ↑n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K hμ) pf✝)
      (IsPrimitiveRoot.powerBasis K hζ).gen =
    μ

Tactic:
rw [PowerBasis.equivOfMinpoly_gen, hμ.powerBasis_gen K]

Result:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic (↑n) K)
hζ : IsPrimitiveRoot (zeta n K L) ↑n
h : ∃ i < ↑n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime ↑n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val = μ

Proof state:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic (↑n) K)
hζ : IsPrimitiveRoot (zeta n K L) ↑n
h : ∃ i < ↑n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime ↑n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K hμ) pf✝) (zeta n K L) = μ

Tactic:
nth_rewrite 4 [← hζ.powerBasis_gen K]

Result:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic (↑n) K)
hζ : IsPrimitiveRoot (zeta n K L) ↑n
h : ∃ i < ↑n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime ↑n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K hμ) pf✝)
      (IsPrimitiveRoot.powerBasis K hζ).gen =
    μ

Proof state:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic (↑n) K)
hζ : IsPrimitiveRoot (zeta n K L) ↑n
h : ∃ i < ↑n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime ↑n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val = μ

Tactic:
convert h.choose_spec.2

Result:
case h.e'_2.h.e'_6
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic (↑n) K)
hζ : IsPrimitiveRoot (zeta n K L) ↑n
h : ∃ i < ↑n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime ↑n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val = h.choose