awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
C' : g = g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
rw : f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ) = g
⊢ f = g
have rw₁ : Eq (α := RingHom.{u, u_1} R[X] S) (f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
  (g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
Tactic: rw [B, C', A]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
C' : g = g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
rw : f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ) = g
rw₁ :
  Eq (α := RingHom.{u, u_1} R[X] S) (f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
    (g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
⊢ f = g
have rw₂ : Eq (α := RingHom.{u, u_1} R[X] S) (g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
  (g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
Tactic: rw [B, C', A]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x y : Fin n → R
⊢ { toFinsupp := (List.ofFn (x + y)).toFinsupp } =
    HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
      { toFinsupp := (List.ofFn y).toFinsupp : R[X] }
have a : ∀ (i : ℕ),
  coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
    (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
          { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
⊢ coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
    (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
          { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
      i
have pos : ∀ (h : i < n),
  coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
    (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
          { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
      i
Tactic: by_cases h : i < n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
pos :
  ∀ (h : i < n),
    coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
      (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
            { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
        i
⊢ coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
    (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
          { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
      i
have neg : ∀ (h : ¬i < n),
  coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
    (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
          { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
      i
Tactic: by_cases h : i < n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x : R
p : Fin n → R
⊢ { toFinsupp := (List.ofFn (x • p)).toFinsupp } =
    HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
      { toFinsupp := (List.ofFn p).toFinsupp : R[X] }
have a : ∀ (i : ℕ),
  coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
    (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
          { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
⊢ coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
    (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
          { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
      i
have pos : ∀ (h : i < n),
  coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
    (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
          { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
      i
Tactic: by_cases h : i < n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
pos :
  ∀ (h : i < n),
    coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
      (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
            { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
        i
⊢ coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
    (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
          { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
      i
have neg : ∀ (h : ¬i < n),
  coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
    (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
          { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
      i
Tactic: by_cases h : i < n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : Ne (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])
⊢ n ≠ 0
have contrapose : ∀ (h : n = 0), Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : n = 0
⊢ Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])
have subst : ∀ {v : Fin 0 → R}, Eq (α := R[X]) ((ofFn 0 : (a : Fin 0 → R) → R[X]) v : R[X]) (0 : R[X])
Tactic: subst h
Cleared hypotheses: n, v, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
⊢ natDegree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < n
have rw : ∀ (N : ℕ), n - 1 < N → Eq.{u_1 + 1} (α := R) (coeff ((ofFn n : (a : Fin n → R) → R[X]) v) N) 0
Tactic: rw [Nat.lt_iff_le_pred h, natDegree_le_iff_coeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
⊢ degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)
have pos : ∀ (h : Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])),
  degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)
Tactic: by_cases h : ofFn n v = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
pos :
  ∀ (h : Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])),
    degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)
⊢ degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)
have neg : ∀ (h : ¬Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])),
  degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)
Tactic: by_cases h : ofFn n v = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])
⊢ degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)
have pos : LT.lt (α := WithBot ℕ) ⊥ (↑n : WithBot ℕ)
Tactic: simp only [h, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
⊢ Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])
have pos : ∀ (h : n = 0),
  Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
pos :
  ∀ (h : n = 0),
    Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
      (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])
⊢ Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])
have neg : ∀ (h : ¬n = 0),
  Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : n = 0
⊢ Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])
have pos : ∀ (v : Fin 0 → R),
  Eq (α := R[X]) ((ofFn 0 : (a : Fin 0 → R) → R[X]) v : R[X])
    (∑ i : Fin 0, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])
Tactic: subst h
Cleared hypotheses: n, v, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬n = 0
⊢ Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])
have neg : Eq.{u_1 + 1} (α := R[X])
  (∑ i ∈ Finset.range n, (monomial i : (a : R) → R[X]) (coeff ((ofFn n : (a : Fin n → R) → R[X]) v) i))
  (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i))
Tactic: rw [as_sum_range' (ofFn n v) n <| ofFn_natDegree_lt (Nat.one_le_iff_ne_zero.mpr h) v]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
⊢ (ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p) = p
have a : ∀ (i : ℕ), coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
⊢ coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i
have pos : ∀ (h : i < n), coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i
Tactic: by_cases! h : i < n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
pos : ∀ (h : i < n), coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i
⊢ coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i
have neg : ∀ (h : n ≤ i), coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i
Tactic: by_cases! h : i < n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.OfFn (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
⊢ coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i
have this : p.coeff i = 0
Tactic: have : p.coeff i = 0 := coeff_eq_zero_of_natDegree_lt <| by lia
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∃ (q : R[X]) (r : Fin n → R[X]),
    (∀ (i : Fin n), (r i).degree < g.degree) ∧ f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
⊢ ∃ (q : R[X]) (r : Fin (n + 1) → R[X]),
    (∀ (i : Fin (n + 1)), (r i).degree < g.degree) ∧ f = q * g ^ (n + 1) + ∑ i : Fin (n + 1), r i * g ^ (↑i : ℕ)
have succ : ∀ (q : R[X]) (r : Fin n → R[X]) (hr : ∀ (i : Fin n), (r i).degree < g.degree)
  (hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)),
  ∃ (q : R[X]) (r : Fin (n + 1) → R[X]),
    (∀ (i : Fin (n + 1)), (r i).degree < g.degree) ∧ f = q * g ^ (n + 1) + ∑ i : Fin (n + 1), r i * g ^ (↑i : ℕ)
Tactic: obtain ⟨q, r, hr, hf⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
⊢ ∃ (q : R[X]) (r : Fin (n + 1) → R[X]),
    (∀ (i : Fin (n + 1)), (r i).degree < g.degree) ∧ f = q * g ^ (n + 1) + ∑ i : Fin (n + 1), r i * g ^ (↑i : ℕ)
have succ : ∀ (i : Fin (n + 1)), degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i) < g.degree
Tactic: refine ⟨q /ₘ g, Fin.snoc r (q %ₘ g), fun i => ?_, hf.trans ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
succ : ∀ (i : Fin (n + 1)), degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i) < g.degree
⊢ ∃ (q : R[X]) (r : Fin (n + 1) → R[X]),
    (∀ (i : Fin (n + 1)), (r i).degree < g.degree) ∧ f = q * g ^ (n + 1) + ∑ i : Fin (n + 1), r i * g ^ (↑i : ℕ)
have succ₁ : q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ) =
  q /ₘ g * g ^ (n + 1) +
    ∑ i : Fin (n + 1),
      HMul.hMul (α := R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i : R[X]) (g ^ (↑i : ℕ))
Tactic: refine ⟨q /ₘ g, Fin.snoc r (q %ₘ g), fun i => ?_, hf.trans ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
i : Fin (n + 1)
⊢ degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i) < g.degree
have succ : ∀ (i : Fin n), degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i.castSucc) < g.degree
Tactic: cases i using Fin.lastCases with
      | cast i => simpa using hr i
      | last => simpa using degree_modByMonic_lt q hg
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
i : Fin (n + 1)
succ :
  ∀ (i : Fin n), degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i.castSucc) < g.degree
