[GOAL]
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
⊢ Function.Injective ↑(autToPow K hμ)
[PROOFSTEP]
intro f g hfg
[GOAL]
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
f g : L ≃ₐ[K] L
hfg : ↑(autToPow K hμ) f = ↑(autToPow K hμ) g
⊢ f = g
[PROOFSTEP]
apply_fun Units.val at hfg 
[GOAL]
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
f g : L ≃ₐ[K] L
hfg : ↑(↑(autToPow K hμ) f) = ↑(↑(autToPow K hμ) g)
⊢ f = g
[PROOFSTEP]
simp only [IsPrimitiveRoot.coe_autToPow_apply] at hfg 
[GOAL]
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
f g : L ≃ₐ[K] L
hfg :
  ↑(Exists.choose (_ : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m)) =
    ↑(Exists.choose (_ : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m))
⊢ f = g
[PROOFSTEP]
revert hfg
[GOAL]
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
f g : L ≃ₐ[K] L
⊢ ↑(Exists.choose (_ : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m)) =
      ↑(Exists.choose (_ : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m)) →
    f = g
[PROOFSTEP]
generalize_proofs hf' hg'
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
⊢ ↑(Exists.choose hf') = ↑(Exists.choose hg') → f = g
[PROOFSTEP]
intro hfg
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : ↑(Exists.choose hf') = ↑(Exists.choose hg')
⊢ f = g
[PROOFSTEP]
have hf := hf'.choose_spec
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : ↑(Exists.choose hf') = ↑(Exists.choose hg')
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
⊢ f = g
[PROOFSTEP]
have hg := hg'.choose_spec
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : ↑(Exists.choose hf') = ↑(Exists.choose hg')
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
⊢ f = g
[PROOFSTEP]
revert hf hg
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : ↑(Exists.choose hf') = ↑(Exists.choose hg')
⊢ ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf' →
    ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg' → f = g
[PROOFSTEP]
generalize_proofs hζ
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : ↑(Exists.choose hf') = ↑(Exists.choose hg')
⊢ ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf' →
    ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg' → f = g
[PROOFSTEP]
intro hf hg
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : ↑(Exists.choose hf') = ↑(Exists.choose hg')
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
⊢ f = g
[PROOFSTEP]
suffices f (hμ.toRootsOfUnity : Lˣ) = g (hμ.toRootsOfUnity : Lˣ)
  by
  apply AlgEquiv.coe_algHom_injective
  apply (hμ.powerBasis K).algHom_ext
  exact this
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : ↑(Exists.choose hf') = ↑(Exists.choose hg')
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑g ↑↑(toRootsOfUnity hμ)
⊢ f = g
[PROOFSTEP]
apply AlgEquiv.coe_algHom_injective
[GOAL]
case a
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : ↑(Exists.choose hf') = ↑(Exists.choose hg')
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑g ↑↑(toRootsOfUnity hμ)
⊢ ↑f = ↑g
[PROOFSTEP]
apply (hμ.powerBasis K).algHom_ext
[GOAL]
case a.h
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : ↑(Exists.choose hf') = ↑(Exists.choose hg')
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
this : ↑f ↑↑(toRootsOfUnity hμ) = ↑g ↑↑(toRootsOfUnity hμ)
⊢ ↑↑f (IsPrimitiveRoot.powerBasis K hμ).gen = ↑↑g (IsPrimitiveRoot.powerBasis K hμ).gen
[PROOFSTEP]
exact this
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : ↑(Exists.choose hf') = ↑(Exists.choose hg')
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
⊢ ↑f ↑↑(toRootsOfUnity hμ) = ↑g ↑↑(toRootsOfUnity hμ)
[PROOFSTEP]
rw [ZMod.eq_iff_modEq_nat] at hfg 
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : Exists.choose hf' ≡ Exists.choose hg' [MOD ↑n]
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
⊢ ↑f ↑↑(toRootsOfUnity hμ) = ↑g ↑↑(toRootsOfUnity hμ)
[PROOFSTEP]
refine' (hf.trans _).trans hg.symm
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : Exists.choose hf' ≡ Exists.choose hg' [MOD ↑n]
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
⊢ ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf' = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
[PROOFSTEP]
rw [← rootsOfUnity.coe_pow _ hf'.choose, ← rootsOfUnity.coe_pow _ hg'.choose]
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : Exists.choose hf' ≡ Exists.choose hg' [MOD ↑n]
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
⊢ ↑↑(toRootsOfUnity hμ ^ Exists.choose hf') = ↑↑(toRootsOfUnity hμ ^ Exists.choose hg')
[PROOFSTEP]
congr 2
[GOAL]
case e_self.e_self
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : Exists.choose hf' ≡ Exists.choose hg' [MOD ↑n]
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
⊢ toRootsOfUnity hμ ^ Exists.choose hf' = toRootsOfUnity hμ ^ Exists.choose hg'
[PROOFSTEP]
rw [pow_eq_pow_iff_modEq]
[GOAL]
case e_self.e_self
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : Exists.choose hf' ≡ Exists.choose hg' [MOD ↑n]
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
⊢ Exists.choose hf' ≡ Exists.choose hg' [MOD orderOf (toRootsOfUnity hμ)]
[PROOFSTEP]
convert hfg
[GOAL]
case h.e'_1
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : Exists.choose hf' ≡ Exists.choose hg' [MOD ↑n]
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
⊢ orderOf (toRootsOfUnity hμ) = ↑n
[PROOFSTEP]
rw [hμ.eq_orderOf]
  -- Porting note: was `{occs := occurrences.pos [2]}`
