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 : (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 + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)) *
      ∏ k ∈ s.erase j, g k
⊢ 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))

Tactic:
simp_rw [← mul_assoc, ← add_mul]

Premises used: add_mul, mul_assoc
-- 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 * ∏ k ∈ s.erase j, g k =
    (r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)) *
      ∏ k ∈ s.erase j, g k

Tactic:
congrArg (· * _) ?_

Premises used: HMul.hMul, congrArg
-- 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 = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)
⊢ r j * ∏ k ∈ s.erase j, g k =
    (r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)) *
      ∏ k ∈ s.erase j, g k

Tactic:
refine congrArg (· * _) ?_

Premises used: HMul.hMul, congrArg
-- 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 = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i * g i + r j * a j /ₘ g j * g i) * g j + r j * a j %ₘ g j * g i)
cons₁ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₂ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j) + r j * a j %ₘ g j * g i
cons₃ :
  r j = r j * b j %ₘ g i * g j + r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₄ : r j = (r j * b j %ₘ g i + r j * b j /ₘ g i * g i) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₅ :
  r j = (r j * b j %ₘ g i + g i * (r j * b j /ₘ g i)) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₆ : r j = r j * b j * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₇ : r j = r j * b j * g j + (r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₈ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j * g i + r j * a j %ₘ g j * g i)
cons₉ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j + r j * a j %ₘ g j) * g i
cons₁₀ : r j = r j * b j * g j + (r j * a j %ₘ g j + r j * a j /ₘ g j * g j) * g i
cons₁₁ : r j = r j * b j * g j + (r j * a j %ₘ g j + g j * (r j * a j /ₘ g j)) * g i
cons₁₂ : r j = r j * b j * g j + r j * a j * g i
cons₁₃ : r j = r j * (b j * g j) + r j * a j * g i
cons₁₄ : r j = r j * (b j * g j) + r j * (a j * g i)
cons₁₅ : r j = r j * (b j * g j + a j * g i)
cons₁₆ : r j = r j * (a j * g i + b j * g j)
cons₁₇ : r j = r j * 1
cons₁₈ cons₁₉ : r j = r j
⊢ r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)

Tactic:
rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]

Premises used: add_mul, HMul.hMul, add_assoc, mul_assoc, Polynomial.divByMonic, add_comm, mul_right_comm, Polynomial.modByMonic, Polynomial.modByMonic_add_div, mul_comm, mul_add, mul_one
-- 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]
hg : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (g i).Monic
hgg : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
hr₁ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (r₁ i).degree < (g i).degree
hr₂ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (r₂ i).degree < (g i).degree
hf :
  q₁ * ∏ i ∈ ∅, g i + ∑ i ∈ ∅, r₁ i * ∏ k ∈ Finset.erase ∅ i, g k =
    q₂ * ∏ i ∈ ∅, g i + ∑ i ∈ ∅, r₂ i * ∏ k ∈ Finset.erase ∅ i, g k
⊢ q₁ = q₂ ∧ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → r₁ i = r₂ i

Tactic:
simpa using hf
-- 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 : ∀ 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)
hr₁ : ∀ i_1 ∈ Finset.cons i s hi, (r₁ i_1).degree < (g i_1).degree
hr₂ : ∀ i_1 ∈ Finset.cons i s hi, (r₂ i_1).degree < (g i_1).degree
hf :
  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₂ * ∏ 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
⊢ (g i).Monic ∧ ∀ x ∈ s, (g x).Monic

Tactic:
rw [Finset.forall_mem_cons] at hg hr₁ hr₂

Premises used: Finset.forall_mem_cons
-- 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 : ∀ 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)
hr₁ : ∀ i_1 ∈ Finset.cons i s hi, (r₁ i_1).degree < (g i_1).degree
hr₂ : ∀ i_1 ∈ Finset.cons i s hi, (r₂ i_1).degree < (g i_1).degree
hf :
  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₂ * ∏ 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
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 hr₁ hr₂

