awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst : Semiring R
p_1 q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
wf : p.divX.degree < p.degree
rw :
  (hp : ¬HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) = 0) →
    (wf :
        (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).divX.degree <
          (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree) →
      M (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]))
⊢ M p

Tactic:
rw [← divX_mul_X_add p] at *

Premises used: Polynomial.divX_mul_X_add
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst : Semiring R
p_1 q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) = 0
wf :
  (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).divX.degree <
    (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
hcp0 : p.coeff 0 = 0
rw : M (p.divX * X)
⊢ M (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]))

Tactic:
rw [hcp0, C_0, add_zero]

Premises used: Polynomial.C_0, add_zero
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst : Semiring R
p_1 q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) = 0
wf :
  (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).divX.degree <
    (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
hcp0 : p.coeff 0 = 0
h : p.divX = 0
⊢ False

Tactic:
simp [h, hcp0] at hp
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst : Semiring R
p_1 q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) = 0
wf :
  (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).divX.degree <
    (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
hcp0 : p.coeff 0 = 0
⊢ M (p.divX * X)

Tactic:
exact
          MX _ (fun h : divX p = 0 => by simp [h, hcp0] at hp) (recOnHorner (divX p) M0 MC MX)

Premises used: Polynomial.divX
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst : Semiring R
p_1 q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) = 0
wf :
  (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).divX.degree <
    (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
hcp0 : ¬p.coeff 0 = 0
hpX0 : p.divX = 0
rw : M 0
⊢ M (p.divX * X)

Tactic:
rw [hpX0, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst : Semiring R
p_1 q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) = 0
wf :
  (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).divX.degree <
    (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
hcp0 : ¬p.coeff 0 = 0
hpX0 : p.divX = 0
⊢ M 0

Tactic:
exact M0
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst : Semiring R
p_1 q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) = 0
wf :
  (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).divX.degree <
    (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
⊢ M (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]))

Tactic:
exact
      if hcp0 : coeff p 0 = 0 then by
        rw [hcp0, C_0, add_zero]
        exact
          MX _ (fun h : divX p = 0 => by simp [h, hcp0] at hp) (recOnHorner (divX p) M0 MC MX)
      else
        MC _ _ (coeff_mul_X_zero _) hcp0
          (if hpX0 : divX p = 0 then show M (divX p * X) by rw [hpX0, zero_mul]; exact M0
          else MX (divX p) hpX0 (recOnHorner _ M0 MC MX))

Premises used: Polynomial.coeff, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) 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 (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
h : 0 < degree.{u} (R := R) 0
⊢ LT.lt (α := WithBot ℕ) 0 ⊥

Tactic:
rw [degree_zero] at h

Premises used: Polynomial.degree_zero
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) 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 (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
h : LT.lt (α := WithBot ℕ) 0 ⊥
⊢ ¬LT.lt (α := WithBot ℕ) 0 ⊥

Tactic:
decide
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) 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 (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
h : LT.lt (α := WithBot ℕ) 0 ⊥
⊢ P 0

Tactic:
exact absurd h (by decide)

Premises used: absurd
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
P : R[X] → Prop
p_1 : R[X]
h0_1 : 0 < p_1.degree
hC : ∀ {a : R}, a ≠ 0 → P (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) 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 (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
p : R[X]
a : R
heq0 : p.coeff 0 = 0
h_1 : a ≠ 0
ih : 0 < p.degree → P p
h0 : 0 < (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree
h : p.degree ≤ 0
rwa :
  ∀
    (h0 :
      0 <
        (HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
            ((C : (a : R) → R[X]) a : R[X])).degree)
    (h : p.degree ≤ 0), 0 < degree.{u} (R := R) ((C : (a : R) → R[X]) a)
rwa₁ :
  ∀ (h0 : 0 < degree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0 + a))) (h : p.degree ≤ 0),
    0 < degree.{u} (R := R) ((C : (a : R) → R[X]) a)
rwa₂ :
  ∀ (h0 : 0 < degree.{u} (R := R) ((C : (a : R) → R[X]) (0 + a))) (h : p.degree ≤ 0),
    0 < degree.{u} (R := R) ((C : (a : R) → R[X]) a)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (h0 : 0 < degree.{u} (R := R) ((C : (a : R) → R[X]) a)) (h : p.degree ≤ 0),
    0 < degree.{u} (R := R) ((C : (a : R) → R[X]) a)
⊢ 0 < degree.{u} (R := R) ((C : (a : R) → R[X]) a)

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

Premises used: zero_add, Polynomial.eq_C_of_degree_le_zero, Polynomial.C_add
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
P : R[X] → Prop
p_1 : R[X]
h0_1 : 0 < p_1.degree
hC : ∀ {a : R}, a ≠ 0 → P (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) 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 (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
p : R[X]
h : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (p * X).degree
h0 : ¬0 < p.degree
rw :
  ∀ (h0' : 0 < (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) X).degree)
    (h0 : ¬0 < p.degree), P (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) X)
⊢ P (p * X)

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

Premises used: le_of_not_gt, Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
P : R[X] → Prop
p_1 : R[X]
h0_1 : 0 < p_1.degree
hC : ∀ {a : R}, a ≠ 0 → P (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) 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 (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
p : R[X]
h_1 : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) X).degree
h0 : ¬0 < p.degree
h : p.coeff 0 = 0
⊢ False

Tactic:
simp [h] at h0'
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
P : R[X] → Prop
p_1 : R[X]
h0_1 : 0 < p_1.degree
hC : ∀ {a : R}, a ≠ 0 → P (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) 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 (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
p : R[X]
h : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) X).degree
h0 : ¬0 < p.degree
⊢ P (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) X)

