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

Proof state:
case 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
η : ↥(rootsOfUnity n K)
⊢ ((autEquivRootsOfUnity hζ H L).symm η) (rootOfSplitsXPowSubC ⋯ a L) =
    (autEquivRootsOfUnity hζ H L) ((autEquivRootsOfUnity hζ H L).symm η) • rootOfSplitsXPowSubC ⋯ a L

Tactic:
rw [MulEquiv.apply_symm_apply, autEquivRootsOfUnity]

Result:
case 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
η : ↥(rootsOfUnity n K)
⊢ (((adjoinRootXPowSubCEquiv hζ H ⋯).symm.autCongr.trans (autAdjoinRootXPowSubCEquiv hζ H).symm).symm η)
      (rootOfSplitsXPowSubC ⋯ a 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)
inst✝ : NeZero n
σ : L ≃ₐ[K] L
⊢ σ (rootOfSplitsXPowSubC ⋯ a L) = (autEquivRootsOfUnity hζ H L) σ • rootOfSplitsXPowSubC ⋯ a L

Tactic:
obtain ⟨η, rfl⟩ := (autEquivRootsOfUnity hζ H L).symm.surjective σ

Result:
case 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
η : ↥(rootsOfUnity n K)
⊢ ((autEquivRootsOfUnity hζ H L).symm η) (rootOfSplitsXPowSubC ⋯ a L) =
    (autEquivRootsOfUnity hζ H L) ((autEquivRootsOfUnity hζ H L).symm η) • rootOfSplitsXPowSubC ⋯ a L

Proof state:
case 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
η : ↥(rootsOfUnity n K)
⊢ ↑↑η • rootOfSplitsXPowSubC ⋯ a L = η • rootOfSplitsXPowSubC ⋯ a L

Tactic:
rfl

Result:
no goals

Proof state:
case 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
η : ↥(rootsOfUnity n K)
⊢ (((adjoinRootXPowSubCEquiv hζ H ⋯).symm.autCongr.trans (autAdjoinRootXPowSubCEquiv hζ H).symm).symm η)
      (rootOfSplitsXPowSubC ⋯ a L) =
    η • rootOfSplitsXPowSubC ⋯ a L

Tactic:
simp only [MulEquiv.symm_trans_apply, AlgEquiv.autCongr_symm, AlgEquiv.symm_symm,
  MulEquiv.symm_symm, AlgEquiv.autCongr_apply, AlgEquiv.trans_apply,
  adjoinRootXPowSubCEquiv_symm_eq_root, autAdjoinRootXPowSubCEquiv_root, map_smul,
  adjoinRootXPowSubCEquiv_root]

Result:
case 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
η : ↥(rootsOfUnity n K)
⊢ ↑↑η • rootOfSplitsXPowSubC ⋯ a L = η • rootOfSplitsXPowSubC ⋯ a L