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 : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
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 : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) 0
⊢ q₁ - q₂ = 0

Tactic:
rw [hr0, hp0, mul_zero, zero_sub, neg_mul, eq_comm, neg_eq_zero,
      ← mul_rotate, (hpm.mul hg.1).mul_right_eq_zero_iff] at hf

Premises used: neg_eq_zero, Polynomial.Monic.mul_right_eq_zero_iff, eq_comm, MulZeroClass.mul_zero, And.left, neg_mul, Polynomial.Monic.mul, mul_rotate, zero_sub
-- 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 : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
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 : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) 0
hf₁ : q₁ - q₂ = 0
⊢ Dvd.dvd.{u_1} (α := R[X]) (∏ i ∈ s, g i) (∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x)

Tactic:
rw [hr0, hp0, mul_zero, zero_sub, neg_mul, eq_comm, neg_eq_zero,
      ← mul_rotate, (hpm.mul hg.1).mul_right_eq_zero_iff] at hf

Premises used: neg_eq_zero, Polynomial.Monic.mul_right_eq_zero_iff, eq_comm, MulZeroClass.mul_zero, And.left, neg_mul, Polynomial.Monic.mul, mul_rotate, zero_sub
-- 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 : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
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 : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) 0
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)
⊢ (r₂ i - r₁ i).degree < (g i).degree

Tactic:
rw [hr0, hp0, mul_zero, zero_sub, neg_mul, eq_comm, neg_eq_zero,
      ← mul_rotate, (hpm.mul hg.1).mul_right_eq_zero_iff] at hf

Premises used: neg_eq_zero, Polynomial.Monic.mul_right_eq_zero_iff, eq_comm, MulZeroClass.mul_zero, And.left, neg_mul, Polynomial.Monic.mul, mul_rotate, zero_sub
-- 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 : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
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 : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) 0
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
⊢ r₂ i - r₁ i = 0

Tactic:
rw [hr0, hp0, mul_zero, zero_sub, neg_mul, eq_comm, neg_eq_zero,
      ← mul_rotate, (hpm.mul hg.1).mul_right_eq_zero_iff] at hf

Premises used: neg_eq_zero, Polynomial.Monic.mul_right_eq_zero_iff, eq_comm, MulZeroClass.mul_zero, And.left, neg_mul, Polynomial.Monic.mul, mul_rotate, zero_sub
-- 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 : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
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 : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) 0
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
⊢ Monic.{u_1} (R := R) (∏ i ∈ s, g i)

Tactic:
rw [hr0, hp0, mul_zero, zero_sub, neg_mul, eq_comm, neg_eq_zero,
      ← mul_rotate, (hpm.mul hg.1).mul_right_eq_zero_iff] at hf

Premises used: neg_eq_zero, Polynomial.Monic.mul_right_eq_zero_iff, eq_comm, MulZeroClass.mul_zero, And.left, neg_mul, Polynomial.Monic.mul, mul_rotate, zero_sub
-- 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 : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
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 : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) 0
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)
⊢ 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 [hr0, hp0, mul_zero, zero_sub, neg_mul, eq_comm, neg_eq_zero,
      ← mul_rotate, (hpm.mul hg.1).mul_right_eq_zero_iff] at hf

Premises used: neg_eq_zero, Polynomial.Monic.mul_right_eq_zero_iff, eq_comm, MulZeroClass.mul_zero, And.left, neg_mul, Polynomial.Monic.mul, mul_rotate, zero_sub
-- 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 : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
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 : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) 0
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)
⊢ Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) 0

Tactic:
rw [hr0, hp0, mul_zero, zero_sub, neg_mul, eq_comm, neg_eq_zero,
      ← mul_rotate, (hpm.mul hg.1).mul_right_eq_zero_iff] at hf

Premises used: neg_eq_zero, Polynomial.Monic.mul_right_eq_zero_iff, eq_comm, MulZeroClass.mul_zero, And.left, neg_mul, Polynomial.Monic.mul, mul_rotate, zero_sub
-- 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 : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) 0
⊢ 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

Tactic:
simp only [sub_mul, Finset.sum_sub_distrib] at hp0

Premises used: sub_mul, Finset.sum_sub_distrib
-- 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
⊢ q₁ = q₂

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₂
⊢ Dvd.dvd.{u_1} (α := R[X]) (∏ i ∈ s, g i) (∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x)

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)
⊢ (r₂ i - r₁ i).degree < (g i).degree

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
⊢ r₂ i = r₁ 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
⊢ Monic.{u_1} (R := R) (∏ i ∈ s, g i)

Tactic:
rw [sub_eq_zero] at hf hr0 hp0

Premises used: sub_eq_zero