awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : CommRing K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : Nontrivial R
ι : Type u_3
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 : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : 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
hc : ∀ (x : ι) (hx : x ∈ s), HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x ^ n x) : K) (gi x ^ n x) = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ (↑j : ℕ) + 1 ≤ n i

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : CommRing K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) = 1
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 :
  HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₁ : K)
      (∑ i ∈ s,
          ∑ j : Fin (n i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₁ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
        K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₂ : K)
      (∑ i ∈ s,
          ∑ j : Fin (n i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₂ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
        K)
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
          (∑ i ∈ s,
              ∑ j : Fin (n i),
                HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
            K) *
        ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
      (algebraMap R[X] K : (a : R[X]) → K)
        (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k)
⊢ HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₁ : K)
        (∑ i ∈ s,
            ∑ j : Fin (n i),
              HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₁ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
          K) *
      ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₂ : K)
        (∑ i ∈ s,
            ∑ j : Fin (n i),
              HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₂ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
          K) *
      ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i)

Tactic:
apply_fun (· * ∏ i ∈ s, algebraMap R[X] K (g i) ^ n i) at hf

Premises used: HMul.hMul, Algebra.algebraMap, Polynomial, Finset.prod, HPow.hPow, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : CommRing K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) = 1
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
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
          (∑ i ∈ s,
              ∑ j : Fin (n i),
                HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
            K) *
        ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
      (algebraMap R[X] K : (a : R[X]) → K)
        (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k)
hf :
  HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₁ : K)
        (∑ i ∈ s,
            ∑ j : Fin (n i),
              HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₁ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
          K) *
      ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₂ : K)
        (∑ i ∈ s,
            ∑ j : Fin (n i),
              HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₂ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
          K) *
      ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i)
⊢ q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r₁ i j.rev * 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.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
rw [hff, hff, (FaithfulSMul.algebraMap_injective R[X] K).eq_iff] at hf

Premises used: Function.Injective.eq_iff, Polynomial, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : CommRing K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) = 1
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
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
          (∑ i ∈ s,
              ∑ j : Fin (n i),
                HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
            K) *
        ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
      (algebraMap R[X] K : (a : R[X]) → K)
        (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k)
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r₁ i j.rev * 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.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
⊢ q₁ = q₂

Tactic:
obtain ⟨hq, hr⟩ := quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique hg hgg
      (fun i hi j => hr₁ i hi j.rev) (fun i hi j => hr₂ i hi j.rev) hf

Premises used: Fin.rev, Polynomial.quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : CommRing K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) = 1
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
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
          (∑ i ∈ s,
              ∑ j : Fin (n i),
                HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
            K) *
        ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
      (algebraMap R[X] K : (a : R[X]) → K)
        (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k)
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r₁ i j.rev * 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.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
hq : q₁ = q₂
⊢ ∀ i ∈ s, Eq.{u_1 + 1} (α := Fin (n i) → R[X]) (fun (j : Fin (n i)) ↦ r₁ i j.rev) fun (j : Fin (n i)) ↦ r₂ i j.rev

Tactic:
obtain ⟨hq, hr⟩ := quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique hg hgg
      (fun i hi j => hr₁ i hi j.rev) (fun i hi j => hr₂ i hi j.rev) hf

Premises used: Fin.rev, Polynomial.quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : CommRing K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) = 1
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
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
          (∑ i ∈ s,
              ∑ j : Fin (n i),
                HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
            K) *
        ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
      (algebraMap R[X] K : (a : R[X]) → K)
        (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k)
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r₁ i j.rev * 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.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
hq : q₁ = q₂
hr : ∀ i ∈ s, Eq.{u_1 + 1} (α := Fin (n i) → R[X]) (fun (j : Fin (n i)) ↦ r₁ i j.rev) fun (j : Fin (n i)) ↦ r₂ i j.rev
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
⟨hq, fun i hi => funext fun j => j.rev_rev ▸ congrFun (hr i hi) j.rev⟩

