awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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]
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
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₂)
have hf₁ : q₁ * g ^ (n + 1) + (∑ x : Fin n, rs₁ x * g ^ (↑x : ℕ) + r₁ * g ^ n) =
  q₂ * g ^ (n + 1) + (∑ x : Fin n, rs₂ x * g ^ (↑x : ℕ) + r₂ * g ^ n)
Tactic: simp only [Fin.sum_univ_castSucc, Fin.snoc_castSucc,
      Fin.val_castSucc, Fin.snoc_last, Fin.val_last] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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]
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
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) + (∑ x : Fin n, rs₁ x * g ^ (↑x : ℕ) + r₁ * g ^ n) =
    q₂ * g ^ (n + 1) + (∑ x : Fin n, rs₂ x * g ^ (↑x : ℕ) + r₂ * g ^ n)
⊢ 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₂)
have hf₁ : (r₁ + g * q₁) * g ^ n + ∑ x : Fin n, rs₁ x * g ^ (↑x : ℕ) = (r₂ + g * q₂) * g ^ n + ∑ x : Fin n, rs₂ x * g ^ (↑x : ℕ)
Tactic: rw [← add_rotate' (r₁ * g ^ n), ← add_rotate' (r₂ * g ^ n), pow_succ', ← mul_assoc, ← mul_assoc,
      ← add_assoc, ← add_assoc, ← add_mul, ← add_mul, ← mul_comm g, ← mul_comm g] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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]
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
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 :
  (r₁ + g * q₁) * g ^ n + ∑ x : Fin n, rs₁ x * g ^ (↑x : ℕ) = (r₂ + g * q₂) * g ^ n + ∑ x : Fin n, rs₂ x * g ^ (↑x : ℕ)
⊢ 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₂)
have hqr : r₁ + g * q₁ = r₂ + g * q₂
Tactic: obtain ⟨hqr, hrs⟩ := ih
      (fun i => by simpa using hr₁ i.castSucc)
      (fun i => by simpa using hr₂ i.castSucc) hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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]
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
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 :
  (r₁ + g * q₁) * g ^ n + ∑ x : Fin n, rs₁ x * g ^ (↑x : ℕ) = (r₂ + g * q₂) * g ^ n + ∑ x : Fin n, rs₂ x * g ^ (↑x : ℕ)
hqr : r₁ + g * q₁ = r₂ + g * q₂
⊢ 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₂)
have hrs : rs₁ = rs₂
Tactic: obtain ⟨hqr, hrs⟩ := ih
      (fun i => by simpa using hr₁ i.castSucc)
      (fun i => by simpa using hr₂ i.castSucc) hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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]
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
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 :
  (r₁ + g * q₁) * g ^ n + ∑ x : Fin n, rs₁ x * g ^ (↑x : ℕ) = (r₂ + g * q₂) * g ^ n + ∑ x : Fin n, rs₂ x * g ^ (↑x : ℕ)
hqr : r₁ + g * q₁ = r₂ + g * q₂
hrs : rs₁ = rs₂
⊢ 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₂)
have hq₁ : (r₁ + g * q₁) /ₘ g = q₁
Tactic: obtain ⟨hq₁, hrr₁⟩ := div_modByMonic_unique q₁ r₁ hg ⟨rfl, by simpa using hr₁ (Fin.last n)⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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]
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
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 :
  (r₁ + g * q₁) * g ^ n + ∑ x : Fin n, rs₁ x * g ^ (↑x : ℕ) = (r₂ + g * q₂) * g ^ n + ∑ x : Fin n, rs₂ x * g ^ (↑x : ℕ)
hqr : r₁ + g * q₁ = r₂ + g * q₂
hrs : rs₁ = rs₂
hq₁ : (r₁ + g * q₁) /ₘ g = q₁
⊢ 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₂)
have hrr₁ : (r₁ + g * q₁) %ₘ g = r₁
Tactic: obtain ⟨hq₁, hrr₁⟩ := div_modByMonic_unique q₁ r₁ hg ⟨rfl, by simpa using hr₁ (Fin.last n)⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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]
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
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 :
  (r₁ + g * q₁) * g ^ n + ∑ x : Fin n, rs₁ x * g ^ (↑x : ℕ) = (r₂ + g * q₂) * g ^ n + ∑ x : Fin n, rs₂ x * g ^ (↑x : ℕ)
