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
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
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 + 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
cons₁₄ : r j = r j * (b j * g j) + r j * (a j * g i)
cons₁₅ : r j = r j * (b j * g 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 * (a j * g i + b j * g j)
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
cons₁₄ : r j = r j * (b j * g j) + r j * (a j * g i)
cons₁₅ : r j = r j * (b j * g j + a j * g i)
cons₁₆ : r j = r j * (a j * g i + b j * g j)
⊢ 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 * 1
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
cons₁₄ : r j = r j * (b j * g j) + r j * (a j * g i)
cons₁₅ : r j = r j * (b j * g j + a j * g i)
cons₁₆ : r j = r j * (a j * g i + b j * g j)
cons₁₇ : r j = r j * 1
⊢ 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
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 ι
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)
⊢ ∃ (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
have empty : ∀ (hg : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (g i).Monic)
  (hgg : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
  ∃ (q : R[X]) (r : ι → R[X]),
    (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (r i).degree < (g i).degree) ∧
      f = q * ∏ i ∈ ∅, g i + ∑ i ∈ ∅, r i * ∏ k ∈ Finset.erase ∅ i, g k
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s hi ih =>
    rw [Finset.forall_mem_cons] at hg
    rw [Finset.coe_cons, Set.pairwise_insert] at hgg
    obtain ⟨q, r, -, hf⟩ := ih hg.2 hgg.1
    have hjs {j : ι} (hj : j ∈ s) : i ≠ j := fun hij => hi (hij ▸ hj)
    have hc (j : ι) : ∃ a b, j ∈ s → a * g i + b * g j = 1 :=
      if h : j ∈ s ∧ i ≠ j then
        (hgg.2 j h.1 h.2).1.elim fun a h => h.elim fun b h => ⟨a, b, fun _ => h⟩
      else
        ⟨0, 0, fun hj => (h ⟨hj, hjs hj⟩).elim⟩
    choose a b hab using hc
    refine ⟨(q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j),
      Function.update (fun j => r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i),
      ?_, hf.trans ?_⟩
    · rw [Finset.forall_mem_cons, Function.update_self]
      refine ⟨degree_modByMonic_lt _ hg.1, fun j hj => ?_⟩
      rw [Function.update_of_ne (hjs hj).symm]
      exact degree_modByMonic_lt _ (hg.2 j hj)
    · rw [Finset.prod_cons, Finset.sum_cons, Function.update_self, Finset.erase_cons, add_mul,
        add_add_add_comm, ← mul_assoc, ← add_mul, add_comm (_ * g i), ← mul_comm (g i),
        modByMonic_add_div, add_mul, add_assoc, add_right_inj, Finset.sum_mul,
        Finset.sum_mul, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
      refine Finset.sum_congr rfl fun j hj => ?_
      rw [Function.update_of_ne (hjs hj).symm, Finset.erase_cons_of_ne _ (hjs hj),
        Finset.prod_cons, ← Finset.mul_prod_erase s g hj]
      simp_rw [← mul_assoc, ← add_mul]
      refine congrArg (· * _) ?_
      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]
Cleared hypotheses: s, hg, hgg
-- 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 : ∀ i_1 ∈ Finset.cons i s hi, (g i_1).Monic
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
hr₁ : ∀ i_1 ∈ Finset.cons i s hi, (r₁ i_1).degree < (g i_1).degree
hr₂ : ∀ i_1 ∈ Finset.cons i s hi, (r₂ i_1).degree < (g i_1).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
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hg₁ : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
Tactic: rw [Finset.forall_mem_cons] at hg hr₁ hr₂
Cleared hypotheses: hg, hgg, hr₁, hr₂, 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 : ∀ i_1 ∈ Finset.cons i s hi, (g i_1).Monic
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
hr₁ : ∀ i_1 ∈ Finset.cons i s hi, (r₁ i_1).degree < (g i_1).degree
hr₂ : ∀ i_1 ∈ Finset.cons i s hi, (r₂ i_1).degree < (g i_1).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
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)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hr₃ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
Tactic: rw [Finset.forall_mem_cons] at hg hr₁ hr₂
Cleared hypotheses: hg, hgg, hr₁, hr₂, 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 : ∀ i_1 ∈ Finset.cons i s hi, (g i_1).Monic
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
hr₁ : ∀ i_1 ∈ Finset.cons i s hi, (r₁ i_1).degree < (g i_1).degree
hr₂ : ∀ i_1 ∈ Finset.cons i s hi, (r₂ i_1).degree < (g i_1).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
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
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have hr₄ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
Tactic: rw [Finset.forall_mem_cons] at hg hr₁ hr₂
Cleared hypotheses: hg, hgg, hr₁, hr₂, 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 ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (∏ i ∈ Finset.cons j s hj, g i)
have cons : IsCoprime (g i) (g j) ∧ IsCoprime (g i) (∏ x ∈ s, g x)
Tactic: rw [Finset.prod_cons, IsCoprime.mul_right_iff]
-- 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]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (g j) ∧ IsCoprime (g i) (∏ x ∈ s, g x)
have cons : i ∉ s
Tactic: refine ⟨hgg (by simp) (by simp) fun hij => hi (by simp [hij]), ih ?_ ?_⟩
-- 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]
i j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
cons : i ∉ s
⊢ IsCoprime (g i) (g j) ∧ IsCoprime (g i) (∏ x ∈ s, g x)
have cons₁ : (↑(Finset.cons i s sorry) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
Tactic: refine ⟨hgg (by simp) (by simp) fun hij => hi (by simp [hij]), ih ?_ ?_⟩
-- 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]
i : ι
s : Finset ι
hi : i ∉ s
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (∏ i ∈ s, g i)
have empty : ∀ (hi : i ∉ ∅) (hgg : (↑(Finset.cons i ∅ hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
  IsCoprime (g i) (∏ i ∈ ∅, g i)
Tactic: induction s using Finset.cons_induction with
      | empty => simp [isCoprime_one_right]
      | cons j s hj ih =>
        rw [Finset.prod_cons, IsCoprime.mul_right_iff]
        refine ⟨hgg (by simp) (by simp) fun hij => hi (by simp [hij]), ih ?_ ?_⟩
        · exact mt Finset.mem_cons_of_mem hi
        · exact hgg.mono (SetLike.coe_mono (Finset.cons_subset_cons.2 (Finset.subset_cons hj)))
Cleared hypotheses: s, hi, hgg
-- 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]
i : ι
s : Finset ι
hi : i ∉ s
hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
empty :
  ∀ (hi : i ∉ ∅) (hgg : (↑(Finset.cons i ∅ hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
    IsCoprime (g i) (∏ i ∈ ∅, g i)
⊢ IsCoprime (g i) (∏ i ∈ s, g i)
have cons : ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
  (ih :
    ∀ (hi : i ∉ s) (hgg : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
      IsCoprime (g i) (∏ i ∈ s, g i))
  (hi : i ∉ Finset.cons j s hj)
  (hgg : (↑(Finset.cons i (Finset.cons j s hj) hi) : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)),
  IsCoprime (g i) (∏ i ∈ Finset.cons j s hj, g i)
Tactic: induction s using Finset.cons_induction with
      | empty => simp [isCoprime_one_right]
      | cons j s hj ih =>
        rw [Finset.prod_cons, IsCoprime.mul_right_iff]
        refine ⟨hgg (by simp) (by simp) fun hij => hi (by simp [hij]), ih ?_ ?_⟩
        · exact mt Finset.mem_cons_of_mem hi
        · exact hgg.mono (SetLike.coe_mono (Finset.cons_subset_cons.2 (Finset.subset_cons hj)))
Cleared hypotheses: s, hi, hgg
-- 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
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
have cop : IsCoprime (g i) (∏ i ∈ s, g i)
Tactic: have cop : IsCoprime (g i) (∏ i ∈ s, g i) := by
      clear *-hgg
      induction s using Finset.cons_induction with
      | empty => simp [isCoprime_one_right]
      | cons j s hj ih =>
        rw [Finset.prod_cons, IsCoprime.mul_right_iff]
        refine ⟨hgg (by simp) (by simp) fun hij => hi (by simp [hij]), ih ?_ ?_⟩
        · exact mt Finset.mem_cons_of_mem hi
        · exact hgg.mono (SetLike.coe_mono (Finset.cons_subset_cons.2 (Finset.subset_cons hj)))