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 ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
cons : r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i * g i + r j * a j /ₘ g j * g i) * g j + r j * a j %ₘ g j * g i)
cons₁ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₂ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j) + r j * a j %ₘ g j * g i
cons₃ :
  r j = r j * b j %ₘ g i * g j + r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₄ : r j = (r j * b j %ₘ g i + r j * b j /ₘ g i * g i) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₅ :
  r j = (r j * b j %ₘ g i + g i * (r j * b j /ₘ g i)) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
⊢ r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)
have cons₆ : r j = r j * b j * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
Tactic: rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]
-- 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 ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
cons : r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i * g i + r j * a j /ₘ g j * g i) * g j + r j * a j %ₘ g j * g i)
cons₁ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₂ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j) + r j * a j %ₘ g j * g i
cons₃ :
  r j = r j * b j %ₘ g i * g j + r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₄ : r j = (r j * b j %ₘ g i + r j * b j /ₘ g i * g i) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₅ :
  r j = (r j * b j %ₘ g i + g i * (r j * b j /ₘ g i)) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₆ : r j = r j * b j * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
⊢ r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)
have cons₇ : r j = r j * b j * g j + (r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
Tactic: rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]
-- 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 ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
cons : r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i * g i + r j * a j /ₘ g j * g i) * g j + r j * a j %ₘ g j * g i)
cons₁ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₂ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j) + r j * a j %ₘ g j * g i
cons₃ :
  r j = r j * b j %ₘ g i * g j + r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₄ : r j = (r j * b j %ₘ g i + r j * b j /ₘ g i * g i) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₅ :
  r j = (r j * b j %ₘ g i + g i * (r j * b j /ₘ g i)) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₆ : r j = r j * b j * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₇ : r j = r j * b j * g j + (r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
⊢ r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)
have cons₈ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j * g i + r j * a j %ₘ g j * g i)
Tactic: rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]
-- 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 ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
cons : r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i * g i + r j * a j /ₘ g j * g i) * g j + r j * a j %ₘ g j * g i)
cons₁ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₂ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j) + r j * a j %ₘ g j * g i
cons₃ :
  r j = r j * b j %ₘ g i * g j + r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₄ : r j = (r j * b j %ₘ g i + r j * b j /ₘ g i * g i) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₅ :
  r j = (r j * b j %ₘ g i + g i * (r j * b j /ₘ g i)) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₆ : r j = r j * b j * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₇ : r j = r j * b j * g j + (r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₈ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j * g i + r j * a j %ₘ g j * g i)
⊢ r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)
have cons₉ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j + r j * a j %ₘ g j) * g i
Tactic: rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]
-- 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 ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
cons : r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i * g i + r j * a j /ₘ g j * g i) * g j + r j * a j %ₘ g j * g i)
cons₁ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₂ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j) + r j * a j %ₘ g j * g i
cons₃ :
  r j = r j * b j %ₘ g i * g j + r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₄ : r j = (r j * b j %ₘ g i + r j * b j /ₘ g i * g i) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₅ :
  r j = (r j * b j %ₘ g i + g i * (r j * b j /ₘ g i)) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₆ : r j = r j * b j * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₇ : r j = r j * b j * g j + (r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₈ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j * g i + r j * a j %ₘ g j * g i)
cons₉ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j + r j * a j %ₘ g j) * g i
⊢ r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)
have cons₁₀ : r j = r j * b j * g j + (r j * a j %ₘ g j + r j * a j /ₘ g j * g j) * g i
Tactic: rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]
-- 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 ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
cons : r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i * g i + r j * a j /ₘ g j * g i) * g j + r j * a j %ₘ g j * g i)
cons₁ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₂ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j) + r j * a j %ₘ g j * g i
cons₃ :
  r j = r j * b j %ₘ g i * g j + r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₄ : r j = (r j * b j %ₘ g i + r j * b j /ₘ g i * g i) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₅ :
  r j = (r j * b j %ₘ g i + g i * (r j * b j /ₘ g i)) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₆ : r j = r j * b j * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₇ : r j = r j * b j * g j + (r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₈ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j * g i + r j * a j %ₘ g j * g i)
