-- Mathlib/FieldTheory/KummerExtension.lean
lemma autEquivRootsOfUnity_smul [NeZero n] (σ : L ≃ₐ[K] L) :
    autEquivRootsOfUnity hζ H L σ • α = σ α

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ' : ζ ∈ primitiveRoots n K
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Tactic:
have hn := NeZero.pos n

Result:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ' : ζ ∈ primitiveRoots n K
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Proof state:
case intro.intro
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
i : ℕ
left✝ : i < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • ζ ^ i • rootOfSplitsXPowSubC ⋯ a L =
    ζ ^ i • (autEquivRootsOfUnity hζ H L) σ • rootOfSplitsXPowSubC ⋯ a L

Tactic:
exact smul_comm _ _ _

Result:
no goals

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
σ : L ≃ₐ[K] L
⊢ (autEquivRootsOfUnity hζ H L) σ • α = σ α

Tactic:
have ⟨ζ, hζ'⟩ := hζ

Result:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ' : ζ ∈ primitiveRoots n K
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
hα : ∃ a_1 < n, (algebraMap K L) ζ ^ a_1 * rootOfSplitsXPowSubC ⋯ a L = α
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Tactic:
obtain ⟨i, _, rfl⟩ := hα

Result:
case intro.intro
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
i : ℕ
left✝ : i < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • ((algebraMap K L) ζ ^ i * rootOfSplitsXPowSubC ⋯ a L) =
    σ ((algebraMap K L) ζ ^ i * rootOfSplitsXPowSubC ⋯ a L)

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hα : α ∈ Multiset.map (fun x => (algebraMap K L) ζ ^ x * rootOfSplitsXPowSubC ⋯ a L) (Multiset.range n)
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Tactic:
simp only [Finset.range_val, Multiset.mem_map, Multiset.mem_range] at hα

Result:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
hα : ∃ a_1 < n, (algebraMap K L) ζ ^ a_1 * rootOfSplitsXPowSubC ⋯ a L = α
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Proof state:
case intro.intro
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
i : ℕ
left✝ : i < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • ((algebraMap K L) ζ ^ i * rootOfSplitsXPowSubC ⋯ a L) =
    σ ((algebraMap K L) ζ ^ i * rootOfSplitsXPowSubC ⋯ a L)

Tactic:
simp only [map_mul, ← map_pow, ← Algebra.smul_def, map_smul,
  autEquivRootsOfUnity_apply_rootOfSplit hζ H L]

Result:
case intro.intro
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
i : ℕ
left✝ : i < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • ζ ^ i • rootOfSplitsXPowSubC ⋯ a L =
    ζ ^ i • (autEquivRootsOfUnity hζ H L) σ • rootOfSplitsXPowSubC ⋯ a L

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ' : ζ ∈ primitiveRoots n K
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Tactic:
rw [mem_primitiveRoots hn] at hζ'

Result:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Tactic:
rw [← mem_nthRoots hn, (hζ'.map_of_injective (algebraMap K L).injective).nthRoots_eq
  (rootOfSplitsXPowSubC_pow a L)] at hα

Result:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
inst✝ : NeZero n
σ : L ≃ₐ[K] L
ζ : K
hα : α ∈ Multiset.map (fun x => (algebraMap K L) ζ ^ x * rootOfSplitsXPowSubC ⋯ a L) (Multiset.range n)
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α