⊢ degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i) < g.degree
have succ₁ : degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) (Fin.last n)) < g.degree
Tactic: cases i using Fin.lastCases with
      | cast i => simpa using hr i
      | last => simpa using degree_modByMonic_lt q hg
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
⊢ q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ) =
    q /ₘ g * g ^ (n + 1) +
      ∑ i : Fin (n + 1),
        HMul.hMul (α := R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i : R[X]) (g ^ (↑i : ℕ))
have succ : q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ) =
  q * g ^ n +
    ∑ i : Fin n,
      HMul.hMul (α := R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i.castSucc : R[X])
        (g ^ (↑i.castSucc : ℕ))
Tactic: rw [Fin.sum_univ_castSucc, ← add_rotate', Fin.snoc_last, Fin.val_last,
        ← add_assoc, pow_succ', ← mul_assoc, ← add_mul, mul_comm (q /ₘ g) g,
        modByMonic_add_div q]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
⊢ ∃ (q : R[X]) (r : Fin n → R[X]),
    (∀ (i : Fin n), (r i).degree < g.degree) ∧ f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
have zero : ∃ (q : R[X]) (r : Fin 0 → R[X]),
  (∀ (i : Fin 0), (r i).degree < g.degree) ∧ f = q * HPow.hPow (β := ℕ) g 0 + ∑ i : Fin 0, r i * g ^ (↑i : ℕ)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    obtain ⟨q, r, hr, hf⟩ := ih
    refine ⟨q /ₘ g, Fin.snoc r (q %ₘ g), fun i => ?_, hf.trans ?_⟩
    · cases i using Fin.lastCases with
      | cast i => simpa using hr i
      | last => simpa using degree_modByMonic_lt q hg
    · rw [Fin.sum_univ_castSucc, ← add_rotate', Fin.snoc_last, Fin.val_last,
        ← add_assoc, pow_succ', ← mul_assoc, ← add_mul, mul_comm (q /ₘ g) g,
        modByMonic_add_div q]
      simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
zero :
  ∃ (q : R[X]) (r : Fin 0 → R[X]),
    (∀ (i : Fin 0), (r i).degree < g.degree) ∧ f = q * HPow.hPow (β := ℕ) g 0 + ∑ i : Fin 0, r i * g ^ (↑i : ℕ)
⊢ ∃ (q : R[X]) (r : Fin n → R[X]),
    (∀ (i : Fin n), (r i).degree < g.degree) ∧ f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
