awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X])
        (if n = 0 then 0 else HPow.hPow (α := R[X]) X (n - 1))).natDegree =
    n - 1
have pos : ∀ (n0 : n = 0), (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) (0 : R[X])).natDegree = n - 1
Tactic: split_ifs with n0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
pos : ∀ (n0 : n = 0), (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) (0 : R[X])).natDegree = n - 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X])
        (if n = 0 then 0 else HPow.hPow (α := R[X]) X (n - 1))).natDegree =
    n - 1
have neg : ∀ (n0 : ¬n = 0),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X (n - 1))).natDegree = n - 1
Tactic: split_ifs with n0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
⊢ p.divX.degree < p.degree
have this : Nontrivial R
Tactic: haveI := Nontrivial.of_polynomial_ne hp0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
⊢ p.divX.degree < (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
have h' : Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
Tactic: have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
⊢ p.divX.degree < (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
have rw : ⊥ < degree.{u} (R := R) ((C : (a : R) → R[X]) (coeff ((C : (a : R) → R[X]) (p.coeff 0)) 0))
Tactic: rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
⊢ p.divX.degree < (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
have hXp0 : p.divX ≠ 0
Tactic: have hXp0 : divX p ≠ 0 := by
          simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
⊢ p.divX.degree < (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
have this₁ : p.divX.leadingCoeff * leadingCoeff X ≠ 0
Tactic: have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * leadingCoeff X ≠ 0
⊢ degree.{u} (R := R) X ≤ (p.divX * X).degree
have rw : 0 + degree.{u} (R := R) X ≤ p.divX.degree + degree.{u} (R := R) X
Tactic: rw [← zero_add (degree X), degree_mul' this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * leadingCoeff X ≠ 0
⊢ 0 ≤ p.divX.degree
have rw : ¬p = (C : (a : R) → R[X]) (p.coeff 0)
Tactic: rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * leadingCoeff X ≠ 0
⊢ p.divX.degree < (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
have this₁ : degree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0)) < (p.divX * X).degree
Tactic: have : degree (C (p.coeff 0)) < degree (divX p * X) :=
          calc
            degree (C (p.coeff 0)) ≤ 0 := degree_C_le
            _ < 1 := by decide
            _ = degree (X : R[X]) := degree_X.symm
            _ ≤ degree (divX p * X) := by
              rw [← zero_add (degree X), degree_mul' this]
              exact add_le_add
                (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                    exact fun h0 => h (h0.symm ▸ degree_C_le))
                    le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this_2 : p.divX.leadingCoeff * leadingCoeff X ≠ 0
this : degree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0)) < (p.divX * X).degree
⊢ p.divX.degree < (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree
have rw : p.divX.degree < (p.divX * X).degree
Tactic: rw [degree_add_eq_left_of_degree_lt this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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
⊢ M p
have have : (wf : p.divX.degree < p.degree) → M p
Tactic: have wf : degree (divX p) < degree p := degree_divX_lt hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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
⊢ M p
have 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]))
Tactic: rw [← divX_mul_X_add p] at *
Cleared hypotheses: hp, wf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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 (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]))
have rw : M (p.divX * X)
Tactic: rw [hcp0, C_0, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (hypothesis)
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
⊢ P 0
have h₁ : LT.lt (α := WithBot ℕ) 0 ⊥
Tactic: rw [degree_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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
⊢ 0 < degree.{u} (R := R) ((C : (a : R) → R[X]) a)
have 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)
Tactic: rwa [eq_C_of_degree_le_zero h, ← C_add, heq0, zero_add] at h0
Cleared hypotheses: h0, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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)
⊢ 0 < degree.{u} (R := R) ((C : (a : R) → R[X]) a)
have 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)
Tactic: rwa [eq_C_of_degree_le_zero h, ← C_add, heq0, zero_add] at h0
Cleared hypotheses: h0, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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)
⊢ 0 < degree.{u} (R := R) ((C : (a : R) → R[X]) a)
have 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)
Tactic: rwa [eq_C_of_degree_le_zero h, ← C_add, heq0, zero_add] at h0
Cleared hypotheses: h0, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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)
⊢ 0 < degree.{u} (R := R) ((C : (a : R) → R[X]) a)
have 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)
Tactic: rwa [eq_C_of_degree_le_zero h, ← C_add, heq0, zero_add] at h0
Cleared hypotheses: h0, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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
⊢ P (p * X)
have 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)
Tactic: rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at h0' ⊢
Cleared hypotheses: h0', h0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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)
⊢ M f
have suffices : f.natDegree = 0 ∨ M f
Tactic: suffices f.natDegree = 0 ∨ M f from Or.recOn this (fun h => (f0 h).elim) id
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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
have refine_1 : ∀ (a : R), natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0 ∨ M ((C : (a : R) → R[X]) a)
Tactic: refine Polynomial.induction_on f ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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)
⊢ f.natDegree = 0 ∨ M f
have refine_2 : ∀ (p q : R[X]), p.natDegree = 0 ∨ M p → q.natDegree = 0 ∨ M q → (p + q).natDegree = 0 ∨ M (p + q)
Tactic: refine Polynomial.induction_on f ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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)
⊢ f.natDegree = 0 ∨ M f
have 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)))
Tactic: refine Polynomial.induction_on f ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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)
have refine_2 : (p + q).natDegree = 0
Tactic: refine Or.inl ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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
have refine_2 : (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) q).natDegree = 0
Tactic: rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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
⊢ (p + q).natDegree = 0
have 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
Tactic: rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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
⊢ (p + q).natDegree = 0
have refine_2₂ : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0 + q.coeff 0)) = 0
Tactic: rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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
⊢ (p + q).natDegree = 0
have refine_2₃ : Eq (α := ℕ) 0 0
Tactic: rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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)
have refine_2 : M (p + q)
Tactic: refine Or.inr ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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 (p + q)
have refine_2 : M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) q)
Tactic: rw [eq_C_of_natDegree_eq_zero hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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)
have refine_2 : M (p + q)
Tactic: refine Or.inr ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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 (p + q)
have refine_2 : M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) p)
Tactic: rw [eq_C_of_natDegree_eq_zero hq, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
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
h :
  (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)))
have pos : ∀ (a0 : a = 0),
  (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: by_cases a0 : a = 0