awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
n : ℕ
chn : Ne.{u + 1} (α := R) (↑n : R) 0
a : R[X]
inst_2 : Nontrivial R
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (a ^ n) : R[X]) (0 : R[X]) ↔
    Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])
have rw : ∀ (chn : Ne.{u + 1} (α := R[X]) (↑n : R[X]) 0) {a : R[X]},
  Nontrivial R →
    (Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (a ^ n) : R[X]) (0 : R[X]) ↔
      Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X]))
Tactic: rw [← C_ne_zero, C_eq_natCast] at chn
Cleared hypotheses: chn, a, inst_2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
h : X ∣ f
g : R[X]
hfg : f = X * g
⊢ f.coeff 0 = 0
have rw : (X * g).coeff 0 = 0
Tactic: rw [hfg, coeff_X_mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
h : X ∣ f
g : R[X]
hfg : f = X * g
rw : (X * g).coeff 0 = 0
⊢ f.coeff 0 = 0
have rw₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [hfg, coeff_X_mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
hf : f.coeff 0 = 0
⊢ f = X * f.divX
have rw : f = X * f.divX + 0
Tactic: rw [← add_zero (X * f.divX), ← C_0, ← hf, X_mul_divX_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
hf : f.coeff 0 = 0
rw : f = X * f.divX + 0
⊢ f = X * f.divX
have rw₁ : f = X * f.divX + (C : (a : R) → R[X]) 0
Tactic: rw [← add_zero (X * f.divX), ← C_0, ← hf, X_mul_divX_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
hf : f.coeff 0 = 0
rw : f = X * f.divX + 0
rw₁ : f = X * f.divX + (C : (a : R) → R[X]) 0
⊢ f = X * f.divX
have rw₂ : f = HAdd.hAdd (β := R[X]) (X * f.divX) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
Tactic: rw [← add_zero (X * f.divX), ← C_0, ← hf, X_mul_divX_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
hf : f.coeff 0 = 0
rw : f = X * f.divX + 0
rw₁ : f = X * f.divX + (C : (a : R) → R[X]) 0
rw₂ : f = HAdd.hAdd (β := R[X]) (X * f.divX) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
⊢ f = X * f.divX
have rw₃ : f = f
Tactic: rw [← add_zero (X * f.divX), ← C_0, ← hf, X_mul_divX_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
⊢ HPow.hPow (α := R[X]) X (n + 1) ∣ f
have succ : ∀ (g : R[X]) (hgf : f = HPow.hPow (α := R[X]) X n * g), HPow.hPow (α := R[X]) X (n + 1) ∣ f
Tactic: obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
⊢ HPow.hPow (α := R[X]) X (n + 1) ∣ f
have this : (HPow.hPow (α := R[X]) X n * g).coeff (0 + n) = g.coeff 0
Tactic: have := coeff_X_pow_mul g n 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
this : (HPow.hPow (α := R[X]) X n * g).coeff (0 + n) = g.coeff 0
⊢ HPow.hPow (α := R[X]) X (n + 1) ∣ f
have this₁ : 0 = g.coeff 0
Tactic: rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
this : 0 = g.coeff 0
⊢ HPow.hPow (α := R[X]) X (n + 1) ∣ f
have succ : ∀ (k : R[X]) (hgk : g = X * k), HPow.hPow (α := R[X]) X (n + 1) ∣ f
Tactic: obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ HPow.hPow (α := R[X]) X (n + 1) ∣ f
have h : f = HPow.hPow (α := R[X]) X (n + 1) * k
Tactic: use k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ f = HPow.hPow (α := R[X]) X (n + 1) * k
have h : f = HPow.hPow (α := R[X]) X n * X * k
Tactic: rwa [pow_succ, mul_assoc, ← hgk]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
h : f = HPow.hPow (α := R[X]) X n * X * k
⊢ f = HPow.hPow (α := R[X]) X (n + 1) * k
have h₁ : f = HPow.hPow (α := R[X]) X n * (X * k)
Tactic: rwa [pow_succ, mul_assoc, ← hgk]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hd : ∀ d < n, f.coeff d = 0
⊢ HPow.hPow (α := R[X]) X n ∣ f
have zero : ∀ (hd : ∀ d < 0, f.coeff d = 0), HPow.hPow (α := R[X]) (β := ℕ) X 0 ∣ f
Tactic: induction n with
    | zero => simp [pow_zero]
    | succ n hn =>
      obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
      have := coeff_X_pow_mul g n 0
      rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
      obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
      use k
      rwa [pow_succ, mul_assoc, ← hgk]
Cleared hypotheses: n, hd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hd : ∀ d < n, f.coeff d = 0
zero : ∀ (hd : ∀ d < 0, f.coeff d = 0), HPow.hPow (α := R[X]) (β := ℕ) X 0 ∣ f
⊢ HPow.hPow (α := R[X]) X n ∣ f
have succ : ∀ (n : ℕ) (hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f) (hd : ∀ d < n + 1, f.coeff d = 0),
  HPow.hPow (α := R[X]) X (n + 1) ∣ f
Tactic: induction n with
    | zero => simp [pow_zero]
    | succ n hn =>
      obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
      have := coeff_X_pow_mul g n 0
      rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
      obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
      use k
      rwa [pow_succ, mul_assoc, ← hgk]
Cleared hypotheses: n, hd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
⊢ False
have hp0 : p ≠ 0
Tactic: have hp0 : p ≠ 0 := fun hp0 => by simp [hp0] at hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r = 0
⊢ False
have hr₁ : q = p ^ (q.natDegree + 1) * 0
Tactic: subst hr0
Cleared hypotheses: r, hr, hr0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
⊢ False
have hr0 : r ≠ 0
Tactic: have hr0 : r ≠ 0 := fun hr0 => by subst hr0; simp [hq] at hr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
⊢ False
have hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
Tactic: have hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1 := by simp [show _ = _ from hmp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
⊢ False
have hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
Tactic: have hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0 := hpn1.symm ▸ zn0.symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
⊢ False
have hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
Tactic: have hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0 := by
      simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_mul, Ne,
          hr0, not_false_eq_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ LT.lt (α := WithBot ℕ) (↑0 : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
have rw : (↑0 : WithBot ℕ) < p.degree
Tactic: rw [← degree_eq_natDegree hp0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ False
have hnp : 0 < p.natDegree
Tactic: have hnp : 0 < natDegree p := Nat.cast_lt.1 <| by
      rw [← degree_eq_natDegree hp0]; exact hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
⊢ False
have this : q.natDegree = (p ^ (q.natDegree + 1) * r).natDegree
Tactic: have := congr_arg natDegree hr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
this : q.natDegree = (p ^ (q.natDegree + 1) * r).natDegree
⊢ False
have this₁ : q.natDegree = q.natDegree * p.natDegree + (1 * p.natDegree + r.natDegree)
Tactic: rw [natDegree_mul' hpnr0, natDegree_pow' hpn0', add_mul, add_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
have obtain : ∀ (r : R[X]) (hdeg : (p * r).natDegree ≤ p.natDegree),
  p * r = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * r).leadingCoeff : R[X])
Tactic: obtain ⟨r, rfl⟩ := hdvd
Cleared hypotheses: q, hdvd, hdeg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
⊢ p * r = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * r).leadingCoeff : R[X])
have inl : ∀ (hdeg : (p * 0).natDegree ≤ p.natDegree),
  p * 0 = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * 0).leadingCoeff : R[X])
Tactic: obtain rfl | hr := eq_or_ne r 0
Cleared hypotheses: r, hdeg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
inl :
  ∀ (hdeg : (p * 0).natDegree ≤ p.natDegree),
    p * 0 = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * 0).leadingCoeff : R[X])
⊢ p * r = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * r).leadingCoeff : R[X])
have inr : ∀ (hr : r ≠ 0), p * r = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * r).leadingCoeff : R[X])
Tactic: obtain rfl | hr := eq_or_ne r 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
⊢ p * r = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * r).leadingCoeff : R[X])
have this : r.natDegree = 0
Tactic: have : r.natDegree = 0 := by simpa [hp.natDegree_mul' hr] using hdeg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
this : r.natDegree = 0
⊢ p * r = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * r).leadingCoeff : R[X])
have inr : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (r.coeff 0) : R[X]) =
  HMul.hMul (β := R[X]) p
    ((C : (a : R) → R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (r.coeff 0) : R[X])).leadingCoeff : R[X])