hqr : r₁ + g * q₁ = r₂ + g * q₂
hrs : rs₁ = rs₂
hq₁ : (r₁ + g * q₁) /ₘ g = q₁
hrr₁ : (r₁ + g * q₁) %ₘ g = r₁
⊢ 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₂)
have hq₂ : (r₂ + g * q₂) /ₘ g = q₂
Tactic: obtain ⟨hq₂, hrr₂⟩ := div_modByMonic_unique q₂ r₂ hg ⟨rfl, by simpa using hr₂ (Fin.last n)⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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]
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
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 :
  (r₁ + g * q₁) * g ^ n + ∑ x : Fin n, rs₁ x * g ^ (↑x : ℕ) = (r₂ + g * q₂) * g ^ n + ∑ x : Fin n, rs₂ x * g ^ (↑x : ℕ)
hqr : r₁ + g * q₁ = r₂ + g * q₂
hrs : rs₁ = rs₂
hq₁ : (r₁ + g * q₁) /ₘ g = q₁
hrr₁ : (r₁ + g * q₁) %ₘ g = r₁
hq₂ : (r₂ + g * q₂) /ₘ g = q₂
⊢ 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₂)
have hrr₂ : (r₂ + g * q₂) %ₘ g = r₂
Tactic: obtain ⟨hq₂, hrr₂⟩ := div_modByMonic_unique q₂ r₂ hg ⟨rfl, by simpa using hr₂ (Fin.last 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 : ℕ
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₂
have zero : ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin 0 → R[X]} (hr₁ : ∀ (i : Fin 0), (r₁ i).degree < g.degree)
  (hr₂ : ∀ (i : Fin 0), (r₂ i).degree < g.degree)
  (hf :
    q₁ * HPow.hPow (β := ℕ) g 0 + ∑ i : Fin 0, r₁ i * g ^ (↑i : ℕ) =
      q₂ * HPow.hPow (β := ℕ) g 0 + ∑ i : Fin 0, r₂ i * g ^ (↑i : ℕ)),
  q₁ = q₂ ∧ r₁ = r₂
Tactic: induction n generalizing q₁ q₂ with
  | zero => exact ⟨by simpa using hf, funext Fin.rec0⟩
  | succ n ih =>
    cases r₁ using Fin.snocCases with | snoc rs₁ r₁
    cases r₂ using Fin.snocCases with | snoc rs₂ r₂
    simp only [Fin.sum_univ_castSucc, Fin.snoc_castSucc,
      Fin.val_castSucc, Fin.snoc_last, Fin.val_last] at hf
    rw [← add_rotate' (r₁ * g ^ n), ← add_rotate' (r₂ * g ^ n), pow_succ', ← mul_assoc, ← mul_assoc,
      ← add_assoc, ← add_assoc, ← add_mul, ← add_mul, ← mul_comm g, ← mul_comm g] at hf
    obtain ⟨hqr, hrs⟩ := ih
      (fun i => by simpa using hr₁ i.castSucc)
      (fun i => by simpa using hr₂ i.castSucc) hf
    obtain ⟨hq₁, hrr₁⟩ := div_modByMonic_unique q₁ r₁ hg ⟨rfl, by simpa using hr₁ (Fin.last n)⟩
    obtain ⟨hq₂, hrr₂⟩ := div_modByMonic_unique q₂ r₂ hg ⟨rfl, by simpa using hr₂ (Fin.last n)⟩
    exact ⟨hq₁.symm.trans (hqr ▸ hq₂), congrArg₂ Fin.snoc hrs (hrr₁.symm.trans (hqr ▸ hrr₂))⟩