[GOAL]
case h.e'_1
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : Exists.choose hf' ≡ Exists.choose hg' [MOD ↑n]
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
⊢ orderOf (toRootsOfUnity hμ) = orderOf μ
[PROOFSTEP]
conv_rhs => rw [← hμ.toRootsOfUnity_coe_val]
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : Exists.choose hf' ≡ Exists.choose hg' [MOD ↑n]
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
| orderOf μ
[PROOFSTEP]
rw [← hμ.toRootsOfUnity_coe_val]
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : Exists.choose hf' ≡ Exists.choose hg' [MOD ↑n]
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
| orderOf μ
[PROOFSTEP]
rw [← hμ.toRootsOfUnity_coe_val]
[GOAL]
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : Exists.choose hf' ≡ Exists.choose hg' [MOD ↑n]
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
| orderOf μ
[PROOFSTEP]
rw [← hμ.toRootsOfUnity_coe_val]
[GOAL]
case h.e'_1
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
f g : L ≃ₐ[K] L
hf' : ∃ m, ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hg' : ∃ m, ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ m
hfg : Exists.choose hf' ≡ Exists.choose hg' [MOD ↑n]
hf : ↑f ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hf'
hg : ↑g ↑↑(toRootsOfUnity hμ) = ↑↑(toRootsOfUnity hμ) ^ Exists.choose hg'
⊢ orderOf (toRootsOfUnity hμ) = orderOf ↑↑(toRootsOfUnity hμ)
[PROOFSTEP]
rw [orderOf_units, orderOf_subgroup]
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
t : (ZMod ↑n)ˣ
⊢ minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n)).gen
[PROOFSTEP]
haveI := IsCyclotomicExtension.neZero' n K L
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
t : (ZMod ↑n)ˣ
this : NeZero ↑↑n
⊢ minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n)).gen
[PROOFSTEP]
simp only [IsPrimitiveRoot.powerBasis_gen]
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
t : (ZMod ↑n)ˣ
this : NeZero ↑↑n
⊢ minpoly K (zeta n K L) = minpoly K (zeta n K L ^ ZMod.val ↑t)
[PROOFSTEP]
have hr :=
  IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible
    ((zeta_spec n K L).pow_of_coprime _ (ZMod.val_coe_unit_coprime t)) h
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
t : (ZMod ↑n)ˣ
this : NeZero ↑↑n
hr : cyclotomic (↑n) K = minpoly K (zeta n K L ^ ZMod.val ↑t)
⊢ minpoly K (zeta n K L) = minpoly K (zeta n K L ^ ZMod.val ↑t)
[PROOFSTEP]
exact ((zeta_spec n K L).minpoly_eq_cyclotomic_of_irreducible h).symm.trans hr
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
f : L ≃ₐ[K] L
⊢ (fun t =>
        PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n))
          (_ :
            minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
              minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n)).gen))
      (OneHom.toFun (↑src✝) f) =
    f
