-- 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 neg
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 : ι
h1 : ¬i = a
hi : i ∈ insert a b
⊢ (r i).degree < (g i).degree

Tactic:
exact hrdeg i (Finset.mem_of_mem_insert_of_ne hi h1)

Result:
no goals

Proof state:
case insert
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,
    (∀ i ∈ insert a b, (r i).degree < (g i).degree) ∧
      ↑f / ∏ i ∈ insert a b, ↑(g i) = ↑q + ∑ i ∈ insert a b, ↑(r i) / ↑(g i)

Tactic:
obtain ⟨q₀, r₁, r₂, hdeg₁, _, hf : (↑f : K) / _ = _⟩ :=
  div_eq_quo_add_rem_div_add_rem_div R K f
    (hg a (b.mem_insert_self a) : Monic (g a))
    (monic_prod_of_monic _ _ fun i hi => hg i (Finset.mem_insert_of_mem hi) :
      Monic (∏ i ∈ b, g i))
    (IsCoprime.prod_right fun i hi =>
      hcop (Finset.mem_coe.2 (b.mem_insert_self a))
        (Finset.mem_coe.2 (Finset.mem_insert_of_mem hi)) (by rintro rfl; exact hab hi))

Result:
case insert.intro.intro.intro.intro.intro
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,
    (∀ i ∈ insert a b, (r i).degree < (g i).degree) ∧
      ↑f / ∏ i ∈ insert a b, ↑(g i) = ↑q + ∑ i ∈ insert a b, ↑(r i) / ↑(g i)

Proof state:
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)

Tactic:
refine Finset.sum_congr rfl fun x hxb => ?_

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)
x : ι
hxb : x ∈ b
⊢ ↑(r x) / ↑(g x) = ↑(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
f : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j => IsCoprime (g i) (g j)
⊢ ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)

Tactic:
induction' s using Finset.induction_on with a b hab Hind f generalizing f

Result:
case empty
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)
⊢ ∃ q r, (∀ i ∈ ∅, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ ∅, ↑(g i) = ↑q + ∑ i ∈ ∅, ↑(r i) / ↑(g i)

case insert
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,
    (∀ i ∈ insert a b, (r i).degree < (g i).degree) ∧
      ↑f / ∏ i ∈ insert a b, ↑(g i) = ↑q + ∑ i ∈ insert a b, ↑(r i) / ↑(g i)