Tactic: rw [eq_C_of_natDegree_eq_zero this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = p
have rw : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) q.leadingCoeff : R[X]) = p
Tactic: rw [eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le hp hdvd hdeg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ LE.le (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
have rw : q.degree ≤ p.degree
Tactic: rw [← degree_eq_natDegree h.2, ← degree_eq_natDegree hq0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.degree =
    (q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree
have rw : p.degree =
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) *
      q).degree
Tactic: rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
        degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
rw :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) *
        q).degree
⊢ p.degree =
    (q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree
have rw₁ : p.degree =
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree +
    q.degree
Tactic: rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
        degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
rw :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) *
        q).degree
rw₁ :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree +
      q.degree
⊢ p.degree =
    (q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree
have rw₂ : p.degree = (↑(p.natDegree - q.natDegree) : WithBot ℕ) + q.degree
Tactic: rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
        degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
rw :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) *
        q).degree
rw₁ :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree +
      q.degree
rw₂ : p.degree = (↑(p.natDegree - q.natDegree) : WithBot ℕ) + q.degree
⊢ p.degree =
    (q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree
have rw₃ : (↑p.natDegree : WithBot ℕ) = (↑(p.natDegree - q.natDegree) : WithBot ℕ) + q.degree
Tactic: rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
        degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
rw :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) *
        q).degree
