awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
cop : IsCoprime (g i) (∏ i ∈ s, g i)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hf₁ : q₁ * (g i * ∏ x ∈ s, g x) + (r₁ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₁ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k) =
  q₂ * (g i * ∏ x ∈ s, g x) + (r₂ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₂ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k)
Tactic: rw [Finset.prod_cons, Finset.sum_cons, Finset.sum_cons, Finset.erase_cons] at hf
Cleared hypotheses: hf, cop
-- 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
hf :
  q₁ * (g i * ∏ x ∈ s, g x) + (r₁ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₁ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k) =
    q₂ * (g i * ∏ x ∈ s, g x) + (r₂ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₂ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k)
cop : IsCoprime (g i) (∏ i ∈ s, g i)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
Tactic: have hjs {j : ι} (hj : j ∈ s) : i ≠ j := fun hij => hi (hij ▸ 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
hf :
  q₁ * (g i * ∏ x ∈ s, g x) + (r₁ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₁ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k) =
    q₂ * (g i * ∏ x ∈ s, g x) + (r₂ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₂ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k)
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hf₁ : g i * (q₁ * ∏ x ∈ s, g x) + (r₁ i * ∏ x ∈ s, g x + g i * ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x) =
  g i * (q₂ * ∏ x ∈ s, g x) + (r₂ i * ∏ x ∈ s, g x + g i * ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)
Tactic: simp +contextual only [Finset.erase_cons_of_ne hi (hjs _),
      Finset.prod_cons, ← mul_left_comm (g i), ← Finset.mul_sum] at hf
Cleared hypotheses: hf
-- 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
hf :
  g i * (q₁ * ∏ x ∈ s, g x) + (r₁ i * ∏ x ∈ s, g x + g i * ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x) =
    g i * (q₂ * ∏ x ∈ s, g x) + (r₂ i * ∏ x ∈ s, g x + g i * ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hf₁ : r₁ i * ∏ x ∈ s, g x + g i * (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x) =
  r₂ i * ∏ x ∈ s, g x + g i * (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)
Tactic: rw [add_left_comm, ← mul_add, add_left_comm, ← mul_add] at hf
Cleared hypotheses: hf
-- 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
hf :
  r₁ i * ∏ x ∈ s, g x + g i * (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x) =
    r₂ i * ∏ x ∈ s, g x + g i * (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hf₁ : g i *
    (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x -
      (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)) =
  (r₂ i - r₁ i) * ∏ x ∈ s, g x
Tactic: rw [← sub_eq_zero, add_sub_add_comm, ← sub_mul, ← mul_sub,
      ← neg_sub, neg_mul, neg_add_eq_sub, sub_eq_zero] at hf
Cleared hypotheses: hf
-- 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
hf :
  g i *
      (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x -
        (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)) =
    (r₂ i - r₁ i) * ∏ x ∈ s, g x
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hgid : g i ∣ r₂ i - r₁ i
Tactic: have hgid : g i ∣ r₂ i - r₁ i := cop.dvd_of_dvd_mul_right (hf ▸ dvd_mul_right _ _)
-- 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
hf :
  g i *
      (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x -
        (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)) =
    (r₂ i - r₁ i) * ∏ x ∈ s, g x
hgid : g i ∣ r₂ i - r₁ i
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hf₁ : g i * ∑ x ∈ s, (r₁ x * ∏ x ∈ s.erase x, g x - r₂ x * ∏ x ∈ s.erase x, g x) =
  (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
Tactic: rw [add_sub_add_comm, ← sub_mul, mul_add, ← mul_assoc,
      ← eq_sub_iff_add_eq', ← sub_mul, ← Finset.sum_sub_distrib] at hf
Cleared hypotheses: hf, hgid
-- 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
hf :
  g i * ∑ x ∈ s, (r₁ x * ∏ x ∈ s.erase x, g x - r₂ x * ∏ x ∈ s.erase x, g x) =
    (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hgid : g i ∣ r₂ i - r₁ i
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have 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
Tactic: simp only [← sub_mul] at hf
Cleared hypotheses: hf
-- 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
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hpgd : Dvd.dvd.{u_1} (α := R[X]) (∏ i ∈ s, g i) (∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x)
Tactic: have hpgd : ∏ i ∈ s, g i ∣ _ := cop.symm.dvd_of_dvd_mul_left (hf.symm ▸ dvd_mul_left _ _)
-- 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)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hdr : (r₂ i - r₁ i).degree < (g i).degree
Tactic: have hdr : (r₂ i - r₁ i).degree < (g i).degree :=
      (degree_sub_le (r₂ i) (r₁ i)).trans_lt (max_lt hr₂.1 hr₁.1)
-- 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
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hr0 : r₂ i - r₁ i = 0
Tactic: have hr0 : r₂ i - r₁ i = 0 := (hg.1.not_dvd_of_degree_lt · hdr).mtr hgid
-- 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
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hpm : Monic.{u_1} (R := R) (∏ i ∈ s, g i)
Tactic: have hpm : (∏ i ∈ s, g i).Monic := monic_prod_of_monic s g hg.2
-- 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)
⊢ 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)
have refine_1 : ⊥ < degree.{u_1} (R := R) (∏ i ∈ s, g i)
Tactic: refine (degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff ?_).2 ?_)
-- 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)
refine_1 : ⊥ < degree.{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)
have refine_2 : ∀ b ∈ s, ((r₁ b - r₂ b) * ∏ k ∈ s.erase b, g k).degree < degree.{u_1} (R := R) (∏ i ∈ s, g i)
Tactic: refine (degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff ?_).2 ?_)
-- 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)
⊢ ⊥ < degree.{u_1} (R := R) (∏ i ∈ s, g i)
have refine_1 : Ne.{u_1 + 1} (α := R[X]) (∏ i ∈ s, g i) 0
Tactic: rw [bot_lt_iff_ne_bot, degree_ne_bot]
-- 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) (∏ i ∈ s, g i)
have refine_2 : ((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
Tactic: rw [← Finset.mul_prod_erase s g hj, mul_comm (g j), (hg.2 j hj).degree_mul]