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
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
⊢ (↑(x ::ₘ t).card : WithBot ℕ) = HAdd.hAdd (α := WithBot ℕ) (↑t.card : WithBot ℕ) 1
have e_a : (x ::ₘ t).card = Add.add (↑t.card : ℕ) 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
⊢ HAdd.hAdd (α := WithBot ℕ) (↑t.card : WithBot ℕ) 1 ≤ p.degree
have rw : HAdd.hAdd (α := WithBot ℕ) 1 (↑t.card : WithBot ℕ) ≤
  1 + (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
Tactic: rw [← degree_add_divByMonic (monic_X_sub_C x) hdeg, degree_X_sub_C, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
| rootMultiplicity a p
have rw : rootMultiplicity a
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) *
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
Tactic: rw [← mul_divByMonic_eq_iff_isRoot.mpr hx]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a p
have conv_rhs : count a (x ::ₘ t) =
  rootMultiplicity a
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
Tactic: conv_rhs => rw [← mul_divByMonic_eq_iff_isRoot.mpr hx]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
⊢ count a (x ::ₘ t) =
    rootMultiplicity a
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
have rw : count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t
Tactic: rw [rootMultiplicity_mul (mul_ne_zero (X_sub_C_ne_zero x) hdiv0),
            rootMultiplicity_X_sub_C, ← htr a]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
⊢ count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t
have pos : ∀ (ha : a = x), count a (x ::ₘ t) = 1 + count a t
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
pos : ∀ (ha : a = x), count a (x ::ₘ t) = 1 + count a t
⊢ count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t
have neg : ∀ (ha : ¬a = x), count a (x ::ₘ t) = 0 + count a t
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
ha : a = x
⊢ count a (x ::ₘ t) = 1 + count a t
have pos : count x (x ::ₘ t) = 1 + count x t
Tactic: rw [ha, count_cons_self, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
ha : a = x
pos : count x (x ::ₘ t) = 1 + count x t
⊢ count a (x ::ₘ t) = 1 + count a t
have pos₁ : count x t + 1 = 1 + count x t
Tactic: rw [ha, count_cons_self, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
ha : a = x
pos : count x (x ::ₘ t) = 1 + count x t
pos₁ : count x t + 1 = 1 + count x t
⊢ count a (x ::ₘ t) = 1 + count a t
have pos₂ : 1 + count x t = 1 + count x t
Tactic: rw [ha, count_cons_self, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
ha : ¬a = x
⊢ count a (x ::ₘ t) = 0 + count a t
have neg : count a t = 0 + count a t
Tactic: rw [count_cons_of_ne ha, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
ha : ¬a = x
neg : count a t = 0 + count a t
⊢ count a (x ::ₘ t) = 0 + count a t
have neg₁ : count a t = count a t
Tactic: rw [count_cons_of_ne ha, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ¬∃ (x : R), p.IsRoot x
a : R
⊢ count a 0 = rootMultiplicity a p
have rw : 0 = rootMultiplicity a p
Tactic: rw [count_zero, rootMultiplicity_eq_zero (not_exists.mp h a)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
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 : ¬∃ (x : R), p.IsRoot x
a : R
rw : 0 = rootMultiplicity a p
⊢ count a 0 = rootMultiplicity a p
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [count_zero, rootMultiplicity_eq_zero (not_exists.mp h a)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
h_1 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y _x →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p_1 : R[X]
h_2 : p_1 ≠ 0
h_3 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p_1 h_2) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
h_4 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p hp) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree < p.natDegree
have apply : LT.lt (α := WithBot ℕ)
  (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
  (↑p.natDegree : WithBot ℕ)
Tactic: apply (Nat.cast_lt (α := WithBot ℕ)).mp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
h_1 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y _x →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p_1 : R[X]
h_2 : p_1 ≠ 0
h_3 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p_1 h_2) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
h_4 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p hp) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree < p.natDegree
have apply : LT.lt (α := WithBot ℕ)
  (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
  (↑p.natDegree : WithBot ℕ)
Tactic: {
  apply (Nat.cast_lt (α := WithBot ℕ)).mp
  simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0] at wf
  assumption}
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
h_1 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y _x →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p_1 : R[X]
h_2 : p_1 ≠ 0
h_3 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p_1 h_2) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
h_4 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p hp) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
apply :
  LT.lt (α := WithBot ℕ)
    (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
    (↑p.natDegree : WithBot ℕ)
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree < p.natDegree
have apply₁ : ∀
  (wf :
    LT.lt (α := WithBot ℕ)
      (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
      (↑p.natDegree : WithBot ℕ)),
  LT.lt (α := WithBot ℕ)
    (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
    (↑p.natDegree : WithBot ℕ)
Tactic: {
  apply (Nat.cast_lt (α := WithBot ℕ)).mp
  simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0] at wf
  assumption}
Cleared hypotheses: wf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
h_1 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y _x →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p_1 : R[X]
h_2 : p_1 ≠ 0
h_3 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p_1 h_2) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
h_4 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p hp) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree < p.natDegree
have decreasing_by : LT.lt (α := WithBot ℕ)
  (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
  (↑p.natDegree : WithBot ℕ)
Tactic: decreasing_by {
  apply (Nat.cast_lt (α := WithBot ℕ)).mp
  simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0] at wf
  assumption}