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
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
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 : ℕ)
⊢ ∃ (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 choose : ∀ (q' : (i : ι) → R[X]) (r' : (i : ι) → Fin (n i) → R[X])
  (hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree)
  (hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)),
  ∃ (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: choose q' r' hr' hr using hc
Cleared hypotheses: hc
-- 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 : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
⊢ ∃ (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 refine : q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
  (q + ∑ i ∈ s, q' i) * ∏ 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: refine ⟨q + ∑ i ∈ s, q' i, r', hr', hf.trans ?_⟩
-- 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 : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
⊢ q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
    (q + ∑ i ∈ s, q' i) * ∏ 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 rw : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k)
  (∑ x ∈ s, (q' x * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n x), r' x j * g x ^ (↑j : ℕ) * ∏ k ∈ s.erase x, g k ^ n k))
Tactic: rw [add_mul, add_assoc, add_right_inj, Finset.sum_mul, ← Finset.sum_add_distrib]
-- 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 : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
⊢ Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k)
    (∑ x ∈ s, (q' x * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n x), r' x j * g x ^ (↑j : ℕ) * ∏ k ∈ s.erase x, g k ^ n k))
have refine : ∀ (i : ι) (hi : i ∈ s),
  r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
Tactic: refine Finset.sum_congr rfl fun i hi => ?_
-- 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 : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
i : ι
hi : i ∈ s
⊢ r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
have rw : r i * ∏ k ∈ s.erase i, g k ^ n k =
  q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
    ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
Tactic: rw [← Finset.mul_prod_erase s _ hi, hr i hi, add_mul, Finset.sum_mul, mul_assoc]
-- 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 : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
i : ι
hi : i ∈ s
rw :
  r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
⊢ r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
have rw₁ : (q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)) * ∏ k ∈ s.erase i, g k ^ n k =
  q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
    ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
Tactic: rw [← Finset.mul_prod_erase s _ hi, hr i hi, add_mul, Finset.sum_mul, mul_assoc]
-- 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 : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
i : ι
hi : i ∈ s
rw :
  r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
rw₁ :
  (q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)) * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
⊢ r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
have rw₂ : q' i * g i ^ n i * ∏ k ∈ s.erase i, g k ^ n k +
    HMul.hMul (α := R[X]) (∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)) (∏ k ∈ s.erase i, g k ^ n k) =
  q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
    ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
Tactic: rw [← Finset.mul_prod_erase s _ hi, hr i hi, add_mul, Finset.sum_mul, mul_assoc]
-- 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 : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
i : ι
hi : i ∈ s
rw :
  r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
rw₁ :
  (q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)) * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
rw₂ :
  q' i * g i ^ n i * ∏ k ∈ s.erase i, g k ^ n k +
      HMul.hMul (α := R[X]) (∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)) (∏ k ∈ s.erase i, g k ^ n k) =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
⊢ r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
have rw₃ : q' i * g i ^ n i * ∏ k ∈ s.erase i, g k ^ n k +
    ∑ i_1 : Fin (n i), r' i i_1 * g i ^ (↑i_1 : ℕ) * ∏ k ∈ s.erase i, g k ^ n k =
  q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
    ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
Tactic: rw [← Finset.mul_prod_erase s _ hi, hr i hi, add_mul, Finset.sum_mul, mul_assoc]
-- 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 : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : (i : ι) → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)
i : ι
hi : i ∈ s
rw :
  r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
rw₁ :
  (q' i * g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)) * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
rw₂ :
  q' i * g i ^ n i * ∏ k ∈ s.erase i, g k ^ n k +
      HMul.hMul (α := R[X]) (∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ)) (∏ k ∈ s.erase i, g k ^ n k) =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
rw₃ :
  q' i * g i ^ n i * ∏ k ∈ s.erase i, g k ^ n k +
      ∑ i_1 : Fin (n i), r' i i_1 * g i ^ (↑i_1 : ℕ) * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
      ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
⊢ r i * ∏ k ∈ s.erase i, g k ^ n k =
    q' i * ∏ i ∈ s, g i ^ n i + ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
have rw₄ : q' i * (g i ^ n i * ∏ k ∈ s.erase i, g k ^ n k) +
    ∑ i_1 : Fin (n i), r' i i_1 * g i ^ (↑i_1 : ℕ) * ∏ k ∈ s.erase i, g k ^ n k =
  q' i * (g i ^ n i * ∏ x ∈ s.erase i, g x ^ n x) +
    ∑ j : Fin (n i), r' i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
Tactic: rw [← Finset.mul_prod_erase s _ hi, hr i hi, add_mul, Finset.sum_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  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 =
    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
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  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 =
    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
h : Nontrivial R
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
have hf₁ : q₁ * ∏ i ∈ s, g i ^ n i +
    ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
  q₂ * ∏ i ∈ s, g i ^ n i +
    ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
Tactic: simp only [← Finset.sum_mul] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ degree.{u_1} (R := R) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ)) < (g i ^ n i).degree
have refine_1 : ⊥ < (g i ^ n i).degree
Tactic: refine (degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff ?_).2 fun j _ => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
refine_1 : ⊥ < (g i ^ n i).degree
⊢ degree.{u_1} (R := R) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ)) < (g i ^ n i).degree
have refine_2 : ∀ (j : Fin (n i)),
  Membership.mem (γ := Finset (Fin (n i))) Finset.univ j → (r i j * g i ^ (↑j : ℕ)).degree < (g i ^ n i).degree
Tactic: refine (degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff ?_).2 fun j _ => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ ⊥ < (g i ^ n i).degree
have refine_1 : g i ^ n 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 ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
h_1 : Membership.mem (γ := Finset (Fin (n i))) Finset.univ j
⊢ (r i j * g i ^ (↑j : ℕ)).degree < (g i ^ n i).degree
have refine_2 : (r i j).degree + (g i ^ (↑j : ℕ)).degree < (g i ^ n i).degree
Tactic: refine (degree_mul_le _ _).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 ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
h_1 : Membership.mem (γ := Finset (Fin (n i))) Finset.univ j
⊢ (r i j).degree + (g i ^ (↑j : ℕ)).degree < (g i ^ n i).degree
have refine_2 : (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) < (↑(n i * (g i).natDegree) : WithBot ℕ)
Tactic: rw [degree_eq_natDegree ((hg i hi).pow j.1).ne_zero, (hg i hi).natDegree_pow,
        degree_eq_natDegree ((hg i hi).pow (n i)).ne_zero, (hg i hi).natDegree_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
h_1 : Membership.mem (γ := Finset (Fin (n i))) Finset.univ j
| (↑(n i * (g i).natDegree) : WithBot ℕ)
have rw : (↑((n i - 1 + 1) * (g i).natDegree) : WithBot ℕ)
Tactic: rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.2 j.neZero.ne)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
h_1 : Membership.mem (γ := Finset (Fin (n i))) Finset.univ j
⊢ (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) < (↑(n i * (g i).natDegree) : WithBot ℕ)
have refine_2 : (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) < (↑((n i - 1 + 1) * (g i).natDegree) : WithBot ℕ)
Tactic: conv_rhs => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.2 j.neZero.ne)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
h_1 : Membership.mem (γ := Finset (Fin (n i))) Finset.univ j
⊢ (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) < (↑((n i - 1 + 1) * (g i).natDegree) : WithBot ℕ)
have refine_2 : (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) <
  (g i).degree + (↑((n i - 1) * (g i).natDegree) : WithBot ℕ)
Tactic: rw [Nat.add_one_mul, Nat.add_comm, Nat.cast_add, ← degree_eq_natDegree (hg i hi).ne_zero]