Tactic:
exact hC fun h : coeff p 0 = 0 => by simp [h] at h0'
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
suffices : f.natDegree = 0 ∨ M f
⊢ M f

Tactic:
suffices f.natDegree = 0 ∨ M f from Or.recOn this (fun h => (f0 h).elim) id
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
⊢ f.natDegree = 0 ∨ M f

Tactic:
Polynomial.induction_on f ?_ ?_ ?_

Premises used: Polynomial.induction_on
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
refine_1 : ∀ (a : R), natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0 ∨ M ((C : (a : R) → R[X]) a)
refine_2 : ∀ (p q : R[X]), p.natDegree = 0 ∨ M p → q.natDegree = 0 ∨ M q → (p + q).natDegree = 0 ∨ M (p + q)
refine_3 :
  ∀ (n : ℕ) (a : R),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
        M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
        M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
⊢ f.natDegree = 0 ∨ M f

Tactic:
refine Polynomial.induction_on f ?_ ?_ ?_
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
⊢ ∀ (a : R), natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0 ∨ M ((C : (a : R) → R[X]) a)

Tactic:
fun a => Or.inl (natDegree_C _)

Premises used: Polynomial.natDegree_C, Or.inl
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
⊢ ∀ (a : R), natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0 ∨ M ((C : (a : R) → R[X]) a)

Tactic:
exact fun a => Or.inl (natDegree_C _)

Premises used: Polynomial.natDegree_C, Or.inl
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
Or.inl ?_

Premises used: Or.inl
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
refine_2 : (p + q).natDegree = 0
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
refine Or.inl ?_

Premises used: Or.inl
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
refine_2 : (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) q).natDegree = 0
refine_2₁ :
  (HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
        ((C : (a : R) → R[X]) (q.coeff 0) : R[X])).natDegree =
    0
refine_2₂ : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0 + q.coeff 0)) = 0
refine_2₃ refine_2₄ : Eq (α := ℕ) 0 0
⊢ (p + q).natDegree = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]

Premises used: Polynomial.natDegree_C, Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.C_add
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : p.natDegree = 0
hq : M q
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : p.natDegree = 0
hq : M q
refine_2 : M (p + q)
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
refine Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : p.natDegree = 0
hq : M q
refine_2 : M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) q)
⊢ M (p + q)

Tactic:
rw [eq_C_of_natDegree_eq_zero hp]

Premises used: Polynomial.eq_C_of_natDegree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : p.natDegree = 0
hq : M q
⊢ M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) q)

Tactic:
h_C_add hq
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : p.natDegree = 0
hq : M q
⊢ M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) q)

Tactic:
exact h_C_add hq
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : M p
hq : q.natDegree = 0
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : M p
hq : q.natDegree = 0
refine_2 : M (p + q)
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
refine Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : M p
hq : q.natDegree = 0
refine_2 : M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) p)
⊢ M (p + q)

Tactic:
rw [eq_C_of_natDegree_eq_zero hq, add_comm]

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, add_comm
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : M p
hq : q.natDegree = 0
⊢ M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) p)

Tactic:
h_C_add hp
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : M p
hq : q.natDegree = 0
⊢ M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) p)

Tactic:
exact h_C_add hp
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : M p
hq : M q
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
Or.inr (h_add hp hq)

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
p q : R[X]
hp : M p
hq : M q
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
exact Or.inr (h_add hp hq)

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
refine_3 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
      M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
      M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
      M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
      M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))

Tactic:
_