awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : ∀ i_1 ∈ Finset.cons i s hi, (g i_1).Monic
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
hg₁ : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
⊢ (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)

Tactic:
rw [Finset.forall_mem_cons] at hg

Premises used: Finset.forall_mem_cons
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
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)
⊢ ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)

Tactic:
rw [Finset.coe_cons, Set.pairwise_insert] at hgg

Premises used: Finset.coe_cons, Set.pairwise_insert
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
cons :
  ∀ (q : R[X]) (r : ι → R[X]) (hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
        f =
          q * ∏ i ∈ Finset.cons i s hi, g i +
            ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k

Tactic:
obtain ⟨q, r, -, hf⟩ := ih hg.2 hgg.1

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
⊢ ∀ {j : ι} (hj : j ∈ s), i ≠ j

Tactic:
have hjs {j : ι} (hj : j ∈ s) : i ≠ j := fun hij => hi (hij ▸ hj)
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
⊢ ∀ (j : ι), ∃ (a : R[X]) (b : R[X]), j ∈ s → a * g i + b * g j = 1

Tactic:
have hc (j : ι) : ∃ a b, j ∈ s → a * g i + b * g j = 1 :=
      if h : j ∈ s ∧ i ≠ j then
        (hgg.2 j h.1 h.2).1.elim fun a h => h.elim fun b h => ⟨a, b, fun _ => h⟩
      else
        ⟨0, 0, fun hj => (h ⟨hj, hjs hj⟩).elim⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
hc : ∀ (j : ι), ∃ (a : R[X]) (b : R[X]), j ∈ s → a * g i + b * g j = 1
cons :
  ∀ (a b : (j : ι) → R[X]) (hab : ∀ j ∈ s, a j * g i + b j * g j = 1),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
        f =
          q * ∏ i ∈ Finset.cons i s hi, g i +
            ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k

Tactic:
choose a b hab 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 ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k

Tactic:
⟨(q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j),
      Function.update (fun j => r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i),
      ?_, hf.trans ?_⟩

Premises used: Function.update, HMul.hMul, Polynomial.divByMonic, HAdd.hAdd, Polynomial.modByMonic, 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 ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
cons :
  ∀ i_1 ∈ Finset.cons i s hi,
    degree.{u_1} (R := R)
        (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
          ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1) <
      (g i_1).degree
cons₁ :
  q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ((q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) *
        ∏ i ∈ Finset.cons i s hi, g i +
      ∑ i_1 ∈ Finset.cons i s hi,
        HMul.hMul (α := R[X]) (β := R[X])
          (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
              ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1 :
            R[X])
          (∏ k ∈ (Finset.cons i s hi).erase i_1, g k : R[X])
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k

Tactic:
refine ⟨(q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j),
      Function.update (fun j => r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i),
      ?_, 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 ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
cons :
  ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i).degree < (g i).degree ∧
    ∀ x ∈ s,
      degree.{u_1} (R := R)
          (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
            ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x) <
        (g x).degree
⊢ ∀ i_1 ∈ Finset.cons i s hi,
    degree.{u_1} (R := R)
        (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
          ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1) <
      (g i_1).degree

Tactic:
rw [Finset.forall_mem_cons, Function.update_self]

Premises used: Finset.forall_mem_cons, Function.update_self
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i).degree < (g i).degree ∧
    ∀ x ∈ s,
      degree.{u_1} (R := R)
          (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
            ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x) <
        (g x).degree

Tactic:
⟨degree_modByMonic_lt _ hg.1, fun j hj => ?_⟩

Premises used: And.left, And.intro, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
cons :
  ∀ (j : ι) (hj : j ∈ s),
    degree.{u_1} (R := R)
        (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
          ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) j) <
      (g j).degree
⊢ ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i).degree < (g i).degree ∧
    ∀ x ∈ s,
      degree.{u_1} (R := R)
          (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
            ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x) <
        (g x).degree

Tactic:
refine ⟨degree_modByMonic_lt _ hg.1, fun j hj => ?_⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
cons : (r j * a j %ₘ g j).degree < (g j).degree
⊢ degree.{u_1} (R := R)
      (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
        ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) j) <
    (g j).degree

Tactic:
rw [Function.update_of_ne (hjs hj).symm]

Premises used: Ne.symm, Function.update_of_ne
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ (r j * a j %ₘ g j).degree < (g j).degree

Tactic:
degree_modByMonic_lt _ (hg.2 j hj)

Premises used: And.right, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ (r j * a j %ₘ g j).degree < (g j).degree

Tactic:
exact degree_modByMonic_lt _ (hg.2 j hj)

