-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem degree_pos_induction_on {P : R[X] → Prop} (p : R[X]) (h0 : 0 < degree p)
    (hC : ∀ {a}, a ≠ 0 → P (C a * X)) (hX : ∀ {p}, 0 < degree p → P p → P (p * X))
    (hadd : ∀ {p} {a}, 0 < degree p → P p → P (p + C a)) : P p :=
  recOnHorner p (fun h => by rw [degree_zero] at h; exact absurd h (by decide))
    (fun p a heq0 _ ih h0 =>
      (have : 0 < degree p :=
        (lt_of_not_ge fun h =>
          not_lt_of_ge (degree_C_le (a := a)) <|
            by rwa [eq_C_of_degree_le_zero h, ← C_add,heq0,zero_add] at h0)
      hadd this (ih this)))
    (fun p _ ih h0' =>
      if h0 : 0 < degree p then hX h0 (ih h0)
      else by
        rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at h0' ⊢
        exact hC fun h : coeff p 0 = 0 => by simp [h, Nat.not_lt_zero] at h0')
    h0

Proof state:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (p * X).degree
h0 : ¬0 < p.degree
⊢ P (p * X)

Tactic:
rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at h0' ⊢

Result:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (C (p.coeff 0) * X).degree
h0 : ¬0 < p.degree
⊢ P (C (p.coeff 0) * X)

Proof state:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (C (p.coeff 0) * X).degree
h0 : ¬0 < p.degree
⊢ P (C (p.coeff 0) * X)

Tactic:
exact hC fun h : coeff p 0 = 0 => by simp [h, Nat.not_lt_zero] at h0'

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
a : R
heq0 : p.coeff 0 = 0
x✝ : a ≠ 0
ih : 0 < p.degree → P p
h0 : 0 < (p + C a).degree
h : 0 ≥ p.degree
⊢ 0 < (C a).degree

Tactic:
rwa [eq_C_of_degree_le_zero h, ← C_add,heq0,zero_add] at h0

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
h : 0 < ⊥
⊢ ¬0 < ⊥

Tactic:
decide

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
h : 0 < degree 0
⊢ P 0

Tactic:
rw [degree_zero] at h

Result:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
h : 0 < ⊥
⊢ P 0

Proof state:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (C (p.coeff 0) * X).degree
h0 : ¬0 < p.degree
h : p.coeff 0 = 0
⊢ False

Tactic:
simp [h, Nat.not_lt_zero] at h0'

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
h : 0 < ⊥
⊢ P 0

Tactic:
exact absurd h (by decide)

Result:
no goals