awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
inr : Ioc n.succ p.natDegree = Icc (n + 1 + 1) p.natDegree
⊢ Eq.{u + 1} (α := R) (∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x)
    (∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i))
have inr₁ : ∀ (i : ℕ) (hi : i ∈ Icc (n + 1 + 1) p.natDegree),
  a ^ (i - (n + 1)) * p.coeff i = a * (a ^ (i - (n + 1 + 1)) * p.coeff i)
Tactic: refine sum_congr ?_ fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ Ioc n.succ p.natDegree = Icc (n + 1 + 1) p.natDegree
have inr : ∀ (a : ℕ), a ∈ Ioc n.succ p.natDegree ↔ a ∈ Icc (n + 1 + 1) p.natDegree
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1)) * p.coeff i = a * (a ^ (i - (n + 1 + 1)) * p.coeff i)
have inr : 1 ≤ i - (n + 1)
Tactic: rw [← mul_assoc, ← pow_succ', eq_comm, i.sub_succ', Nat.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ 1 ≤ i - (n + 1)
have inr : 1 + (n + 1) ≤ i
Tactic: apply Nat.le_sub_of_add_le
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ 1 + (n + 1) ≤ i
have inr : n + 1 + 1 ≤ i
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
    ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
have rw : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
Tactic: rw [Icc_eq_empty (Nat.lt_succ_iff.mpr h).not_ge, sum_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
have a₁ : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
have pos : ∀ (hp : p.natDegree = 0), (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
Tactic: by_cases hp : p.natDegree = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
pos : ∀ (hp : p.natDegree = 0), (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
have neg : ∀ (hp : ¬p.natDegree = 0), (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
Tactic: by_cases hp : p.natDegree = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : p.natDegree = 0
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
have pos : p.degree < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree
Tactic: rw [(divByMonic_eq_zero_iff <| monic_X_sub_C a).mpr, coeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : p.natDegree = 0
⊢ p.degree < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree
have pos : p.natDegree < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree
Tactic: apply degree_lt_degree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : p.natDegree = 0
⊢ p.natDegree < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree
have pos : LT.lt (α := ℕ) 0 1
Tactic: rw [hp, natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : ¬p.natDegree = 0
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
have neg : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree < n
Tactic: apply coeff_eq_zero_of_natDegree_lt
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : ¬p.natDegree = 0
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree < n
have neg : p.natDegree - 1 < n
Tactic: rw [natDegree_divByMonic p (monic_X_sub_C a), natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
⊢ ¬IsField.{u} R[X]
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
h0 : p ≠ 0
⊢ FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p
have this : Nontrivial R
Tactic: haveI := Nontrivial.of_polynomial_ne h0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p
have refine : 0 < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree
Tactic: refine finiteMultiplicity_of_degree_pos_of_monic ?_ (monic_X_sub_C _) h0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree
have rw : LT.lt (α := WithBot ℕ) 0 1
Tactic: rw [degree_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
p0 : p ≠ 0
a : R
inst_1 : DecidablePred fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p
⊢ (if h0 : p = 0 then 0
    else
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯) =
    Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯
have rw : Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) sorry =
  Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) sorry
Tactic: rw [dif_neg p0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : DecidableEq R
p : R[X]
a : R
⊢ rootMultiplicity a p =
    if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p
have simp : Eq (α := ℕ)
  (if h : p = 0 then 0
  else
    Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) sorry)
  (if p = 0 then 0
  else
    WithTop.untopD 1
      (if h : FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p then
        (↑(Nat.find (p := fun (n : ℕ) ↦
              ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) h) :
          ℕ∞)
      else ⊤))
Tactic: simp only [rootMultiplicity, multiplicity, emultiplicity]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : DecidableEq R
p : R[X]
a : R
⊢ Eq (α := ℕ)
    (if h : p = 0 then 0
    else
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯)
    (if p = 0 then 0
    else
      WithTop.untopD 1
        (if h : FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p then
          (↑(Nat.find (p := fun (n : ℕ) ↦
                ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) h) :
            ℕ∞)
        else ⊤))
have isTrue : p = 0 → Eq (α := ℕ) 0 0
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : DecidableEq R
p : R[X]
a : R
isTrue : p = 0 → Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ)
    (if h : p = 0 then 0
    else
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯)
    (if p = 0 then 0
    else
      WithTop.untopD 1
        (if h : FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p then
          (↑(Nat.find (p := fun (n : ℕ) ↦
                ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) h) :
            ℕ∞)
        else ⊤))
have isFalse : ∀ (h : ¬p = 0),
  Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) sorry =
    WithTop.untopD 1
      (if h : FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p then
        (↑(Nat.find (p := fun (n : ℕ) ↦
              ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) h) :
          ℕ∞)
      else ⊤)
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯ =
    WithTop.untopD 1
      (if h : FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p then
        (↑(Nat.find (p := fun (n : ℕ) ↦
              ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) h) :
          ℕ∞)
      else ⊤)
have isFalse : Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) sorry =
  WithTop.untopD 1
    (↑(Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
          sorry) :
      ℕ∞)
Tactic: simp only [finiteMultiplicity_X_sub_C a h, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
r a : R
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
have inl : Subsingleton R → rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
r a : R
inl : Subsingleton R → rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
have inr : Nontrivial R → rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
r a : R
h : Subsingleton R
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
have inl : rootMultiplicity a 0 = 0
Tactic: rw [Subsingleton.elim (C r) 0, rootMultiplicity_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
r a : R
h : Subsingleton R
inl : rootMultiplicity a 0 = 0
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
have inl₁ : Eq (α := ℕ) 0 0
Tactic: rw [Subsingleton.elim (C r) 0, rootMultiplicity_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
have inr : (if Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) then 0
  else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r)) =
  0
Tactic: rw [rootMultiplicity_eq_multiplicity]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
⊢ (if Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r)) =
    0
have pos : ∀ (hr : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])), Eq (α := ℕ) 0 0
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
pos : ∀ (hr : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])), Eq (α := ℕ) 0 0
⊢ (if Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r)) =
    0