Cleared hypotheses: n, q₁, q₂, r₁, r₂, hr₁, 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 : ℕ
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 : ℕ)
zero :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin 0 → R[X]} (hr₁ : ∀ (i : Fin 0), (r₁ i).degree < g.degree)
    (hr₂ : ∀ (i : Fin 0), (r₂ i).degree < g.degree)
    (hf :
      q₁ * HPow.hPow (β := ℕ) g 0 + ∑ i : Fin 0, r₁ i * g ^ (↑i : ℕ) =
        q₂ * HPow.hPow (β := ℕ) g 0 + ∑ i : Fin 0, r₂ i * g ^ (↑i : ℕ)),
    q₁ = q₂ ∧ r₁ = r₂
⊢ q₁ = q₂ ∧ r₁ = r₂
have succ : ∀ (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₂
Tactic: induction n generalizing q₁ q₂ with
  | zero => exact ⟨by simpa using hf, funext Fin.rec0⟩
  | succ n ih =>
    cases r₁ using Fin.snocCases with | snoc rs₁ r₁
    cases r₂ using Fin.snocCases with | snoc rs₂ r₂
    simp only [Fin.sum_univ_castSucc, Fin.snoc_castSucc,
      Fin.val_castSucc, Fin.snoc_last, Fin.val_last] at hf
    rw [← add_rotate' (r₁ * g ^ n), ← add_rotate' (r₂ * g ^ n), pow_succ', ← mul_assoc, ← mul_assoc,
      ← add_assoc, ← add_assoc, ← add_mul, ← add_mul, ← mul_comm g, ← mul_comm g] at hf
    obtain ⟨hqr, hrs⟩ := ih
      (fun i => by simpa using hr₁ i.castSucc)
      (fun i => by simpa using hr₂ i.castSucc) hf
    obtain ⟨hq₁, hrr₁⟩ := div_modByMonic_unique q₁ r₁ hg ⟨rfl, by simpa using hr₁ (Fin.last n)⟩
    obtain ⟨hq₂, hrr₂⟩ := div_modByMonic_unique q₂ r₂ hg ⟨rfl, by simpa using hr₂ (Fin.last n)⟩
    exact ⟨hq₁.symm.trans (hqr ▸ hq₂), congrArg₂ Fin.snoc hrs (hrr₁.symm.trans (hqr ▸ hrr₂))⟩
Cleared hypotheses: n, q₁, q₂, r₁, r₂, hr₁, hr₂, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : ∀ i_1 ∈ Finset.cons i s hi, (g i_1).Monic
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
have hg₁ : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
Tactic: rw [Finset.forall_mem_cons] at hg
Cleared hypotheses: hg, hgg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
have hgg₁ : ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
  ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
Tactic: rw [Finset.coe_cons, Set.pairwise_insert] at hgg
Cleared hypotheses: hgg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
have cons : ∀ (q : R[X]) (r : ι → R[X]) (hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k),
  ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
Tactic: obtain ⟨q, r, -, hf⟩ := ih hg.2 hgg.1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
have hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
Tactic: have hjs {j : ι} (hj : j ∈ s) : i ≠ j := fun hij => hi (hij ▸ hj)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
have hc : ∀ (j : ι), ∃ (a : R[X]) (b : R[X]), j ∈ s → a * g i + b * g j = 1
Tactic: have hc (j : ι) : ∃ a b, j ∈ s → a * g i + b * g j = 1 :=
      if h : j ∈ s ∧ i ≠ j then
        (hgg.2 j h.1 h.2).1.elim fun a h => h.elim fun b h => ⟨a, b, fun _ => h⟩
      else
        ⟨0, 0, fun hj => (h ⟨hj, hjs hj⟩).elim⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
hc : ∀ (j : ι), ∃ (a : R[X]) (b : R[X]), j ∈ s → a * g i + b * g j = 1
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
have cons : ∀ (a b : (j : ι) → R[X]) (hab : ∀ j ∈ s, a j * g i + b j * g j = 1),
  ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
Tactic: choose a b hab using hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
have cons : ∀ i_1 ∈ Finset.cons i s hi,
  degree.{u_1} (R := R)
      (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
        ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1) <
    (g i_1).degree
Tactic: refine ⟨(q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j),
      Function.update (fun j => r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i),
      ?_, hf.trans ?_⟩