-- 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_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 → (if i = a then r₁ else r i).degree < (g i).degree

Tactic:
split_ifs with h1

Result:
case pos
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
⊢ i ∈ insert a b → r₁.degree < (g i).degree

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
⊢ i ∈ insert a b → (r i).degree < (g i).degree

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)
i : ι
hi : i ∈ b
⊢ a ≠ i

Tactic:
rintro rfl

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)
hi : a ∈ b
⊢ False

Proof state:
case insert.intro.intro.intro.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[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)
⊢ ∃ 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:
refine ⟨q₀ + q, fun i => if i = a then r₁ else r 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 ∈ insert a b, ((fun i => if i = a then r₁ else r i) i).degree < (g i).degree

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)