have neg : ∀ (hr : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])),
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r) = 0
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
hr : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])
⊢ multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r) = 0
have h : natDegree.{u} (R := R) ((C : (a : R) → R[X]) r) <
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree
Tactic: have h : natDegree (C r) < natDegree (X - C a) := by simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
have inr : (if Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) then 0
  else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r)) =
  0
Tactic: classical
  rw [rootMultiplicity_eq_multiplicity]
  split_ifs with hr
  · rfl
  have h : natDegree (C r) < natDegree (X - C a) := by simp
  simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
inr inr₁ inr₂ :
  (if Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r)) =
    0
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
have pos : ∀ (hr : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])), Eq (α := ℕ) 0 0
Tactic: classical
  rw [rootMultiplicity_eq_multiplicity]
  split_ifs with hr
  · rfl
  have h : natDegree (C r) < natDegree (X - C a) := by simp
  simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
inr inr₁ inr₂ :
  (if Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r)) =
    0
pos : ∀ (hr : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])), Eq (α := ℕ) 0 0
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
have neg : ∀ (hr : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])),
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r) = 0
Tactic: classical
  rw [rootMultiplicity_eq_multiplicity]
  split_ifs with hr
  · rfl
  have h : natDegree (C r) < natDegree (X - C a) := by simp
  simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
inr inr₁ inr₂ :
  (if Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r)) =
    0
pos : ∀ (hr : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])), Eq (α := ℕ) 0 0
neg neg₁ :
  ∀ (hr : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])),
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r) = 0
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
have neg₂ : ∀ (hr : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]))
  (h :
    natDegree.{u} (R := R) ((C : (a : R) → R[X]) r) <
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree),
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r) = 0
Tactic: classical
  rw [rootMultiplicity_eq_multiplicity]
  split_ifs with hr
  · rfl
  have h : natDegree (C r) < natDegree (X - C a) := by simp
  simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p ∣ p
have rw : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p ∣
  p
Tactic: rw [rootMultiplicity_eq_multiplicity, if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p ∣ p
have rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
    if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p) ∣
  p
Tactic: classical
    rw [rootMultiplicity_eq_multiplicity, if_neg h]; apply pow_multiplicity_dvd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
rw :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
      if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p) ∣
    p
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p ∣ p
have rw₁ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p ∣
  p
Tactic: classical
    rw [rootMultiplicity_eq_multiplicity, if_neg h]; apply pow_multiplicity_dvd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) =
    p
have this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).Monic
Tactic: have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_X_sub_C _).pow _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).Monic
| p
have rw : 0 +
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p)
Tactic: rw [← modByMonic_add_div p, (modByMonic_eq_zero_iff_dvd this).2 (pow_rootMultiplicity_dvd _ _)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).Monic
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) =
    p
have conv_rhs : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) =
  0 +
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p)
Tactic: conv_rhs =>
    rw [← modByMonic_add_div p, (modByMonic_eq_zero_iff_dvd this).2 (pow_rootMultiplicity_dvd _ _)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ (q : R[X]),
    p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q ∧
      ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
have rw : ∃ (q : R[X]),
  p =
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
          multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p *
        q ∧
    ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
Tactic: rw [rootMultiplicity_eq_multiplicity, if_neg hp]