-- Mathlib/FieldTheory/Separable.lean
theorem separable_X_pow_sub_C_unit {n : ℕ} (u : Rˣ) (hn : IsUnit (n : R)) :
    Separable (X ^ n - C (u : R))

Proof state:
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (C ↑n * X ^ (n - 1)) = 1

Tactic:
calc
  -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1)) =
      C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) := by
    simp only [C.map_mul, C_eq_natCast]
    ring
  _ = 1 := by
    simp only [Units.inv_mul, hn', C.map_one, mul_one, ← pow_succ',
      Nat.sub_add_cancel (show 1 ≤ n from hpos), sub_add_cancel]

Result:
no goals

Proof state:
case inl
R : Type u
inst✝ : CommRing R
u : Rˣ
a✝ : Nontrivial R
hn : IsUnit ↑0
⊢ (X ^ 0 - C ↑u).Separable

Tactic:
simp at hn

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
⊢ (X ^ n - C ↑u).Separable

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
⊢ (X ^ n - C ↑u).Separable

Proof state:
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1)) =
    C ↑u⁻¹ * C ↑u - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * (C n' * ↑n) * (X * X ^ (n - 1))

Tactic:
ring

Result:
no goals

Proof state:
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ ∃ a b, a * (X ^ n - C ↑u) + b * derivative (X ^ n - C ↑u) = 1

Tactic:
refine ⟨-C ↑u⁻¹, C (↑u⁻¹ : R) * C n' * X, ?_⟩

Result:
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * derivative (X ^ n - C ↑u) = 1

Proof state:
case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
⊢ (X ^ n - C ↑u).Separable

Tactic:
apply (separable_def' (X ^ n - C (u : R))).2

Result:
case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
⊢ ∃ a b, a * (X ^ n - C ↑u) + b * derivative (X ^ n - C ↑u) = 1

Proof state:
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
⊢ (X ^ n - C ↑u).Separable

Tactic:
rcases n.eq_zero_or_pos with (rfl | hpos)

Result:
case inl
R : Type u
inst✝ : CommRing R
u : Rˣ
a✝ : Nontrivial R
hn : IsUnit ↑0
⊢ (X ^ 0 - C ↑u).Separable

case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
⊢ (X ^ n - C ↑u).Separable

Proof state:
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1)) =
    C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1))

Tactic:
simp only [C.map_mul, C_eq_natCast]

Result:
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1)) =
    C ↑u⁻¹ * C ↑u - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * (C n' * ↑n) * (X * X ^ (n - 1))

Proof state:
case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
⊢ ∃ a b, a * (X ^ n - C ↑u) + b * derivative (X ^ n - C ↑u) = 1

Tactic:
obtain ⟨n', hn'⟩ := hn.exists_left_inv

Result:
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ ∃ a b, a * (X ^ n - C ↑u) + b * derivative (X ^ n - C ↑u) = 1

Proof state:
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * derivative (X ^ n - C ↑u) = 1

Tactic:
rw [derivative_sub, derivative_C, sub_zero, derivative_pow X n, derivative_X, mul_one]

Result:
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (C ↑n * X ^ (n - 1)) = 1

Proof state:
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) = 1

Tactic:
simp only [Units.inv_mul, hn', C.map_one, mul_one, ← pow_succ',
  Nat.sub_add_cancel (show 1 ≤ n from hpos), sub_add_cancel]

Result:
no goals