awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
⊢ f /ₘ g = q ∧ f %ₘ g = r
have h₅ : q - f /ₘ g = 0
Tactic: have h₅ : q - f /ₘ g = 0 :=
    _root_.by_contradiction fun hqf =>
      not_le_of_gt h₄ <|
        calc
          degree g ≤ degree g + degree (q - f /ₘ g) := by
            rw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf]
            norm_cast
            exact Nat.le_add_right _ _
          _ = degree (r - f %ₘ g) := by rw [h₂, degree_mul']; simpa [Monic.def.1 hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
have this : Nontrivial R
Tactic: haveI : Nontrivial R := f.domain_nontrivial
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this : Nontrivial R
⊢ map f p = map f (p %ₘ q) + map f q * map f (p /ₘ q)
have rw : map f p = map f (p %ₘ q) + map f (q * (p /ₘ q))
Tactic: rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this : Nontrivial R
rw : map f p = map f (p %ₘ q) + map f (q * (p /ₘ q))
⊢ map f p = map f (p %ₘ q) + map f q * map f (p /ₘ q)
have rw₁ : map f p = map f (p %ₘ q + q * (p /ₘ q))
Tactic: rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this : Nontrivial R
rw : map f p = map f (p %ₘ q) + map f (q * (p /ₘ q))
rw₁ : map f p = map f (p %ₘ q + q * (p /ₘ q))
⊢ map f p = map f (p %ₘ q) + map f q * map f (p /ₘ q)
have rw₂ : map f p = map f p
Tactic: rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this : Nontrivial R
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) q.leadingCoeff : S) (0 : S)
have rw : Ne.{v + 1} (α := S) 1 0
Tactic: rw [Monic.def.1 hq, f.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this : Nontrivial R
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
have this₁ : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q)
Tactic: have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q) :=
    div_modByMonic_unique ((p /ₘ q).map f) _ (hq.map f)
      ⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div],
        calc
          _ ≤ degree (p %ₘ q) := degree_map_le
          _ < degree q := degree_modByMonic_lt _ hq
          _ = _ :=
            Eq.symm <|
              degree_map_eq_of_leadingCoeff_ne_zero _
                (by rw [Monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : p %ₘ q = 0
⊢ q ∣ p
have rw : q ∣ q * (p /ₘ q)
Tactic: rw [← modByMonic_add_div p q, h, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
⊢ p %ₘ q = 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 q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
⊢ p %ₘ q = 0
have obtain : ∀ (r : R[X]) (hr : p = q * r), p %ₘ q = 0
Tactic: obtain ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
⊢ p %ₘ q = 0
have by_contra : ∀ (hpq0 : ¬p %ₘ q = 0), False
Tactic: by_contra hpq0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ p %ₘ q = q * (r - p /ₘ q)
have rw : p - q * (p /ₘ q) = q * (r - p /ₘ q)
Tactic: rw [modByMonic_eq_sub_mul_div, mul_sub, ← hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
rw : p - q * (p /ₘ q) = q * (r - p /ₘ q)
⊢ p %ₘ q = q * (r - p /ₘ q)
have rw₁ : p - q * (p /ₘ q) = q * r - q * (p /ₘ q)
Tactic: rw [modByMonic_eq_sub_mul_div, mul_sub, ← hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
rw : p - q * (p /ₘ q) = q * (r - p /ₘ q)
rw₁ : p - q * (p /ₘ q) = q * r - q * (p /ₘ q)
⊢ p %ₘ q = q * (r - p /ₘ q)
have rw₂ : p - q * (p /ₘ q) = p - q * (p /ₘ q)
Tactic: rw [modByMonic_eq_sub_mul_div, mul_sub, ← hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ False
have hmod : p %ₘ q = q * (r - p /ₘ q)
Tactic: have hmod : p %ₘ q = q * (r - p /ₘ q) := by rw [modByMonic_eq_sub_mul_div, mul_sub, ← hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
⊢ False
have this : (q * (r - p /ₘ q)).degree < q.degree
Tactic: have : degree (q * (r - p /ₘ q)) < degree q := hmod ▸ degree_modByMonic_lt _ hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h_1 : q ∣ p
h_2 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
⊢ (p %ₘ q).leadingCoeff = 0
have rw : (q * (r - p /ₘ q)).leadingCoeff = 0
Tactic: rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h_1 : q ∣ p
h_2 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
rw : (q * (r - p /ₘ q)).leadingCoeff = 0
⊢ (p %ₘ q).leadingCoeff = 0
have rw₁ : (q * 0).leadingCoeff = 0
Tactic: rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h_1 : q ∣ p
h_2 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
rw : (q * (r - p /ₘ q)).leadingCoeff = 0
rw₁ : (q * 0).leadingCoeff = 0
⊢ (p %ₘ q).leadingCoeff = 0
have rw₂ : Eq.{u + 1} (α := R) (leadingCoeff 0) 0
Tactic: rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h_1 : q ∣ p
h_2 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
rw : (q * (r - p /ₘ q)).leadingCoeff = 0
rw₁ : (q * 0).leadingCoeff = 0
rw₂ : Eq.{u + 1} (α := R) (leadingCoeff 0) 0
⊢ (p %ₘ q).leadingCoeff = 0
have rw₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
⊢ False
have hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
Tactic: have hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0 := fun h =>
      hpq0 <|
        leadingCoeff_eq_zero.1
          (by rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
⊢ q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
have rwa : 1 * (r - p /ₘ q).leadingCoeff ≠ 0
Tactic: rwa [Monic.def.1 hq, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False
have hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
Tactic: have hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0 := by rwa [Monic.def.1 hq, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False
have this₁ : HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(r - p /ₘ q).natDegree : WithBot ℕ) < (↑q.natDegree : WithBot ℕ)
Tactic: rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero,
      degree_eq_natDegree (mt leadingCoeff_eq_zero.2 hrpq0)] at this
Cleared hypotheses: this, hrpq0, hlc
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
⊢ q * p %ₘ q = 0
have rw : q ∣ q * p
Tactic: rw [modByMonic_eq_zero_iff_dvd hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : R[X]
hx : x.Monic
⊢ map f x ∣ map f y ↔ x ∣ y
have rw : map f (y %ₘ x) = 0 ↔ y %ₘ x = 0
Tactic: rw [← modByMonic_eq_zero_iff_dvd hx, ← modByMonic_eq_zero_iff_dvd (hx.map f), ←
    map_modByMonic f hx]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : R[X]
hx : x.Monic
H : map f (y %ₘ x) = 0
⊢ map f (y %ₘ x) = map f 0
have rw : 0 = map f 0
Tactic: rw [H, Polynomial.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : R[X]
hx : x.Monic
H : map f (y %ₘ x) = 0
rw : 0 = map f 0
⊢ map f (y %ₘ x) = map f 0
have rw₁ : Eq.{v + 1} (α := S[X]) 0 0
Tactic: rw [H, Polynomial.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : R[X]
hx : x.Monic
H : y %ₘ x = 0
⊢ map f (y %ₘ x) = 0
have rw : map f 0 = 0
Tactic: rw [H, Polynomial.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : R[X]
hx : x.Monic
H : y %ₘ x = 0
rw : map f 0 = 0
⊢ map f (y %ₘ x) = 0
have rw₁ : Eq.{v + 1} (α := S[X]) 0 0
Tactic: rw [H, Polynomial.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
| p
have rw : p %ₘ 1 + 1 * (p /ₘ 1)
Tactic: rw [← modByMonic_add_div p 1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
| p %ₘ 1 + 1 * (p /ₘ 1)
have simp : p /ₘ 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
| p
have rw : p /ₘ 1
Tactic: rw [← modByMonic_add_div p 1]; simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ p /ₘ 1 = p
have conv_rhs : p /ₘ 1 = p
Tactic: conv_rhs => rw [← modByMonic_add_div p 1]; simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
conv_rhs : p /ₘ 1 = p
⊢ p /ₘ 1 = p
have conv_rhs₁ : p /ₘ 1 = p /ₘ 1
Tactic: conv_rhs => rw [← modByMonic_add_div p 1]; simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ (↑n : WithBot ℕ)
⊢ ∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) ((p %ₘ q).coeff (↑i : ℕ)) = p %ₘ q
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 q : R[X]
hmo : q.Monic
⊢ q * p /ₘ q = p
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 q : R[X]
hmo : q.Monic
h : Nontrivial R
⊢ 0 + q * p = q * p
have rw : q * p = q * p
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmo : q.Monic
h : Nontrivial R
⊢ q * p /ₘ q = p
have refine : degree.{u} (R := R) 0 < q.degree
Tactic: refine (div_modByMonic_unique _ 0 hmo ⟨by rw [zero_add], ?_⟩).1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
    p.coeff (n + 1) + a * (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1)
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
n : ℕ
h : Nontrivial R
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
    p.coeff (n + 1) + a * (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1)
have this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Monic
Tactic: have := monic_X_sub_C a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : Nontrivial R
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Monic
q : R[X] := p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])
⊢ q.coeff n = p.coeff (n + 1) + a * q.coeff (n + 1)
have rw : q.coeff n =
  (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) +
          HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))).coeff
      (n + 1) +
    a * q.coeff (n + 1)
Tactic: rw [← p.modByMonic_add_div (X - C a)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : Nontrivial R
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Monic
q : R[X] := p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])
⊢ q.coeff n =
    (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) +
            HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
              (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))).coeff
        (n + 1) +
      a * q.coeff (n + 1)
have this₁ : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < (↑(n + 1) : WithBot ℕ)
Tactic: have : degree (p %ₘ (X - C a)) < ↑(n + 1) := degree_X_sub_C a ▸ p.degree_modByMonic_lt this
    |>.trans_le <| WithBot.coe_le_coe.mpr le_add_self
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
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 inr : ∀
  (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),
  (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
Tactic: wlog h : p.natDegree ≤ n generalizing n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
inr :
  ∀
    (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),
    (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
⊢ (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 wlog : ∀ (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
Tactic: wlog h : p.natDegree ≤ n generalizing n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
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
⊢ (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 inr : ∀ (n_1 : ℕ) (hn : n_1 < p.natDegree),
  n ≤ n_1 →
    ∀
      (ih :
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n_1 + 1) =
          ∑ i ∈ Icc (n_1 + 1 + 1) p.natDegree, a ^ (i - (n_1 + 1 + 1)) * p.coeff i),
      (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
Tactic: refine Nat.decreasingInduction' (fun n hn _ ih ↦ ?_) (le_of_not_ge h) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
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
inr :
  ∀ (n_1 : ℕ) (hn : n_1 < p.natDegree),
    n ≤ n_1 →
      ∀
        (ih :
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n_1 + 1) =
            ∑ i ∈ Icc (n_1 + 1 + 1) p.natDegree, a ^ (i - (n_1 + 1 + 1)) * p.coeff i),
        (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
⊢ (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 inr₁ : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff p.natDegree =
  ∑ i ∈ Icc (p.natDegree + 1) p.natDegree, a ^ (i - (p.natDegree + 1)) * p.coeff i
Tactic: refine Nat.decreasingInduction' (fun n hn _ ih ↦ ?_) (le_of_not_ge h) ?_
-- 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
⊢ (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 inr : p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
  p.coeff (n + 1) + ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)
Tactic: rw [coeff_divByMonic_X_sub_C_rec, ih, eq_comm, Icc_eq_cons_Ioc (Nat.succ_le_iff.mpr hn),
          sum_cons, Nat.sub_self, pow_zero, one_mul, mul_sum]
-- 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
⊢ p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)
have inr : 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))
Tactic: congr 1
-- 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
⊢ 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 : Ioc n.succ p.natDegree = Icc (n + 1 + 1) p.natDegree
Tactic: refine sum_congr ?_ fun i hi ↦ ?_