awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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)
j : ι
hj : j ∈ s
⊢ ((r₁ j - r₂ j) * ∏ k ∈ s.erase j, g k).degree < degree.{u_1} (R := R) (∏ x ∈ s.erase j, g x) + (g j).degree
have refine_2 : (r₁ j - r₂ j).degree + degree.{u_1} (R := R) (∏ k ∈ s.erase j, g k) <
  degree.{u_1} (R := R) (∏ x ∈ s.erase j, g x) + (g j).degree
Tactic: refine (degree_mul_le (r₁ j - r₂ j) (∏ k ∈ s.erase j, g k)).trans_lt ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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)
j : ι
hj : j ∈ s
⊢ degree.{u_1} (R := R) (∏ k ∈ s.erase j, g k) ≠ ⊥
have rw : Ne.{u_1 + 1} (α := R[X]) (∏ k ∈ s.erase j, g k) 0
Tactic: rw [degree_ne_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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)
j : ι
hj : j ∈ s
⊢ (r₁ j - r₂ j).degree + degree.{u_1} (R := R) (∏ k ∈ s.erase j, g k) <
    degree.{u_1} (R := R) (∏ x ∈ s.erase j, g x) + (g j).degree
have dnb : degree.{u_1} (R := R) (∏ k ∈ s.erase j, g k) ≠ ⊥
Tactic: have dnb : (∏ k ∈ s.erase j, g k).degree ≠ ⊥ := by
          rw [degree_ne_bot]
          exact (monic_prod_of_monic _ g
            fun j hj => hg.2 j (Finset.mem_of_mem_erase hj)).ne_zero_of_polynomial_ne
            fun h : r₂ i - r₁ i = g i => lt_irrefl _ (h ▸ hdr)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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)
j : ι
hj : j ∈ s
dnb : degree.{u_1} (R := R) (∏ k ∈ s.erase j, g k) ≠ ⊥
⊢ (r₁ j - r₂ j).degree + degree.{u_1} (R := R) (∏ k ∈ s.erase j, g k) <
    degree.{u_1} (R := R) (∏ x ∈ s.erase j, g x) + (g j).degree
have refine_2 : (r₁ j - r₂ j).degree < (g j).degree
Tactic: rw [add_comm, WithBot.add_lt_add_iff_left dnb]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have 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)
Tactic: have hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree := by
      refine (degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff ?_).2 ?_)
      · rw [bot_lt_iff_ne_bot, degree_ne_bot]
        exact hpm.ne_zero_of_polynomial_ne fun h : r₂ i - r₁ i = g i => lt_irrefl _ (h ▸ hdr)
      · intro j hj
        rw [← Finset.mul_prod_erase s g hj, mul_comm (g j), (hg.2 j hj).degree_mul]
        refine (degree_mul_le (r₁ j - r₂ j) (∏ k ∈ s.erase j, g k)).trans_lt ?_
        have dnb : (∏ k ∈ s.erase j, g k).degree ≠ ⊥ := by
          rw [degree_ne_bot]
          exact (monic_prod_of_monic _ g
            fun j hj => hg.2 j (Finset.mem_of_mem_erase hj)).ne_zero_of_polynomial_ne
            fun h : r₂ i - r₁ i = g i => lt_irrefl _ (h ▸ hdr)
        rw [add_comm, WithBot.add_lt_add_iff_left dnb]
        exact (degree_sub_le (r₁ j) (r₂ j)).trans_lt (max_lt (hr₁.2 j hj) (hr₂.2 j hj))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hp0 : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k) 0
Tactic: have hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0 :=
      (hpm.not_dvd_of_degree_lt · hdp).mtr hpgd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hf₁ : 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
Cleared hypotheses: hf, hpgd, hdr, hr0, hpm, hdp, hp0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have 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
Tactic: simp only [sub_mul, Finset.sum_sub_distrib] at hp0
Cleared hypotheses: hp0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hf₁ : q₁ = q₂
Tactic: rw [sub_eq_zero] at hf hr0 hp0
Cleared hypotheses: hf, hpgd, hdr, hr0, hpm, hdp, hp0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hr0₁ : r₂ i = r₁ i
Tactic: rw [sub_eq_zero] at hf hr0 hp0
Cleared hypotheses: hf, hpgd, hdr, hr0, hpm, hdp, hp0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have 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)
Tactic: rw [sub_eq_zero] at hf hr0 hp0
Cleared hypotheses: hf, hpgd, hdr, hr0, hpm, hdp, hp0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hrr : ∀ 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)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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 : (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
have 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
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)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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 : 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
have 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 : ℕ)
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⟩