awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
x x_1 : R[X]
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ∣ x * x_1 →
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ∣ x ∨
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ∣ x_1
have simp_rw : eval r x = 0 ∨ eval r x_1 = 0 → eval r x = 0 ∨ eval r x_1 = 0
Tactic: simp_rw [dvd_iff_isRoot, IsRoot.def, eval_mul, mul_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ Prime.{u} (M := R[X]) X
have h : X = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)
Tactic: convert! prime_X_sub_C (0 : R)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
h : IsUnit p
⊢ False
have obtain : ∀ (u : R) (h : (C : (a : R) → R[X]) u = p), False
Tactic: obtain ⟨u, -, h⟩ := isUnit_iff.mp h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
h_1 : IsUnit p
u : R
h : (C : (a : R) → R[X]) u = p
⊢ False
have apply : LE.le (α := WithBot ℕ) 1 0
Tactic: apply not_le.mpr (zero_lt_one' (WithBot ℕ))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
⊢ IsUnit f ∨ IsUnit g
have inr : ∀ (this : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g) (H : g.degree < f.degree),
  IsUnit f ∨ IsUnit g
Tactic: wlog! H : f.degree ≤ g.degree generalizing f g
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
inr :
  ∀ (this : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g) (H : g.degree < f.degree),
    IsUnit f ∨ IsUnit g
⊢ IsUnit f ∨ IsUnit g
have wlog! : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g
Tactic: wlog! H : f.degree ≤ g.degree generalizing f g
Cleared hypotheses: f, g, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
this : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g
H : g.degree < f.degree
⊢ IsUnit f ∨ IsUnit g
have h₁ : p = g * f
Tactic: rw [mul_comm] at h
Cleared hypotheses: h, this, H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
⊢ IsUnit f ∨ IsUnit g
have h₁ : IsUnit f
Tactic: left
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
⊢ IsUnit f
have hp₁ : f.degree = 0 ∧ g.degree = 1 ∨ f.degree = 1 ∧ g.degree = 0
Tactic: rw [h, degree_mul, Nat.WithBot.add_eq_one_iff] at hp
Cleared hypotheses: hp, h, H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
hp : f.degree = 0 ∧ g.degree = 1 ∨ f.degree = 1 ∧ g.degree = 0
h : p = f * g
H : f.degree ≤ g.degree
⊢ IsUnit f
have h₁ : ∀ (hf : f.degree = 0) (hg : g.degree = 1), IsUnit f
Tactic: rcases hp with ⟨hf, hg⟩ | ⟨hf, hg⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
hp : f.degree = 0 ∧ g.degree = 1 ∨ f.degree = 1 ∧ g.degree = 0
h : p = f * g
H : f.degree ≤ g.degree
h₁ : ∀ (hf : f.degree = 0) (hg : g.degree = 1), IsUnit f
⊢ IsUnit f
have h₂ : ∀ (hf : f.degree = 1) (hg : g.degree = 0), IsUnit f
Tactic: rcases hp with ⟨hf, hg⟩ | ⟨hf, hg⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 0
hg : g.degree = 1
⊢ IsUnit f
have hf₁ : f = (C : (a : R) → R[X]) (f.coeff 0)
Tactic: replace hf := f.eq_C_of_degree_eq_zero hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
⊢ IsUnit f
have h₁ : IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
⊢ IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
have h₁ : IsUnit (f.coeff 0)
Tactic: apply IsUnit.map C
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
⊢ IsUnit (f.coeff 0)
have hc₁ : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
Tactic: rw [h, hf, coeff_C_mul, coeff_C_mul] at hc
Cleared hypotheses: hc, h, H, hg, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
⊢ IsUnit (f.coeff 0)
have h₁ : f.coeff 0 ∣ f.coeff 0 * g.coeff 0
Tactic: apply hc
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
h₁ : f.coeff 0 ∣ f.coeff 0 * g.coeff 0
⊢ IsUnit (f.coeff 0)
have h₂ : f.coeff 0 ∣ f.coeff 0 * g.coeff 1
Tactic: apply hc
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ Irreducible
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X]))
have hp : (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])).degree =
  1
Tactic: apply irreducible_of_degree_eq_one_of_isRelPrime_coeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
hp :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).degree =
    1
⊢ Irreducible
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X]))
have hc : IsRelPrime
  ((HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).coeff
    0)
  ((HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).coeff
    1)
Tactic: apply irreducible_of_degree_eq_one_of_isRelPrime_coeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).degree =
    1
have hp : ((if WithBot.unbotD 0 1 = HAdd.hAdd (α := ℕ) 0 1 then
      (if Eq (α := ℕ) 0 0 then a else 0) * if Eq (α := ℕ) 1 1 then 1 else 0
    else 0) +
    if Eq (α := ℕ) (WithBot.unbotD 0 1) 0 then b else 0) ≠
  0