Premises used: Eq.rec, funext, Fin.rev, congrFun, And.intro, Fin.rev_rev
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : CommRing K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) = 1
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
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
          (∑ i ∈ s,
              ∑ j : Fin (n i),
                HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
            K) *
        ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
      (algebraMap R[X] K : (a : R[X]) → K)
        (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k)
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r₁ i j.rev * 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.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k
hq : q₁ = q₂
hr : ∀ i ∈ s, Eq.{u_1 + 1} (α := Fin (n i) → R[X]) (fun (j : Fin (n i)) ↦ r₁ i j.rev) fun (j : Fin (n i)) ↦ r₂ i j.rev
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
exact ⟨hq, fun i hi => funext fun j => j.rev_rev ▸ congrFun (hr i hi) j.rev⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : CommRing K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) = 1
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 :
  HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₁ : K)
      (∑ i ∈ s,
          ∑ j : Fin (n i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₁ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
        K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₂ : K)
      (∑ i ∈ s,
          ∑ j : Fin (n i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₂ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
        K)
suffices :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
          (∑ i ∈ s,
              ∑ j : Fin (n i),
                HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
            K) *
        ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
      (algebraMap R[X] K : (a : R[X]) → K)
        (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k)
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
suffices hff : ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
      (algebraMap R[X] K q + ∑ i ∈ s, ∑ j,
        algebraMap R[X] K (r i j) * gi i ^ (j.1 + 1)) * ∏ i ∈ s, algebraMap R[X] K (g i) ^ n i =
      algebraMap R[X] K (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s,
        ∑ j : Fin (n i), r i j.rev * g i ^ j.1 * ∏ k ∈ s.erase i, g k ^ n k) by
    apply_fun (· * ∏ i ∈ s, algebraMap R[X] K (g i) ^ n i) at hf
    rw [hff, hff, (FaithfulSMul.algebraMap_injective R[X] K).eq_iff] at hf
    obtain ⟨hq, hr⟩ := quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique hg hgg
      (fun i hi j => hr₁ i hi j.rev) (fun i hi j => hr₂ i hi j.rev) hf
    exact ⟨hq, fun i hi => funext fun j => j.rev_rev ▸ congrFun (hr i hi) j.rev⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : CommRing K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) = 1
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 :
  HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₁ : K)
      (∑ i ∈ s,
          ∑ j : Fin (n i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₁ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
        K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₂ : K)
      (∑ i ∈ s,
          ∑ j : Fin (n i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₂ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
        K)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
simp_rw :
  HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
        (∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) : K) +
      ∑ x ∈ s,
        ∑ i : Fin (n x),
          HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r x i) : K) (gi x ^ ((↑i : ℕ) + 1)) *
            ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
        (∏ x ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x) : K) +
      ∑ x ∈ s,
        ∑ x_1 : Fin (n x),
          HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r x x_1.rev) : K)
              (HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (↑x_1 : ℕ)) *
            ∏ x ∈ s.erase x, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x)
⊢ HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
        (∑ i ∈ s,
            ∑ j : Fin (n i),
              HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
          K) *
      ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    (algebraMap R[X] K : (a : R[X]) → K)
      (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j : Fin (n i), r i j.rev * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k)

Tactic:
simp_rw [add_mul, Finset.sum_mul, map_add, map_sum, map_mul, map_prod, map_pow]

Premises used: add_mul, map_add, map_pow, map_sum, map_prod, map_mul, Finset.sum_mul
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : CommRing K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) = 1
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 :
  HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₁ : K)
      (∑ i ∈ s,
          ∑ j : Fin (n i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₁ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
        K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₂ : K)
      (∑ i ∈ s,
          ∑ j : Fin (n i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₂ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
        K)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
⊢ HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
        (∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) : K) +
      ∑ x ∈ s,
        ∑ i : Fin (n x),
          HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r x i) : K) (gi x ^ ((↑i : ℕ) + 1)) *
            ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
        (∏ x ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x) : K) +
      ∑ x ∈ s,
        ∑ x_1 : Fin (n x),
          HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r x x_1.rev) : K)
              (HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (↑x_1 : ℕ)) *
            ∏ x ∈ s.erase x, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x)

Tactic:
congrArg (_ + ·) (Finset.sum_congr rfl fun i hi => ?_)

Premises used: congrArg, HAdd.hAdd, Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : CommRing K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) = 1
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 :
  HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₁ : K)
      (∑ i ∈ s,
          ∑ j : Fin (n i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₁ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
        K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₂ : K)
      (∑ i ∈ s,
          ∑ j : Fin (n i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₂ i j) : K) (gi i ^ ((↑j : ℕ) + 1)) :
        K)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
refine :
  ∀ (i : ι) (hi : i ∈ s),
    Eq.{u_2 + 1} (α := K)
      (∑ i_1 : Fin (n i),
        HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i i_1) : K) (gi i ^ ((↑i_1 : ℕ) + 1)) *
          ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i))
      (∑ x : Fin (n i),
        HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i x.rev) : K)
            (HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑x : ℕ)) *
          ∏ x ∈ s.erase i, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x))
⊢ HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
        (∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) : K) +
      ∑ x ∈ s,
        ∑ i : Fin (n x),
          HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r x i) : K) (gi x ^ ((↑i : ℕ) + 1)) *
            ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
        (∏ x ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x) : K) +
      ∑ x ∈ s,
        ∑ x_1 : Fin (n x),
          HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r x x_1.rev) : K)
              (HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (↑x_1 : ℕ)) *
            ∏ x ∈ s.erase x, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x)

Tactic:
refine congrArg (_ + ·) (Finset.sum_congr rfl fun i hi => ?_)

Premises used: congrArg, HAdd.hAdd, Finset.sum_congr, rfl