rw₁ :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree +
      q.degree
rw₂ : p.degree = (↑(p.natDegree - q.natDegree) : WithBot ℕ) + q.degree
rw₃ : (↑p.natDegree : WithBot ℕ) = (↑(p.natDegree - q.natDegree) : WithBot ℕ) + q.degree
⊢ p.degree =
    (q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree
have rw₄ : (↑p.natDegree : WithBot ℕ) =
  HAdd.hAdd (α := WithBot ℕ) (↑(p.natDegree - q.natDegree) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
        degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
rw :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) *
        q).degree
rw₁ :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree +
      q.degree
rw₂ : p.degree = (↑(p.natDegree - q.natDegree) : WithBot ℕ) + q.degree
rw₃ : (↑p.natDegree : WithBot ℕ) = (↑(p.natDegree - q.natDegree) : WithBot ℕ) + q.degree
rw₄ :
  (↑p.natDegree : WithBot ℕ) =
    HAdd.hAdd (α := WithBot ℕ) (↑(p.natDegree - q.natDegree) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
⊢ p.degree =
    (q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree
have rw₅ : Eq (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(p.natDegree - q.natDegree + q.natDegree) : WithBot ℕ)
Tactic: rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
        degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
rw :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) *
        q).degree
rw₁ :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree +
      q.degree
rw₂ : p.degree = (↑(p.natDegree - q.natDegree) : WithBot ℕ) + q.degree
rw₃ : (↑p.natDegree : WithBot ℕ) = (↑(p.natDegree - q.natDegree) : WithBot ℕ) + q.degree
rw₄ :
  (↑p.natDegree : WithBot ℕ) =
    HAdd.hAdd (α := WithBot ℕ) (↑(p.natDegree - q.natDegree) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
rw₅ : Eq (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(p.natDegree - q.natDegree + q.natDegree) : WithBot ℕ)
⊢ p.degree =
    (q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree
have rw₆ : Eq (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
Tactic: rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
        degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.leadingCoeff =
    (q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).leadingCoeff
have rw : p.leadingCoeff =
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
      (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).leadingCoeff
Tactic: rw [leadingCoeff_monic_mul hq, leadingCoeff_mul_X_pow, leadingCoeff_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
rw :
  p.leadingCoeff =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).leadingCoeff
⊢ p.leadingCoeff =
    (q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).leadingCoeff
have rw₁ : p.leadingCoeff = leadingCoeff ((C : (a : R) → R[X]) p.leadingCoeff)
Tactic: rw [leadingCoeff_monic_mul hq, leadingCoeff_mul_X_pow, leadingCoeff_C]