R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
⊢ Separable (X ^ n - ↑C ↑u)
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
⊢ Separable (X ^ n - ↑C ↑u)
nontriviality R
case inl
R : Type u
inst✝ : CommRing R
u : Rˣ
✝ : Nontrivial R
hn : IsUnit ↑0
⊢ Separable (X ^ 0 - ↑C ↑u)

case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
⊢ Separable (X ^ n - ↑C ↑u)
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
⊢ Separable (X ^ n - ↑C ↑u)
rcases n.eq_zero_or_pos with (rfl | hpos)
case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
⊢ ∃ a b, a * (X ^ n - ↑C ↑u) + b * ↑derivative (X ^ n - ↑C ↑u) = 1
case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
⊢ Separable (X ^ n - ↑C ↑u)
apply (separable_def' (X ^ n - C (u : R))).2
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : 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
case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
⊢ ∃ a b, a * (X ^ n - ↑C ↑u) + b * ↑derivative (X ^ n - ↑C ↑u) = 1
obtain ⟨n', hn'⟩ := hn.exists_left_inv
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : 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
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : 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
refine' ⟨-C ↑u⁻¹, C (↑u⁻¹ : R) * C n' * X, _⟩
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : 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
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : 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
rw [derivative_sub, derivative_C, sub_zero, derivative_pow X n, derivative_X, mul_one]
no goals
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : 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
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_nat_cast]
    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]
no goals
case inl
R : Type u
inst✝ : CommRing R
u : Rˣ
✝ : Nontrivial R
hn : IsUnit ↑0
⊢ Separable (X ^ 0 - ↑C ↑u)
simp at hn
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : 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))
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : 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))
simp only [C.map_mul, C_eq_nat_cast]
no goals
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : 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))
ring
no goals
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : 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
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]