cons₉ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j + r j * a j %ₘ g j) * g i
cons₁₀ : r j = r j * b j * g j + (r j * a j %ₘ g j + r j * a j /ₘ g j * g j) * g i
⊢ r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)
have cons₁₁ : r j = r j * b j * g j + (r j * a j %ₘ g j + g j * (r j * a j /ₘ g j)) * g i
Tactic: rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]
-- 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 ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
cons : r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i * g i + r j * a j /ₘ g j * g i) * g j + r j * a j %ₘ g j * g i)
cons₁ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₂ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j) + r j * a j %ₘ g j * g i
cons₃ :
  r j = r j * b j %ₘ g i * g j + r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₄ : r j = (r j * b j %ₘ g i + r j * b j /ₘ g i * g i) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₅ :
  r j = (r j * b j %ₘ g i + g i * (r j * b j /ₘ g i)) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₆ : r j = r j * b j * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₇ : r j = r j * b j * g j + (r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₈ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j * g i + r j * a j %ₘ g j * g i)
cons₉ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j + r j * a j %ₘ g j) * g i
cons₁₀ : r j = r j * b j * g j + (r j * a j %ₘ g j + r j * a j /ₘ g j * g j) * g i
cons₁₁ : r j = r j * b j * g j + (r j * a j %ₘ g j + g j * (r j * a j /ₘ g j)) * g i
⊢ r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)
have cons₁₂ : r j = r j * b j * g j + r j * a j * g i
Tactic: rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]
-- 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 ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
cons : r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i * g i + r j * a j /ₘ g j * g i) * g j + r j * a j %ₘ g j * g i)
cons₁ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₂ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j) + r j * a j %ₘ g j * g i
cons₃ :
  r j = r j * b j %ₘ g i * g j + r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₄ : r j = (r j * b j %ₘ g i + r j * b j /ₘ g i * g i) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₅ :
  r j = (r j * b j %ₘ g i + g i * (r j * b j /ₘ g i)) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₆ : r j = r j * b j * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₇ : r j = r j * b j * g j + (r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₈ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j * g i + r j * a j %ₘ g j * g i)
cons₉ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j + r j * a j %ₘ g j) * g i
cons₁₀ : r j = r j * b j * g j + (r j * a j %ₘ g j + r j * a j /ₘ g j * g j) * g i
cons₁₁ : r j = r j * b j * g j + (r j * a j %ₘ g j + g j * (r j * a j /ₘ g j)) * g i
cons₁₂ : r j = r j * b j * g j + r j * a j * g i
⊢ r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)
have cons₁₃ : r j = r j * (b j * g j) + r j * a j * g i
Tactic: rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]
-- 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 ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg :
  ((↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)) ∧
    ∀ b ∈ (↑s : Set ι), i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι} (hj : j ∈ s), i ≠ j
a b : (j : ι) → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
cons : r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i * g i + r j * a j /ₘ g j * g i) * g j + r j * a j %ₘ g j * g i)
cons₁ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₂ :
  r j = r j * b j %ₘ g i * g j + (r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j) + r j * a j %ₘ g j * g i
cons₃ :
  r j = r j * b j %ₘ g i * g j + r j * b j /ₘ g i * g i * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₄ : r j = (r j * b j %ₘ g i + r j * b j /ₘ g i * g i) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₅ :
  r j = (r j * b j %ₘ g i + g i * (r j * b j /ₘ g i)) * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₆ : r j = r j * b j * g j + r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i
cons₇ : r j = r j * b j * g j + (r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)
cons₈ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j * g i + r j * a j %ₘ g j * g i)
cons₉ : r j = r j * b j * g j + (r j * a j /ₘ g j * g j + r j * a j %ₘ g j) * g i
cons₁₀ : r j = r j * b j * g j + (r j * a j %ₘ g j + r j * a j /ₘ g j * g j) * g i
cons₁₁ : r j = r j * b j * g j + (r j * a j %ₘ g j + g j * (r j * a j /ₘ g j)) * g i
cons₁₂ : r j = r j * b j * g j + r j * a j * g i
cons₁₃ : r j = r j * (b j * g j) + r j * a j * g i
⊢ r j = r j * b j %ₘ g i * g j + ((r j * b j /ₘ g i + r j * a j /ₘ g j) * g i * g j + r j * a j %ₘ g j * g i)
have cons₁₄ : r j = r j * (b j * g j) + r j * (a j * g i)
Tactic: rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]