-- Mathlib/FieldTheory/KummerExtension.lean
lemma autAdjoinRootXPowSubCEquiv_symm_smul [NeZero n] (σ) :
    ((autAdjoinRootXPowSubCEquiv hζ H).symm σ : Kˣ) • (root _ : K[n√a]) = σ (root _)

Proof state:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
this : Fact (Irreducible (X ^ n - C a))
⊢ (if a = 0 then root (X ^ n - C a) else σ (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a)) =
    σ (root (X ^ n - C a))

Tactic:
simp_rw [← root_X_pow_sub_C_eq_zero_iff H]

Result:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
this : Fact (Irreducible (X ^ n - C a))
⊢ (if root (X ^ n - C a) = 0 then root (X ^ n - C a)
    else σ (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a)) =
    σ (root (X ^ n - C a))

Proof state:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
⊢ ↑((autAdjoinRootXPowSubCEquiv hζ H).symm σ) • root (X ^ n - C a) = σ (root (X ^ n - C a))

Tactic:
have := Fact.mk H

Result:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
this : Fact (Irreducible (X ^ n - C a))
⊢ ↑((autAdjoinRootXPowSubCEquiv hζ H).symm σ) • root (X ^ n - C a) = σ (root (X ^ n - C a))

Proof state:
case neg
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
this : Fact (Irreducible (X ^ n - C a))
h : ¬root (X ^ n - C a) = 0
⊢ σ (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a) = σ (root (X ^ n - C a))

Tactic:
rw [div_mul_cancel₀ _ h]

Result:
no goals

Proof state:
case pos
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
this : Fact (Irreducible (X ^ n - C a))
h : root (X ^ n - C a) = 0
⊢ root (X ^ n - C a) = σ (root (X ^ n - C a))

Tactic:
rw [h, map_zero]

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)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
this : Fact (Irreducible (X ^ n - C a))
⊢ (if root (X ^ n - C a) = 0 then root (X ^ n - C a)
    else σ (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a)) =
    σ (root (X ^ n - C a))

Tactic:
split_ifs with h

Result:
case pos
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
this : Fact (Irreducible (X ^ n - C a))
h : root (X ^ n - C a) = 0
⊢ root (X ^ n - C a) = σ (root (X ^ n - C a))

case neg
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
this : Fact (Irreducible (X ^ n - C a))
h : ¬root (X ^ n - C a) = 0
⊢ σ (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a) = σ (root (X ^ n - C a))

Proof state:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
this : Fact (Irreducible (X ^ n - C a))
⊢ ↑((autAdjoinRootXPowSubCEquiv hζ H).symm σ) • root (X ^ n - C a) = σ (root (X ^ n - C a))

Tactic:
simp only [autAdjoinRootXPowSubCEquiv, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
  MulEquiv.symm_mk, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, AdjoinRootXPowSubCEquivToRootsOfUnity,
  AdjoinRoot.algebraMap_eq, rootsOfUnity.mkOfPowEq, Units.smul_def, Algebra.smul_def,
  rootsOfUnityEquivOfPrimitiveRoots_symm_apply, Units.val_ofPowEqOne, ite_mul, one_mul]

Result:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
this : Fact (Irreducible (X ^ n - C a))
⊢ (if a = 0 then root (X ^ n - C a) else σ (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a)) =
    σ (root (X ^ n - C a))