[PROOFSTEP]
simp only [MonoidHom.toFun_eq_coe]
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
f : L ≃ₐ[K] L
⊢ PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
      (IsPrimitiveRoot.powerBasis K
        (_ :
          IsPrimitiveRoot
            (zeta n K L ^ ZMod.val ↑(↑(IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)) f)) ↑n))
      (_ :
        minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
          minpoly K
            (IsPrimitiveRoot.powerBasis K
                (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑(OneHom.toFun (↑src✝) f)) ↑n)).gen) =
    f
[PROOFSTEP]
apply AlgEquiv.coe_algHom_injective
[GOAL]
case a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
f : L ≃ₐ[K] L
⊢ ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K
          (_ :
            IsPrimitiveRoot
              (zeta n K L ^ ZMod.val ↑(↑(IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)) f)) ↑n))
        (_ :
          minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
            minpoly K
              (IsPrimitiveRoot.powerBasis K
                  (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑(OneHom.toFun (↑src✝) f)) ↑n)).gen)) =
    ↑f
[PROOFSTEP]
apply (hζ.powerBasis K).algHom_ext
[GOAL]
case a.h
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
f : L ≃ₐ[K] L
⊢ ↑↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
            (IsPrimitiveRoot.powerBasis K
              (_ :
                IsPrimitiveRoot
                  (zeta n K L ^ ZMod.val ↑(↑(IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)) f)) ↑n))
            (_ :
              minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
                minpoly K
                  (IsPrimitiveRoot.powerBasis K
                      (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑(OneHom.toFun (↑src✝) f)) ↑n)).gen))
      (IsPrimitiveRoot.powerBasis K hζ).gen =
    ↑↑f (IsPrimitiveRoot.powerBasis K hζ).gen
[PROOFSTEP]
simp only [AlgHom.coe_coe]
[GOAL]
case a.h
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
f : L ≃ₐ[K] L
⊢ ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K
            (_ :
              IsPrimitiveRoot
                (zeta n K L ^ ZMod.val ↑(↑(IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)) f)) ↑n))
          (_ :
            minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
              minpoly K
                (IsPrimitiveRoot.powerBasis K
                    (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑(OneHom.toFun (↑src✝) f)) ↑n)).gen))
      (IsPrimitiveRoot.powerBasis K hζ).gen =
    ↑f (IsPrimitiveRoot.powerBasis K hζ).gen
[PROOFSTEP]
rw [PowerBasis.equivOfMinpoly_gen]
[GOAL]
case a.h
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
f : L ≃ₐ[K] L
⊢ (IsPrimitiveRoot.powerBasis K
        (_ :
          IsPrimitiveRoot
            (zeta n K L ^ ZMod.val ↑(↑(IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)) f)) ↑n)).gen =
    ↑f (IsPrimitiveRoot.powerBasis K hζ).gen
[PROOFSTEP]
simp only [IsPrimitiveRoot.powerBasis_gen, IsPrimitiveRoot.autToPow_spec]
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
⊢ OneHom.toFun (↑src✝)
      ((fun t =>
          PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
            (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n))
            (_ :
              minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
                minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n)).gen))
        x) =
    x
[PROOFSTEP]
simp only [MonoidHom.toFun_eq_coe]
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
⊢ ↑(IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n))
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n))
        (_ :
          minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
            minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen)) =
    x
[PROOFSTEP]
generalize_proofs _ h
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
⊢ ↑(IsPrimitiveRoot.autToPow K h✝)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h) =
    x
[PROOFSTEP]
have key := hζ.autToPow_spec K ((hζ.powerBasis K).equivOfMinpoly ((hμ x).powerBasis K) h)
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L)
⊢ ↑(IsPrimitiveRoot.autToPow K h✝)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h) =
    x
[PROOFSTEP]
have := (hζ.powerBasis K).equivOfMinpoly_gen ((hμ x).powerBasis K) h
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L)
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (IsPrimitiveRoot.powerBasis K hζ).gen =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
⊢ ↑(IsPrimitiveRoot.autToPow K h✝)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h) =
    x
[PROOFSTEP]
rw [hζ.powerBasis_gen K] at this 
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L)
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
⊢ ↑(IsPrimitiveRoot.autToPow K h✝)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h) =
    x