Tactic: compute_degree!
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
hp :
  ((if WithBot.unbotD 0 1 = HAdd.hAdd (α := ℕ) 0 1 then
        (if Eq (α := ℕ) 0 0 then a else 0) * if Eq (α := ℕ) 1 1 then 1 else 0
      else 0) +
      if Eq (α := ℕ) (WithBot.unbotD 0 1) 0 then b else 0) ≠
    0
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).degree =
    1
have hp₁ : HAdd.hAdd (α := ℕ) 0 1 ≤ WithBot.unbotD 0 1
Tactic: compute_degree!
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
S : Type v
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial S
inst_2 : Semiring S
inst_3 : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
⊢ Ne.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S) ∨
    Ne.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
have by_contra! : ∀ (hp : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S))
  (hq : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)), False
Tactic: by_contra! ⟨hp, hq⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
S : Type v
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial S
inst_2 : Semiring S
inst_3 : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
hp : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
hq : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
⊢ False
have rcases : ∀ (w w_1 : R[X]) (h : w * p + w_1 * q = 1), False
Tactic: rcases h with ⟨_, _, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (hypothesis)
Goal:
S : Type v
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial S
inst_2 : Semiring S
inst_3 : Algebra R S
p q : R[X]
s : S
hp : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
hq : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
w w_1 : R[X]
h : w * p + w_1 * q = 1
⊢ False
have h₁ : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) (w * p + w_1 * q) : S) ((aeval s : (a : R[X]) → S) 1 : S)
Tactic: apply_fun aeval s at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
h : IsUnit (a - b)
⊢ HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])) =
    1
have rw : Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑h.unit⁻¹ : R) * (a - b)) : R[X]) (1 : R[X])
Tactic: rw [neg_mul_comm, ← left_distrib, neg_add_eq_sub, sub_sub_sub_cancel_left, ← C_sub, ← C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
h : IsUnit (a - b)
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑h.unit⁻¹ : R) * (a - b)) : R[X]) ((C : (a : R) → R[X]) 1 : R[X])
have h₁ : (↑h.unit⁻¹ : R) * (a - b) = 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have hp : p ≠ 0
Tactic: have hp : p ≠ 0 := left_ne_zero_of_mul hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have hq : q ≠ 0
Tactic: have hq : q ≠ 0 := right_ne_zero_of_mul hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have rw : (if p * q = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q)) =
  rootMultiplicity x p + rootMultiplicity x q
Tactic: rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw :
  (if p * q = 0 then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q)) =
    rootMultiplicity x p + rootMultiplicity x q
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have rw₁ : multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
  rootMultiplicity x p + rootMultiplicity x q
Tactic: rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw :
  (if p * q = 0 then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q)) =
    rootMultiplicity x p + rootMultiplicity x q
rw₁ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    rootMultiplicity x p + rootMultiplicity x q
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have rw₂ : multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
  (if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p) +
    rootMultiplicity x q
Tactic: rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw :
  (if p * q = 0 then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q)) =
    rootMultiplicity x p + rootMultiplicity x q
rw₁ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    rootMultiplicity x p + rootMultiplicity x q
rw₂ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    (if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p) +
      rootMultiplicity x q
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have rw₃ : multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p + rootMultiplicity x q
Tactic: rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw :
  (if p * q = 0 then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q)) =
    rootMultiplicity x p + rootMultiplicity x q
rw₁ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    rootMultiplicity x p + rootMultiplicity x q
rw₂ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    (if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p) +
      rootMultiplicity x q
rw₃ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p + rootMultiplicity x q
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have rw₄ : multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p +
    if q = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) q
Tactic: rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw :
  (if p * q = 0 then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q)) =
    rootMultiplicity x p + rootMultiplicity x q
rw₁ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    rootMultiplicity x p + rootMultiplicity x q
rw₂ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    (if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p) +
      rootMultiplicity x q
rw₃ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p + rootMultiplicity x q
rw₄ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p +
      if q = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) q
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have rw₅ : multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p +
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) q
Tactic: rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw :
  (if p * q = 0 then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q)) =
    rootMultiplicity x p + rootMultiplicity x q
rw₁ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    rootMultiplicity x p + rootMultiplicity x q
rw₂ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    (if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p) +
      rootMultiplicity x q
rw₃ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p + rootMultiplicity x q
rw₄ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p +
      if q = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) q
rw₅ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p +
      multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) q
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have rw₆ : multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p +
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) q =
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p +
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) q
Tactic: rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have have : ∀ (hp : p ≠ 0), rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
Tactic: classical
  have hp : p ≠ 0 := left_ne_zero_of_mul hpq
  have hq : q ≠ 0 := right_ne_zero_of_mul hpq
  rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
have have₁ have₂ : ∀ (hp : p ≠ 0), rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have have₃ : ∀ (hp : p ≠ 0) (hq : q ≠ 0), rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
Tactic: classical
  have hp : p ≠ 0 := left_ne_zero_of_mul hpq
  have hq : q ≠ 0 := right_ne_zero_of_mul hpq
  rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h_1 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) = 0
⊢ False
have hp₁ : Ne.{u + 1} (α := R[X]) 0 0
Tactic: rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, mul_zero] at hp
Cleared hypotheses: hp, hx, hpd, h