-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
lemma natDegree_eq_one : p.natDegree = 1 ↔ ∃ a ≠ 0, ∃ b, C a * X + C b = p

Proof state:
case refine_3.intro.intro.intro
R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
⊢ (C a * X + C b).natDegree = 1

Tactic:
simp [ha]

Result:
no goals

Proof state:
case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = p

Tactic:
ext n

Result:
case refine_2.a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff n = p.coeff n

Proof state:
case refine_3
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p) → p.natDegree = 1

Tactic:
rintro ⟨a, ha, b, rfl⟩

Result:
case refine_3.intro.intro.intro
R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
⊢ (C a * X + C b).natDegree = 1

Proof state:
case refine_2.a.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (n + 1 + 1) = p.coeff (n + 1 + 1)

Tactic:
simp only [coeff_add, coeff_mul_X, coeff_C_succ, add_zero]

Result:
case refine_2.a.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ 0 = p.coeff (n + 1 + 1)

Proof state:
case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p.coeff 1 = 0
⊢ False

Tactic:
rw [← hp, coeff_natDegree, leadingCoeff_eq_zero] at h

Result:
case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p = 0
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree = 1 ↔ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p

Tactic:
refine ⟨fun hp ↦ ⟨p.coeff 1, fun h ↦ ?_, p.coeff 0, ?_⟩, ?_⟩

Result:
case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p.coeff 1 = 0
⊢ False

case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = p

case refine_3
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p) → p.natDegree = 1

Proof state:
case refine_2.a.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0 = p.coeff 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_2.a.succ.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (0 + 1) = p.coeff (0 + 1)

Tactic:
simp

Result:
no goals

Proof state:
case refine_2.a.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ 0 = p.coeff (n + 1 + 1)

Tactic:
rw [coeff_eq_zero_of_natDegree_lt]

Result:
case refine_2.a.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ p.natDegree < n + 1 + 1

Proof state:
case refine_2.a.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ p.natDegree < n + 1 + 1

Tactic:
simp [hp]

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p = 0
⊢ False

Tactic:
aesop

Result:
no goals

Proof state:
case refine_2.a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
obtain _ | _ | n := n

Result:
case refine_2.a.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0 = p.coeff 0

case refine_2.a.succ.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (0 + 1) = p.coeff (0 + 1)

case refine_2.a.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (n + 1 + 1) = p.coeff (n + 1 + 1)