-- Mathlib/Algebra/Polynomial/PartialFractions.lean
theorem div_eq_quo_add_sum_rem_div (f : R[X]) {ι : Type*} {g : ι → R[X]} {s : Finset ι}
    (hg : ∀ i ∈ s, (g i).Monic) (hcop : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)) :
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧
        ((↑f : K) / ∏ i ∈ s, ↑(g i)) = ↑q + ∑ i ∈ s, (r i : K) / (g i : K)

Proof state:
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
ι : Type u_1
g : ι → R[X]
a : ι
b : Finset ι
hab : a ∉ b
Hind :
  ∀ (f : R[X]),
    (∀ i ∈ b, (g i).Monic) →
      ((↑b).Pairwise fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ i ∈ b, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ i ∈ insert a b, (g i).Monic
hcop : (↑(insert a b)).Pairwise fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : r₁.degree < (g a).degree
left✝ : r₂.degree < (∏ i ∈ b, g i).degree
hf✝ : ↑f / (↑(g a) * ↑(∏ i ∈ b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ i ∈ b, (r i).degree < (g i).degree
hf : ↑f / ↑(g a * ∏ i ∈ b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
IH : ↑r₂ / ↑(∏ i ∈ b, g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
⊢ ↑(q₀ + q) + (↑r₁ / ↑(g a) + ∑ i ∈ b, ↑(r i) / ↑(g i)) =
    ↑(q₀ + q) + (↑r₁ / ↑(g a) + ∑ x ∈ b, ↑(if x = a then r₁ else r x) / ↑(g x))

Tactic:
congr 2

Result:
case e_a.e_a
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
ι : Type u_1
g : ι → R[X]
a : ι
b : Finset ι
hab : a ∉ b
Hind :
  ∀ (f : R[X]),
    (∀ i ∈ b, (g i).Monic) →
      ((↑b).Pairwise fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ i ∈ b, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ i ∈ insert a b, (g i).Monic
hcop : (↑(insert a b)).Pairwise fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : r₁.degree < (g a).degree
left✝ : r₂.degree < (∏ i ∈ b, g i).degree
hf✝ : ↑f / (↑(g a) * ↑(∏ i ∈ b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ i ∈ b, (r i).degree < (g i).degree
hf : ↑f / ↑(g a * ∏ i ∈ b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
IH : ↑r₂ / ↑(∏ i ∈ b, g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
⊢ ∑ i ∈ b, ↑(r i) / ↑(g i) = ∑ x ∈ b, ↑(if x = a then r₁ else r x) / ↑(g x)

Proof state:
case pos.refl
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
ι : Type u_1
g : ι → R[X]
a : ι
b : Finset ι
hab : a ∉ b
Hind :
  ∀ (f : R[X]),
    (∀ i ∈ b, (g i).Monic) →
      ((↑b).Pairwise fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ i ∈ b, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ i ∈ insert a b, (g i).Monic
hcop : (↑(insert a b)).Pairwise fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : r₁.degree < (g a).degree
left✝ : r₂.degree < (∏ i ∈ b, g i).degree
hf : ↑f / (↑(g a) * ↑(∏ i ∈ b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ i ∈ b, (r i).degree < (g i).degree
IH : ↑?m.17923 / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
⊢ a ∈ insert a b → r₁.degree < (g a).degree

Tactic:
intro

Result:
case pos.refl
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
ι : Type u_1
g : ι → R[X]
a : ι
b : Finset ι
hab : a ∉ b
Hind :
  ∀ (f : R[X]),
    (∀ i ∈ b, (g i).Monic) →
      ((↑b).Pairwise fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ i ∈ b, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ i ∈ insert a b, (g i).Monic
hcop : (↑(insert a b)).Pairwise fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : r₁.degree < (g a).degree
left✝ : r₂.degree < (∏ i ∈ b, g i).degree
hf : ↑f / (↑(g a) * ↑(∏ i ∈ b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ i ∈ b, (r i).degree < (g i).degree
IH : ↑?m.17923 / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
a✝ : a ∈ insert a b
⊢ r₁.degree < (g a).degree

Proof state:
case insert.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
ι : Type u_1
g : ι → R[X]
a : ι
b : Finset ι
hab : a ∉ b
Hind :
  ∀ (f : R[X]),
    (∀ i ∈ b, (g i).Monic) →
      ((↑b).Pairwise fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ i ∈ b, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ i ∈ insert a b, (g i).Monic
hcop : (↑(insert a b)).Pairwise fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : r₁.degree < (g a).degree
left✝ : r₂.degree < (∏ i ∈ b, g i).degree
hf : ↑f / (↑(g a) * ↑(∏ i ∈ b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ i ∈ b, (r i).degree < (g i).degree
IH : ↑?m.17923 / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
⊢ ∀ i ∈ insert a b, ((fun i => if i = a then r₁ else r i) i).degree < (g i).degree

Tactic:
intro i

Result:
case insert.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
ι : Type u_1
g : ι → R[X]
a : ι
b : Finset ι
hab : a ∉ b
Hind :
  ∀ (f : R[X]),
    (∀ i ∈ b, (g i).Monic) →
      ((↑b).Pairwise fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ i ∈ b, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ i ∈ insert a b, (g i).Monic
hcop : (↑(insert a b)).Pairwise fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : r₁.degree < (g a).degree
left✝ : r₂.degree < (∏ i ∈ b, g i).degree
hf : ↑f / (↑(g a) * ↑(∏ i ∈ b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ i ∈ b, (r i).degree < (g i).degree
IH : ↑?m.17923 / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
i : ι
⊢ i ∈ insert a b → ((fun i => if i = a then r₁ else r i) i).degree < (g i).degree