-- 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:
case insert.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
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)
⊢ ↑f / ∏ i ∈ insert a b, ↑(g i) = ↑(q₀ + q) + ∑ i ∈ insert a b, ↑((fun i => if i = a then r₁ else r i) i) / ↑(g i)

Tactic:
norm_cast at hf IH ⊢

Result:
case insert.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
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 : ↑?m.17923 / ↑(∏ i ∈ b, g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
⊢ ↑f / ↑(∏ i ∈ insert a b, g i) = ↑(q₀ + q) + ∑ x ∈ insert a b, ↑(if x = a then r₁ else r x) / ↑(g x)

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]
f : R[X]
hg : ∀ i ∈ ∅, (g i).Monic
hcop : (↑∅).Pairwise fun i j => IsCoprime (g i) (g j)
⊢ ↑f / ∏ i ∈ ∅, ↑(g i) = ↑f + ∑ i ∈ ∅, ↑((fun x => 0) i) / ↑(g i)

Tactic:
simp

Result:
no goals

Proof state:
case insert.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
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₀ + ↑r₁ / ↑(g a) + (↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)) =
    ↑(q₀ + q) + (↑r₁ / ↑(g a) + ∑ x ∈ b, ↑(if x = a then r₁ else r x) / ↑(g x))

Tactic:
trans (↑(q₀ + q : R[X]) : K) + (↑r₁ / ↑(g a) + ∑ i ∈ b, (r i : K) / (g i : K))

Result:
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₀ + ↑r₁ / ↑(g a) + (↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)) = ↑(q₀ + q) + (↑r₁ / ↑(g a) + ∑ i ∈ b, ↑(r i) / ↑(g i))

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))