-- Mathlib/FieldTheory/IsSepClosed.lean
theorem exists_root_C_mul_X_pow_add_C_mul_X_add_C
    [IsSepClosed k] {n : ℕ} (a b c : k) (hn : (n : k) = 0) (hn' : 2 ≤ n) (hb : b ≠ 0) :
    ∃ x, a * x ^ n + b * x + c = 0

Proof state:
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
hdeg : f.degree ≠ 0
hsep : f.Separable
x : k
hx : f.IsRoot x
⊢ ∃ x, a * x ^ n + b * x + c = 0

Tactic:
exact ⟨x, by simpa [f] using hx⟩

Result:
no goals

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
⊢ f.natDegree ≠ Zero.zero

Tactic:
by_cases ha : a = 0

Result:
case pos
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : a = 0
⊢ f.natDegree ≠ Zero.zero

case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
⊢ f.natDegree ≠ Zero.zero

Proof state:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
⊢ f.natDegree = n

Tactic:
simp_rw [f]

Result:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
⊢ (C a * X ^ n + C b * X + C c).natDegree = n

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
⊢ ∃ x, a * x ^ n + b * x + c = 0

Tactic:
let f : k[X] := C a * X ^ n + C b * X + C c

Result:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
⊢ ∃ x, a * x ^ n + b * x + c = 0

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
hdeg : f.degree ≠ 0
⊢ ∃ x, a * x ^ n + b * x + c = 0

Tactic:
have hsep : f.Separable := separable_C_mul_X_pow_add_C_mul_X_add_C a b c hn hb.isUnit

Result:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
hdeg : f.degree ≠ 0
hsep : f.Separable
⊢ ∃ x, a * x ^ n + b * x + c = 0

Proof state:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
h0 : n ≠ 0
h1 : n ≠ 1
⊢ (C a * X ^ n + C b * X + C c).natDegree = n

Tactic:
have : 1 ≤ n := le_trans one_le_two hn'

Result:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
h0 : n ≠ 0
h1 : n ≠ 1
this : 1 ≤ n
⊢ (C a * X ^ n + C b * X + C c).natDegree = n

Proof state:
case neg.coeff_ne_zero
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
h0 : n ≠ 0
h1 : n ≠ 1
this : 1 ≤ n
⊢ ¬((a + if n = 1 then b else 0) + if n = 0 then c else 0) = 0

Tactic:
simp [h0, h1, ha]

Result:
no goals

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
⊢ n ≠ 0

Tactic:
linarith only [hn']

Result:
no goals

Proof state:
case pos
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : a = 0
⊢ f.natDegree = 1

Tactic:
simp_rw [f, ha, map_zero, zero_mul, zero_add]

Result:
case pos
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : a = 0
⊢ (C b * X + C c).natDegree = 1

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
h0 : n ≠ 0
⊢ n ≠ 1

Tactic:
linarith only [hn']

Result:
no goals

Proof state:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
h0 : n ≠ 0
⊢ (C a * X ^ n + C b * X + C c).natDegree = n

Tactic:
have h1 : n ≠ 1 := by linarith only [hn']

Result:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
h0 : n ≠ 0
h1 : n ≠ 1
⊢ (C a * X ^ n + C b * X + C c).natDegree = n

Proof state:
case pos
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : a = 0
⊢ (C b * X + C c).natDegree = 1

Tactic:
compute_degree!

Result:
no goals

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
hdeg : f.degree ≠ 0
hsep : f.Separable
x : k
hx : f.IsRoot x
⊢ a * x ^ n + b * x + c = 0

Tactic:
simpa [f] using hx

Result:
no goals

Proof state:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
⊢ (C a * X ^ n + C b * X + C c).natDegree = n

Tactic:
have h0 : n ≠ 0 := by linarith only [hn']

Result:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
h0 : n ≠ 0
⊢ (C a * X ^ n + C b * X + C c).natDegree = n

Proof state:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
⊢ f.natDegree ≠ Zero.zero

Tactic:
suffices f.natDegree = n from this ▸ (lt_of_lt_of_le zero_lt_two hn').ne'

Result:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
⊢ f.natDegree = n

Proof state:
case pos
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : a = 0
⊢ f.natDegree ≠ Zero.zero

Tactic:
suffices f.natDegree = 1 from this ▸ one_ne_zero

Result:
case pos
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : a = 0
⊢ f.natDegree = 1

Proof state:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
h0 : n ≠ 0
h1 : n ≠ 1
this : 1 ≤ n
⊢ (C a * X ^ n + C b * X + C c).natDegree = n

Tactic:
compute_degree!

Result:
case neg.coeff_ne_zero
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
ha : ¬a = 0
h0 : n ≠ 0
h1 : n ≠ 1
this : 1 ≤ n
⊢ ¬((a + if n = 1 then b else 0) + if n = 0 then c else 0) = 0

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
hdeg : f.degree ≠ 0
hsep : f.Separable
⊢ ∃ x, a * x ^ n + b * x + c = 0

Tactic:
obtain ⟨x, hx⟩ := exists_root f hdeg hsep

Result:
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
hdeg : f.degree ≠ 0
hsep : f.Separable
x : k
hx : f.IsRoot x
⊢ ∃ x, a * x ^ n + b * x + c = 0