Premises used: Finset.forall_mem_cons
-- 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 : ∀ 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)
hr₁ : ∀ i_1 ∈ Finset.cons i s hi, (r₁ i_1).degree < (g i_1).degree
hr₂ : ∀ i_1 ∈ Finset.cons i s hi, (r₂ i_1).degree < (g i_1).degree
hf :
  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₂ * ∏ 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
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)
⊢ (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree

Tactic:
rw [Finset.forall_mem_cons] at hg hr₁ hr₂

Premises used: Finset.forall_mem_cons
-- 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 : ∀ 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)
hr₁ : ∀ i_1 ∈ Finset.cons i s hi, (r₁ i_1).degree < (g i_1).degree
hr₂ : ∀ i_1 ∈ Finset.cons i s hi, (r₂ i_1).degree < (g i_1).degree
hf :
  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₂ * ∏ 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
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
⊢ (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree

Tactic:
rw [Finset.forall_mem_cons] at hg hr₁ hr₂

Premises used: Finset.forall_mem_cons
-- 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 : ∀ 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)
hr₁ : ∀ i_1 ∈ Finset.cons i s hi, (r₁ i_1).degree < (g i_1).degree
hr₂ : ∀ i_1 ∈ Finset.cons i s hi, (r₂ i_1).degree < (g i_1).degree
hf :
  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₂ * ∏ 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
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
⊢ 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₂ * ∏ 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:
rw [Finset.forall_mem_cons] at hg hr₁ hr₂

Premises used: Finset.forall_mem_cons
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
i : ι
hi : i ∉ ∅
hgg : (↑(Finset.cons i ∅ hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (∏ i ∈ ∅, g i)

Tactic:
simp [isCoprime_one_right]

Premises used: isCoprime_one_right
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
cons : IsCoprime (g i) (g j) ∧ IsCoprime (g i) (∏ x ∈ s, g x)
⊢ IsCoprime (g i) (∏ i ∈ Finset.cons j s hj, g i)

Tactic:
rw [Finset.prod_cons, IsCoprime.mul_right_iff]

Premises used: IsCoprime.mul_right_iff, Finset.prod_cons
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ i ∈ (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ j ∈ (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
hij : i = j
⊢ i ∈ Finset.cons j s hj

Tactic:
simp [hij]
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
cons : i ∉ s
cons₁ : (↑(Finset.cons i s ⋯) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (g j) ∧ IsCoprime (g i) (∏ x ∈ s, g x)

Tactic:
refine ⟨hgg (by simp) (by simp) fun hij => hi (by simp [hij]), ih ?_ ?_⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ i ∉ s

Tactic:
mt Finset.mem_cons_of_mem hi

Premises used: Finset.mem_cons_of_mem, mt
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ i ∉ s

Tactic:
exact mt Finset.mem_cons_of_mem hi

Premises used: Finset.mem_cons_of_mem, mt
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ (↑(Finset.cons i s ⋯) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)

Tactic:
hgg.mono (SetLike.coe_mono (Finset.cons_subset_cons.2 (Finset.subset_cons hj)))

Premises used: Iff.mpr, Finset.cons_subset_cons, Set.Pairwise.mono, Finset.subset_cons, 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]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ (↑(Finset.cons i s ⋯) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)

Tactic:
exact hgg.mono (SetLike.coe_mono (Finset.cons_subset_cons.2 (Finset.subset_cons hj)))

Premises used: Set.Pairwise.mono, 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]
i : ι
s : Finset ι
hi : i ∉ s
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
empty :
  ∀ (hi : i ∉ ∅) (hgg : (↑(Finset.cons i ∅ hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ ∅, g i)
cons :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
    (ih :
      ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
        IsCoprime (g i) (∏ i ∈ s, g i))
    (hi : i ∉ Finset.cons j s hj)
    (hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ Finset.cons j s hj, g i)
⊢ IsCoprime (g i) (∏ i ∈ s, g i)

Tactic:
induction s using Finset.cons_induction with
      | empty => simp [isCoprime_one_right]
      | cons j s hj ih =>
        rw [Finset.prod_cons, IsCoprime.mul_right_iff]
        refine ⟨hgg (by simp) (by simp) fun hij => hi (by simp [hij]), ih ?_ ?_⟩
        · exact mt Finset.mem_cons_of_mem hi
        · exact hgg.mono (SetLike.coe_mono (Finset.cons_subset_cons.2 (Finset.subset_cons hj)))

Premises used: Finset.mem_cons_of_mem, mt, IsCoprime.mul_right_iff, isCoprime_one_right, Finset.prod_cons
-- 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
hf :
  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₂ * ∏ 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
⊢ IsCoprime (g i) (∏ i ∈ s, g i)

Tactic:
have cop : IsCoprime (g i) (∏ i ∈ s, g i) := by
      clear *-hgg
      induction s using Finset.cons_induction with
      | empty => simp [isCoprime_one_right]
      | cons j s hj ih =>
        rw [Finset.prod_cons, IsCoprime.mul_right_iff]
        refine ⟨hgg (by simp) (by simp) fun hij => hi (by simp [hij]), ih ?_ ?_⟩
        · exact mt Finset.mem_cons_of_mem hi
        · exact hgg.mono (SetLike.coe_mono (Finset.cons_subset_cons.2 (Finset.subset_cons hj)))