Premises used: And.right, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_2
inst_2 : DecidableEq ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
cons :
  Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k)
    (∑ x ∈ s,
      (r x * b x %ₘ g i * ∏ x ∈ s, g x +
        ((r x * b x /ₘ g i + r x * a x /ₘ g x) * (g i * ∏ x ∈ s, g x) +
          HMul.hMul (α := R[X]) (β := R[X])
            (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
                ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x :
              R[X])
            (∏ k ∈ (Finset.cons i s hi).erase x, g k : R[X]))))
⊢ q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ((q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) *
        ∏ i ∈ Finset.cons i s hi, g i +
      ∑ i_1 ∈ Finset.cons i s hi,
        HMul.hMul (α := R[X]) (β := R[X])
          (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
              ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1 :
            R[X])
          (∏ k ∈ (Finset.cons i s hi).erase i_1, g k : R[X])

Tactic:
rw [Finset.prod_cons, Finset.sum_cons, Function.update_self, Finset.erase_cons, add_mul,
        add_add_add_comm, ← mul_assoc, ← add_mul, add_comm (_ * g i), ← mul_comm (g i),
        modByMonic_add_div, add_mul, add_assoc, add_right_inj, Finset.sum_mul,
        Finset.sum_mul, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]

Premises used: add_mul, HMul.hMul, Finset.sum_cons, Finset.sum_add_distrib, add_assoc, mul_assoc, Finset.erase_cons, add_comm, Polynomial.modByMonic_add_div, Finset.prod_cons, mul_comm, add_add_add_comm, Function.update_self, 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 ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k)
    (∑ x ∈ s,
      (r x * b x %ₘ g i * ∏ x ∈ s, g x +
        ((r x * b x /ₘ g i + r x * a x /ₘ g x) * (g i * ∏ x ∈ s, g x) +
          HMul.hMul (α := R[X]) (β := R[X])
            (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
                ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x :
              R[X])
            (∏ k ∈ (Finset.cons i s hi).erase x, g k : R[X]))))

Tactic:
Finset.sum_congr rfl fun j hj => ?_

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 ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
cons :
  ∀ (j : ι) (hj : j ∈ s),
    r j * ∏ k ∈ s.erase j, g k =
      r j * b j %ₘ g i * ∏ x ∈ s, g x +
        ((r j * b j /ₘ g i + r j * a j /ₘ g j) * (g i * ∏ x ∈ s, g x) +
          HMul.hMul (α := R[X]) (β := R[X])
            (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
                ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) j :
              R[X])
            (∏ k ∈ (Finset.cons i s hi).erase j, g k : R[X]))
⊢ Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k)
    (∑ x ∈ s,
      (r x * b x %ₘ g i * ∏ x ∈ s, g x +
        ((r x * b x /ₘ g i + r x * a x /ₘ g x) * (g i * ∏ x ∈ s, g x) +
          HMul.hMul (α := R[X]) (β := R[X])
            (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
                ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x :
              R[X])
            (∏ k ∈ (Finset.cons i s hi).erase x, g k : R[X]))))

Tactic:
refine Finset.sum_congr rfl fun j hj => ?_

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 ι
f : R[X]
g : ι → 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)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
cons :
  r j * ∏ k ∈ s.erase j, g k =
    r j * b j %ₘ g i * (g j * ∏ x ∈ s.erase j, g x) +
      ((r j * b j /ₘ g i + r j * a j /ₘ g j) * (g i * (g j * ∏ x ∈ s.erase j, g x)) +
        r j * a j %ₘ g j * (g i * ∏ x ∈ s.erase j, g x))
⊢ r j * ∏ k ∈ s.erase j, g k =
    r j * b j %ₘ g i * ∏ x ∈ s, g x +
      ((r j * b j /ₘ g i + r j * a j /ₘ g j) * (g i * ∏ x ∈ s, g x) +
        HMul.hMul (α := R[X]) (β := R[X])
          (Function.update (β := fun (a : ι) ↦ R[X]) (fun (j : ι) ↦ r j * a j %ₘ g j) i
              ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) j :
            R[X])
          (∏ k ∈ (Finset.cons i s hi).erase j, g k : R[X]))

Tactic:
rw [Function.update_of_ne (hjs hj).symm, Finset.erase_cons_of_ne _ (hjs hj),
        Finset.prod_cons, ← Finset.mul_prod_erase s g hj]

Premises used: Ne.symm, Finset.mul_prod_erase, Finset.prod_cons, Finset.erase_cons_of_ne, Function.update_of_ne