awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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 : ℕ)
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 : ℕ)
⊢ ∃ (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 : ℕ)

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

Premises used: add_mul, Fin.sum_univ_castSucc, add_assoc, mul_assoc, cast, add_rotate', pow_succ', Fin.val_last, Fin.snoc_last
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
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₂

Tactic:
simpa using hf
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
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:
exact ⟨by simpa using hf, funext Fin.rec0⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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 : ℕ)
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₂
⊢ q₁ = q₂ ∧ r₁ = r₂

Tactic:
cases r₁ using Fin.snocCases with | snoc rs₁ r₁
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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 : ℕ)
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₂)
⊢ q₁ = q₂ ∧ Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) rs₁ r₁ = r₂

Tactic:
cases r₂ using Fin.snocCases with | snoc rs₂ r₂
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₁ * 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

Premises used: Fin.sum_univ_castSucc, Fin.snoc_castSucc, Fin.val_last, Fin.snoc_last, Fin.val_castSucc
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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)
⊢ (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

Premises used: add_mul, HMul.hMul, add_assoc, mul_assoc, add_rotate', HPow.hPow, mul_comm, pow_succ'
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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 : ℕ)
i : Fin n
⊢ (rs₁ i).degree < g.degree

Tactic:
simpa using hr₁ i.castSucc

Premises used: Fin.castSucc
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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 : ℕ)
i : Fin n
⊢ (rs₂ i).degree < g.degree

Tactic:
simpa using hr₂ i.castSucc

Premises used: Fin.castSucc
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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 : ℕ)
⊢ 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
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₂
⊢ rs₁ = rs₂

Tactic:
obtain ⟨hqr, hrs⟩ := ih
      (fun i => by simpa using hr₁ i.castSucc)
      (fun i => by simpa using hr₂ i.castSucc) hf
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₂
⊢ r₁.degree < g.degree

Tactic:
simpa using hr₁ (Fin.last n)

Premises used: Fin.last
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₂
⊢ (r₁ + g * q₁) /ₘ g = q₁

Tactic:
obtain ⟨hq₁, hrr₁⟩ := div_modByMonic_unique q₁ r₁ hg ⟨rfl, by simpa using hr₁ (Fin.last n)⟩

Premises used: Polynomial.div_modByMonic_unique, And.intro, rfl
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₁
⊢ (r₁ + g * q₁) %ₘ g = r₁

Tactic:
obtain ⟨hq₁, hrr₁⟩ := div_modByMonic_unique q₁ r₁ hg ⟨rfl, by simpa using hr₁ (Fin.last n)⟩

Premises used: Polynomial.div_modByMonic_unique, And.intro, rfl
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₁
⊢ r₂.degree < g.degree

Tactic:
simpa using hr₂ (Fin.last n)

Premises used: Fin.last
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₁
⊢ (r₂ + g * q₂) /ₘ g = q₂

Tactic:
obtain ⟨hq₂, hrr₂⟩ := div_modByMonic_unique q₂ r₂ hg ⟨rfl, by simpa using hr₂ (Fin.last n)⟩

Premises used: Polynomial.div_modByMonic_unique, And.intro, rfl
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₂
⊢ (r₂ + g * q₂) %ₘ g = r₂

Tactic:
obtain ⟨hq₂, hrr₂⟩ := div_modByMonic_unique q₂ r₂ hg ⟨rfl, by simpa using hr₂ (Fin.last n)⟩

Premises used: Polynomial.div_modByMonic_unique, And.intro, rfl
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₂
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₂)

Tactic:
⟨hq₁.symm.trans (hqr ▸ hq₂), congrArg₂ Fin.snoc hrs (hrr₁.symm.trans (hqr ▸ hrr₂))⟩

Premises used: Eq.rec, Fin.snoc, congrArg₂, And.intro, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₂
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₂)

Tactic:
exact ⟨hq₁.symm.trans (hqr ▸ hq₂), congrArg₂ Fin.snoc hrs (hrr₁.symm.trans (hqr ▸ hrr₂))⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₂
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₂
⊢ 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₂))⟩

Premises used: add_mul, Fin.sum_univ_castSucc, Fin.snoc_castSucc, add_assoc, mul_assoc, mul_comm, pow_succ', Fin.val_last, Fin.snoc_last, Fin.val_castSucc
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → R[X]
hg : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (g i).Monic
hgg : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (r i).degree < (g i).degree) ∧
      f = q * ∏ i ∈ ∅, g i + ∑ i ∈ ∅, r i * ∏ k ∈ Finset.erase ∅ i, g k

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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)
⊢ (g i).Monic ∧ ∀ x ∈ s, (g x).Monic

Tactic:
rw [Finset.forall_mem_cons] at hg

Premises used: Finset.forall_mem_cons