[PROOFSTEP]
rw [this, IsPrimitiveRoot.powerBasis_gen] at key 
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
⊢ ↑(IsPrimitiveRoot.autToPow K h✝)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h) =
    x
[PROOFSTEP]
conv at key =>
  congr; congr
  rw [← hζ.toRootsOfUnity_coe_val]
  rfl; rfl
  rw [← hζ.toRootsOfUnity_coe_val]
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
[PROOFSTEP]
  congr; congr
  rw [← hζ.toRootsOfUnity_coe_val]
  rfl; rfl
  rw [← hζ.toRootsOfUnity_coe_val]
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
[PROOFSTEP]
  congr; congr
  rw [← hζ.toRootsOfUnity_coe_val]
  rfl; rfl
  rw [← hζ.toRootsOfUnity_coe_val]
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
[PROOFSTEP]
congr
[GOAL]
case a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| zeta n K L ^
    ZMod.val
      ↑(↑(IsPrimitiveRoot.autToPow K hζ)
          (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
            (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h))
case a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| zeta n K L ^ ZMod.val ↑x
[PROOFSTEP]
congr
[GOAL]
case a.a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| zeta n K L
case a.a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| ZMod.val
    ↑(↑(IsPrimitiveRoot.autToPow K hζ)
        (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h))
case a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| zeta n K L ^ ZMod.val ↑x
[PROOFSTEP]
rw [← hζ.toRootsOfUnity_coe_val]
[GOAL]
case a.a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| ↑↑(IsPrimitiveRoot.toRootsOfUnity hζ)
case a.a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| ZMod.val
    ↑(↑(IsPrimitiveRoot.autToPow K hζ)
        (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h))
case a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| zeta n K L ^ ZMod.val ↑x
[PROOFSTEP]
rfl
[GOAL]
case a.a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| ZMod.val
    ↑(↑(IsPrimitiveRoot.autToPow K hζ)
        (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h))
case a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| zeta n K L ^ ZMod.val ↑x
[PROOFSTEP]
rfl
[GOAL]
case a
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  zeta n K L ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    zeta n K L ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
| zeta n K L ^ ZMod.val ↑x
[PROOFSTEP]
rw [← hζ.toRootsOfUnity_coe_val]
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  ↑↑(IsPrimitiveRoot.toRootsOfUnity hζ) ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    ↑↑(IsPrimitiveRoot.toRootsOfUnity hζ) ^ ZMod.val ↑x
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
⊢ ↑(IsPrimitiveRoot.autToPow K h✝)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h) =
    x
[PROOFSTEP]
simp only [← rootsOfUnity.coe_pow] at key 
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  ↑↑(IsPrimitiveRoot.toRootsOfUnity hζ ^
          ZMod.val
            ↑(↑(IsPrimitiveRoot.autToPow K hζ)
                (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
                  (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h))) =
    ↑↑(IsPrimitiveRoot.toRootsOfUnity hζ ^ ZMod.val ↑x)
⊢ ↑(IsPrimitiveRoot.autToPow K h✝)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h) =
    x
[PROOFSTEP]
replace key := rootsOfUnity.coe_injective key
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  IsPrimitiveRoot.toRootsOfUnity hζ ^
      ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    IsPrimitiveRoot.toRootsOfUnity hζ ^ ZMod.val ↑x
⊢ ↑(IsPrimitiveRoot.autToPow K h✝)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h) =
    x
[PROOFSTEP]
rw [pow_eq_pow_iff_modEq, ← orderOf_subgroup, ← orderOf_units, hζ.toRootsOfUnity_coe_val, ←
  (zeta_spec n K L).eq_orderOf, ← ZMod.eq_iff_modEq_nat] at key 
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  ↑(ZMod.val
        ↑(↑(IsPrimitiveRoot.autToPow K hζ)
            (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h))) =
    ↑(ZMod.val ↑x)
⊢ ↑(IsPrimitiveRoot.autToPow K h✝)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h) =
    x
[PROOFSTEP]
simp only [ZMod.nat_cast_val, ZMod.cast_id', id.def] at key 
[GOAL]
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 := zeta_spec n K L
hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑t) ↑n :=
  fun t => IsPrimitiveRoot.pow_of_coprime hζ (ZMod.val ↑t) (ZMod.val_coe_unit_coprime t)
