awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → 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))
    (hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree) (hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree)
    (hf :
      q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
        q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k),
    q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : q₁ - q₂ = 0
hpgd : Dvd.dvd.{u_1} (α := R[X]) (∏ i ∈ s, g i) (∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x)
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : Monic.{u_1} (R := R) (∏ i ∈ s, g i)
hdp : degree.{u_1} (R := R) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) < degree.{u_1} (R := R) (∏ i ∈ s, g i)
hp0 : HSub.hSub (α := R[X]) (∑ x ∈ s, r₁ x * ∏ k ∈ s.erase x, g k) (∑ x ∈ s, r₂ x * ∏ k ∈ s.erase x, g k) = 0
hf₁ : q₁ = q₂
hpgd₁ : Dvd.dvd.{u_1} (α := R[X]) (∏ i ∈ s, g i) (∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x)
hdr₁ : (r₂ i - r₁ i).degree < (g i).degree
hr0₁ : r₂ i = r₁ i
hpm₁ : Monic.{u_1} (R := R) (∏ i ∈ s, g i)
⊢ degree.{u_1} (R := R) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) < degree.{u_1} (R := R) (∏ i ∈ s, g i)

Tactic:
rw [sub_eq_zero] at hf hr0 hp0

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → 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))
    (hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree) (hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree)
    (hf :
      q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
        q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k),
    q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : q₁ - q₂ = 0
hpgd : Dvd.dvd.{u_1} (α := R[X]) (∏ i ∈ s, g i) (∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x)
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : Monic.{u_1} (R := R) (∏ i ∈ s, g i)
hdp : degree.{u_1} (R := R) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) < degree.{u_1} (R := R) (∏ i ∈ s, g i)
hp0 : HSub.hSub (α := R[X]) (∑ x ∈ s, r₁ x * ∏ k ∈ s.erase x, g k) (∑ x ∈ s, r₂ x * ∏ k ∈ s.erase x, g k) = 0
hf₁ : q₁ = q₂
hpgd₁ : Dvd.dvd.{u_1} (α := R[X]) (∏ i ∈ s, g i) (∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x)
hdr₁ : (r₂ i - r₁ i).degree < (g i).degree
hr0₁ : r₂ i = r₁ i
hpm₁ : Monic.{u_1} (R := R) (∏ i ∈ s, g i)
hdp₁ : degree.{u_1} (R := R) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) < degree.{u_1} (R := R) (∏ i ∈ s, g i)
⊢ Eq.{u_1 + 1} (α := R[X]) (∑ x ∈ s, r₁ x * ∏ k ∈ s.erase x, g k) (∑ x ∈ s, r₂ x * ∏ k ∈ s.erase x, g k)

Tactic:
rw [sub_eq_zero] at hf hr0 hp0

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → 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))
    (hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree) (hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree)
    (hf :
      q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
        q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k),
    q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : q₁ = q₂
hpgd : Dvd.dvd.{u_1} (α := R[X]) (∏ i ∈ s, g i) (∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x)
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i = r₁ i
hpm : Monic.{u_1} (R := R) (∏ i ∈ s, g i)
hdp : degree.{u_1} (R := R) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) < degree.{u_1} (R := R) (∏ i ∈ s, g i)
hp0 : Eq.{u_1 + 1} (α := R[X]) (∑ x ∈ s, r₁ x * ∏ k ∈ s.erase x, g k) (∑ x ∈ s, r₂ x * ∏ k ∈ s.erase x, g k)
⊢ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
obtain ⟨-, hrr⟩ := ih hg.2 (hgg.mono (SetLike.coe_mono (Finset.subset_cons hi)))
      hr₁.2 hr₂.2 congr($hf * ∏ i ∈ s, g i + $hp0)

Premises used: HMul.hMul, congrArg, Set.Pairwise.mono, id, Finset.subset_cons, Finset.prod, And.right, HAdd.hAdd, congr, SetLike.coe_mono
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → 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))
    (hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree) (hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree)
    (hf :
      q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
        q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k),
    q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : q₁ = q₂