have succ : ∀ (n : ℕ)
  (ih :
    ∃ (q : R[X]) (r : Fin n → R[X]),
      (∀ (i : Fin n), (r i).degree < g.degree) ∧ f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)),
  ∃ (q : R[X]) (r : Fin (n + 1) → R[X]),
    (∀ (i : Fin (n + 1)), (r i).degree < g.degree) ∧ f = q * g ^ (n + 1) + ∑ i : Fin (n + 1), r i * g ^ (↑i : ℕ)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    obtain ⟨q, r, hr, hf⟩ := ih
    refine ⟨q /ₘ g, Fin.snoc r (q %ₘ g), fun i => ?_, hf.trans ?_⟩
    · cases i using Fin.lastCases with
      | cast i => simpa using hr i
      | last => simpa using degree_modByMonic_lt q hg
    · rw [Fin.sum_univ_castSucc, ← add_rotate', Fin.snoc_last, Fin.val_last,
        ← add_assoc, pow_succ', ← mul_assoc, ← add_mul, mul_comm (q /ₘ g) g,
        modByMonic_add_div q]
      simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]} (hr₁ : ∀ (i : Fin n), (r₁ i).degree < g.degree)
    (hr₂ : ∀ (i : Fin n), (r₂ i).degree < g.degree)
    (hf : q₁ * g ^ n + ∑ i : Fin n, r₁ i * g ^ (↑i : ℕ) = q₂ * g ^ n + ∑ i : Fin n, r₂ i * g ^ (↑i : ℕ)),
    q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
r₁ r₂ : Fin (n + 1) → R[X]
hr₁ : ∀ (i : Fin (n + 1)), (r₁ i).degree < g.degree
hr₂ : ∀ (i : Fin (n + 1)), (r₂ i).degree < g.degree
hf :
  q₁ * g ^ (n + 1) + ∑ i : Fin (n + 1), r₁ i * g ^ (↑i : ℕ) = q₂ * g ^ (n + 1) + ∑ i : Fin (n + 1), r₂ i * g ^ (↑i : ℕ)
⊢ q₁ = q₂ ∧ r₁ = r₂
have succ : ∀ (rs₁ : (i : Fin n) → R[X]) (r₁ : R[X])
  (hr₁ : ∀ (i : Fin (n + 1)), degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₁ r₁ i) < g.degree)
  (hf :
    q₁ * g ^ (n + 1) +
        ∑ i : Fin (n + 1),
          HMul.hMul (α := R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₁ r₁ i : R[X]) (g ^ (↑i : ℕ)) =
      q₂ * g ^ (n + 1) + ∑ i : Fin (n + 1), r₂ i * g ^ (↑i : ℕ)),
  q₁ = q₂ ∧ Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₁ r₁ = r₂
Tactic: cases r₁ using Fin.snocCases with | snoc rs₁ r₁
Cleared hypotheses: r₁, hr₁, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]} (hr₁ : ∀ (i : Fin n), (r₁ i).degree < g.degree)
    (hr₂ : ∀ (i : Fin n), (r₂ i).degree < g.degree)
    (hf : q₁ * g ^ n + ∑ i : Fin n, r₁ i * g ^ (↑i : ℕ) = q₂ * g ^ n + ∑ i : Fin n, r₂ i * g ^ (↑i : ℕ)),
    q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
r₂ : Fin (n + 1) → R[X]
hr₂ : ∀ (i : Fin (n + 1)), (r₂ i).degree < g.degree
rs₁ : (i : Fin n) → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₁ r₁ i) < g.degree
hf :
  q₁ * g ^ (n + 1) +
      ∑ i : Fin (n + 1),
        HMul.hMul (α := R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₁ r₁ i : R[X]) (g ^ (↑i : ℕ)) =
    q₂ * g ^ (n + 1) + ∑ i : Fin (n + 1), r₂ i * g ^ (↑i : ℕ)
⊢ q₁ = q₂ ∧ Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₁ r₁ = r₂
have succ : ∀ (rs₂ : (i : Fin n) → R[X]) (r₂ : R[X])
  (hr₂ : ∀ (i : Fin (n + 1)), degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₂ r₂ i) < g.degree)
  (hf :
    q₁ * g ^ (n + 1) +
        ∑ i : Fin (n + 1),
          HMul.hMul (α := R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₁ r₁ i : R[X]) (g ^ (↑i : ℕ)) =
      q₂ * g ^ (n + 1) +
        ∑ i : Fin (n + 1),
          HMul.hMul (α := R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₂ r₂ i : R[X]) (g ^ (↑i : ℕ))),
  q₁ = q₂ ∧
    Eq.{u_1 + 1} (α := Fin (n + 1) → R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₁ r₁)
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₂ r₂)
Tactic: cases r₂ using Fin.snocCases with | snoc rs₂ r₂
Cleared hypotheses: r₂, hr₂, hf