src✝ : (L ≃ₐ[K] L) →* (ZMod ↑n)ˣ := IsPrimitiveRoot.autToPow K (_ : IsPrimitiveRoot (zeta n K L) ↑n)
x : (ZMod ↑n)ˣ
h✝ : IsPrimitiveRoot (zeta n K L) ↑n
h :
  minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
this :
  ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)
      (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)).gen
key :
  ↑(↑(IsPrimitiveRoot.autToPow K hζ)
        (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h)) =
    ↑x
⊢ ↑(IsPrimitiveRoot.autToPow K h✝)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L ^ ZMod.val ↑x) ↑n)) h) =
    x
[PROOFSTEP]
exact Units.ext key
[GOAL]
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) = μ
[PROOFSTEP]
simp_rw [fromZetaAut, autEquivPow_symm_apply]
  -- Porting note: `generalize_proofs` did not generalize the same proofs, making the proof different.
[GOAL]
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)
⊢ ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L) ↑n))
          (IsPrimitiveRoot.powerBasis K
            (_ :
              IsPrimitiveRoot
                (zeta n K L ^
                  ZMod.val
                    ↑(ZMod.unitOfCoprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ))
                        (_ : Nat.coprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ)) ↑n)))
                ↑n))
          (_ :
            minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L) ↑n)).gen =
              minpoly K
                (IsPrimitiveRoot.powerBasis K
                    (_ :
                      IsPrimitiveRoot
                        (zeta n K L ^
                          ZMod.val
                            ↑(ZMod.unitOfCoprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ))
                                (_ : Nat.coprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ)) ↑n)))
                        ↑n)).gen))
      (zeta n K L) =
    μ
[PROOFSTEP]
generalize_proofs h1 h2
[GOAL]
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)
h1 :
  IsPrimitiveRoot
    (zeta n K L ^
      ZMod.val
        ↑(ZMod.unitOfCoprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ))
            (_ : Nat.coprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ)) ↑n)))
    ↑n
h2 :
  minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L) ↑n)).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K h1).gen
⊢ ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L) ↑n))
          (IsPrimitiveRoot.powerBasis K h1) h2)
      (zeta n K L) =
    μ
[PROOFSTEP]
nth_rewrite 4 [← (zeta_spec n K L).powerBasis_gen K]
[GOAL]
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)
h1 :
  IsPrimitiveRoot
    (zeta n K L ^
      ZMod.val
        ↑(ZMod.unitOfCoprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ))
            (_ : Nat.coprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ)) ↑n)))
    ↑n
h2 :
  minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L) ↑n)).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K h1).gen
⊢ ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L) ↑n))
          (IsPrimitiveRoot.powerBasis K h1) h2)
      (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L) ↑n)).gen =
    μ
[PROOFSTEP]
have := Exists.choose_spec ((zeta_spec n K L).eq_pow_of_pow_eq_one hμ.pow_eq_one n.pos)
[GOAL]
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)
h1 :
  IsPrimitiveRoot
    (zeta n K L ^
      ZMod.val
        ↑(ZMod.unitOfCoprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ))
            (_ : Nat.coprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ)) ↑n)))
    ↑n
h2 :
  minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L) ↑n)).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K h1).gen
this :
  Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ) < ↑n ∧
    zeta n K L ^ Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ) = μ
⊢ ↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L) ↑n))
          (IsPrimitiveRoot.powerBasis K h1) h2)
      (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L) ↑n)).gen =
    μ
[PROOFSTEP]
rw [PowerBasis.equivOfMinpoly_gen, h1.powerBasis_gen K, ZMod.coe_unitOfCoprime, ZMod.val_cast_of_lt this.1]
[GOAL]
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)
h1 :
  IsPrimitiveRoot
    (zeta n K L ^
      ZMod.val
        ↑(ZMod.unitOfCoprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ))
            (_ : Nat.coprime (Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ)) ↑n)))
    ↑n
h2 :
  minpoly K (IsPrimitiveRoot.powerBasis K (_ : IsPrimitiveRoot (zeta n K L) ↑n)).gen =
    minpoly K (IsPrimitiveRoot.powerBasis K h1).gen
this :
  Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ) < ↑n ∧
    zeta n K L ^ Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ) = μ
⊢ zeta n K L ^ Exists.choose (_ : ∃ i, i < ↑n ∧ zeta n K L ^ i = μ) = μ
[PROOFSTEP]
exact this.2