hpgd : Dvd.dvd.{u_1} (α := R[X]) (∏ i ∈ s, g i) (∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x)
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i = r₁ i
hpm : Monic.{u_1} (R := R) (∏ i ∈ s, g i)
hdp : degree.{u_1} (R := R) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) < degree.{u_1} (R := R) (∏ i ∈ s, g i)
hp0 : Eq.{u_1 + 1} (α := R[X]) (∑ x ∈ s, r₁ x * ∏ k ∈ s.erase x, g k) (∑ x ∈ s, r₂ x * ∏ k ∈ s.erase x, g k)
hrr : ∀ i ∈ s, r₁ i = r₂ i
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
⟨hf, (Finset.forall_mem_cons hi (fun j => r₁ j = r₂ j)).2 ⟨hr0.symm, hrr⟩⟩

Premises used: Iff.mpr, And.intro, Finset.forall_mem_cons, Eq.symm, Eq
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → 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))
    (hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree) (hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree)
    (hf :
      q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
        q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k),
    q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : q₁ = q₂
hpgd : Dvd.dvd.{u_1} (α := R[X]) (∏ i ∈ s, g i) (∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x)
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i = r₁ i
hpm : Monic.{u_1} (R := R) (∏ i ∈ s, g i)
hdp : degree.{u_1} (R := R) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) < degree.{u_1} (R := R) (∏ i ∈ s, g i)
hp0 : Eq.{u_1 + 1} (α := R[X]) (∑ x ∈ s, r₁ x * ∏ k ∈ s.erase x, g k) (∑ x ∈ s, r₂ x * ∏ k ∈ s.erase x, g k)
hrr : ∀ i ∈ s, r₁ i = r₂ i
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
exact ⟨hf, (Finset.forall_mem_cons hi (fun j => r₁ j = r₂ j)).2 ⟨hr0.symm, hrr⟩⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
obtain :
  ∀ (q : R[X]) (r : ι → R[X]) (hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k),
    ∃ (q : R[X]) (r : (i : ι) → Fin (n i) → R[X]),
      (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
        f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
⊢ ∃ (q : R[X]) (r : (i : ι) → Fin (n i) → R[X]),
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
obtain ⟨q, r, -, hf⟩ := eq_quo_mul_prod_add_sum_rem_mul_prod f
    (fun i hi => (hg i hi).pow (n i))
    (hgg.mono' fun i j hij => hij.pow)

Premises used: Polynomial.eq_quo_mul_prod_add_sum_rem_mul_prod, Polynomial.Monic.pow, Set.Pairwise.mono'
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
⊢ ∀ (i : ι),
    ∃ (q' : R[X]) (r' : Fin (n i) → R[X]),
      i ∈ s →
        (∀ (j : Fin (n i)), (r' j).degree < (g i).degree) ∧
          r i = q' * g i ^ n i + ∑ j : Fin (n i), r' j * g i ^ (↑j : ℕ)

Tactic:
have hc (i : ι) : ∃ (q' : R[X]) (r' : Fin (n i) → R[X]), i ∈ s →
      (∀ j, (r' j).degree < (g i).degree) ∧
      r i = q' * g i ^ (n i) + ∑ j, r' j * g i ^ j.1 :=
    if hi : i ∈ s then
      (eq_quo_mul_pow_add_sum_rem_mul_pow (r i) (hg i hi) (n i)).elim
        fun q' h => h.elim fun r' h => ⟨q', r', fun _ => h⟩
    else
      ⟨0, fun _ => 0, hi.elim⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
hc :
  ∀ (i : ι),
    ∃ (q' : R[X]) (r' : Fin (n i) → R[X]),
      i ∈ s →
        (∀ (j : Fin (n i)), (r' j).degree < (g i).degree) ∧
          r i = q' * g i ^ n i + ∑ j : Fin (n i), r' j * g i ^ (↑j : ℕ)
choose :
  ∀ (q' : (i : ι) → R[X]) (r' : (i : ι) → Fin (n i) → R[X])
    (hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree)
    (hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)),
    ∃ (q : R[X]) (r : (i : ι) → Fin (n i) → R[X]),
      (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
        f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
⊢ ∃ (q : R[X]) (r : (i : ι) → Fin (n i) → R[X]),
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
choose q' r' hr' hr using hc
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
⊢ ∃ (q : R[X]) (r : (i : ι) → Fin (n i) → R[X]),
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
⟨q + ∑ i ∈ s, q' i, r', hr', hf.trans ?_⟩

Premises used: HAdd.hAdd, And.intro, Exists.intro, Finset.sum, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
refine :
  q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
    (q + ∑ i ∈ s, q' i) * ∏ i ∈ s, g i ^ n i +
      ∑ i ∈ s, ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
⊢ ∃ (q : R[X]) (r : (i : ι) → Fin (n i) → R[X]),
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
refine ⟨q + ∑ i ∈ s, q' i, r', hr', hf.trans ?_⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
rw :
  Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k)
    (∑ x ∈ s, (q' x * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n x), r' x j * g x ^ (↑j : ℕ) * ∏ k ∈ s.erase x, g k ^ n k))
⊢ q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
    (q + ∑ i ∈ s, q' i) * ∏ i ∈ s, g i ^ n i +
      ∑ i ∈ s, ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
rw [add_mul, add_assoc, add_right_inj, Finset.sum_mul, ← Finset.sum_add_distrib]

Premises used: add_mul, Finset.sum_add_distrib, add_assoc, add_right_inj, Finset.sum_mul
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
⊢ Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k)
    (∑ x ∈ s, (q' x * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n x), r' x j * g x ^ (↑j : ℕ) * ∏ k ∈ s.erase x, g k ^ n k))

Tactic:
Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
refine :
  ∀ (i : ι) (hi : i ∈ s),
    r i * ∏ k ∈ s.erase i, g k ^ n k =
      q' i * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
⊢ Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k)
    (∑ x ∈ s, (q' x * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n x), r' x j * g x ^ (↑j : ℕ) * ∏ k ∈ s.erase x, g k ^ n k))

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
i : ι
hi : i ∈ s
rw :
  r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
rw₁ :
  (q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)) * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
rw₂ :
  q' i * g i ^ n i * ∏ k ∈ s.erase i, g k ^ n k +
      HMul.hMul (α := R[X]) (∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)) (∏ k ∈ s.erase i, g k ^ n k) =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
rw₃ :
  q' i * g i ^ n i * ∏ k ∈ s.erase i, g k ^ n k +
      ∑ i_1 : Fin (n i), r' i i_1 * g i ^ (↑i_1 : ℕ) * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
rw₄ rw₅ :
  q' i * (g i ^ n i * ∏ k ∈ s.erase i, g k ^ n k) +
      ∑ i_1 : Fin (n i), r' i i_1 * g i ^ (↑i_1 : ℕ) * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
⊢ r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
rw [← Finset.mul_prod_erase s _ hi, hr i hi, add_mul, Finset.sum_mul, mul_assoc]

Premises used: add_mul, mul_assoc, Finset.mul_prod_erase, Finset.sum_mul
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r₁ i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r₂ i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r₁ i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r₂ i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
h : Nontrivial R
⊢ q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)

Tactic:
simp only [← Finset.sum_mul] at hf

Premises used: Finset.sum_mul
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ degree.{u_1} (R := R) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ)) < (g i ^ n i).degree

Tactic:
(degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff ?_).2 fun j _ => ?_)

Premises used: Iff.mpr, Polynomial.degree_sum_le, Finset.sup_lt_iff, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
refine_1 : ⊥ < (g i ^ n i).degree
refine_2 :
  ∀ (j : Fin (n i)),
    Membership.mem (γ := Finset (Fin (n i))) Finset.univ j → (r i j * g i ^ (↑j : ℕ)).degree < (g i ^ n i).degree
⊢ degree.{u_1} (R := R) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ)) < (g i ^ n i).degree

Tactic:
refine (degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff ?_).2 fun j _ => ?_)

Premises used: Iff.mpr, Polynomial.degree_sum_le, Finset.sup_lt_iff, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
refine_1 : g i ^ n i ≠ 0
⊢ ⊥ < (g i ^ n i).degree

Tactic:
rw [bot_lt_iff_ne_bot, degree_ne_bot]

Premises used: bot_lt_iff_ne_bot, Polynomial.degree_ne_bot