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
obtain :
  ∀ (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),
    ∃ (q : R[X]) (r : (i : ι) → Fin (n i) → R[X]),
      (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
        HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K) (∏ i ∈ s, gi i ^ n i : 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]),
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K) (∏ i ∈ s, gi i ^ n i : 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)

Tactic:
obtain ⟨q, r, hr, hf⟩ := eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow f hg hgg n

Premises used: Polynomial.eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow
-- 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
⊢ ∃ (q : R[X]) (r : (i : ι) → Fin (n i) → R[X]),
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K) (∏ i ∈ s, gi i ^ n i : 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)

Tactic:
⟨q, fun i j => r i j.rev, fun i hi j => hr i hi j.rev, ?_⟩

Premises used: Fin.rev, And.intro, Exists.intro
-- 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
refine :
  HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K) (∏ i ∈ s, gi i ^ n i : 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) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
              (gi i ^ ((↑j : ℕ) + 1)) :
        K)
⊢ ∃ (q : R[X]) (r : (i : ι) → Fin (n i) → R[X]),
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K) (∏ i ∈ s, gi i ^ n i : 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)

Tactic:
refine ⟨q, fun i j => r i j.rev, fun i hi j => 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 : 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
rw :
  HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
        (∏ x ∈ s, HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x ^ n x) : K) (gi x ^ n x) : K) +
      HMul.hMul (α := K) (β := K)
        ((algebraMap R[X] K : (a : R[X]) → K)
            (∑ i ∈ s, ∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k) :
          K)
        (∏ i ∈ s, gi i ^ n i : 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) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
              (gi i ^ ((↑j : ℕ) + 1)) :
        K)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K) (∏ i ∈ s, gi i ^ n i : 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) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
              (gi i ^ ((↑j : ℕ) + 1)) :
        K)

Tactic:
rw [hf, map_add, map_mul, map_prod, add_mul, mul_assoc, ← Finset.prod_mul_distrib]

Premises used: add_mul, Finset.prod_mul_distrib, mul_assoc, map_add, map_prod, map_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 : 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
x : ι
hx : x ∈ s
rw : HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x) * gi x ^ n x = 1
rw₁ : HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (gi x) ^ n x = 1
rw₂ : HMul.hMul (β := K) (gi x) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) ^ n x = 1
rw₃ : HPow.hPow (α := K) 1 (n x) = 1
rw₄ rw₅ : Eq.{u_2 + 1} (α := K) 1 1
⊢ HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x ^ n x) : K) (gi x ^ n x) = 1

Tactic:
rw [map_pow, ← mul_pow, mul_comm, hgi x hx, one_pow]

Premises used: one_pow, map_pow, mul_comm, mul_pow
-- 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
⊢ ∀ (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

Tactic:
have hc (x : ι) (hx : x ∈ s) : (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1 := by
    rw [map_pow, ← mul_pow, mul_comm, hgi x hx, one_pow]
-- 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
rw :
  Eq.{u_2 + 1} (α := K)
    (∑ i ∈ s,
      HMul.hMul (α := K) (β := K)
        ((algebraMap R[X] K : (a : R[X]) → K) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k) :
          K)
        (∏ i ∈ s, gi i ^ n i : K))
    (∑ i ∈ s,
      ∑ j : Fin (n i),
        HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
          (gi i ^ ((↑j : ℕ) + 1)))
⊢ HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
        (∏ x ∈ s, HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x ^ n x) : K) (gi x ^ n x) : K) +
      HMul.hMul (α := K) (β := K)
        ((algebraMap R[X] K : (a : R[X]) → K)
            (∑ i ∈ s, ∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k) :
          K)
        (∏ i ∈ s, gi i ^ n i : 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) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
              (gi i ^ ((↑j : ℕ) + 1)) :
        K)

Tactic:
rw [Finset.prod_congr rfl hc, Finset.prod_const_one,
    mul_one, add_right_inj, map_sum, Finset.sum_mul]

Premises used: Finset.prod_congr, map_sum, Finset.prod_const_one, mul_one, add_right_inj, rfl, 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 : 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
⊢ Eq.{u_2 + 1} (α := K)
    (∑ i ∈ s,
      HMul.hMul (α := K) (β := K)
        ((algebraMap R[X] K : (a : R[X]) → K) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k) :
          K)
        (∏ i ∈ s, gi i ^ n i : K))
    (∑ i ∈ s,
      ∑ j : Fin (n i),
        HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
          (gi i ^ ((↑j : ℕ) + 1)))

Tactic:
Finset.sum_congr rfl fun i hi => ?_

Premises used: 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 : 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
refine :
  ∀ (i : ι) (hi : i ∈ s),
    HMul.hMul (α := K) (β := K)
        ((algebraMap R[X] K : (a : R[X]) → K) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k) :
          K)
        (∏ i ∈ s, gi i ^ n i : K) =
      ∑ j : Fin (n i),
        HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
          (gi i ^ ((↑j : ℕ) + 1))
⊢ Eq.{u_2 + 1} (α := K)
    (∑ i ∈ s,
      HMul.hMul (α := K) (β := K)
        ((algebraMap R[X] K : (a : R[X]) → K) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k) :
          K)
        (∏ i ∈ s, gi i ^ n i : K))
    (∑ i ∈ s,
      ∑ j : Fin (n i),
        HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
          (gi i ^ ((↑j : ℕ) + 1)))

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Premises used: 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 : 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
rw :
  Eq.{u_2 + 1} (α := K)
    (∑ i_1 : Fin (n i),
      HMul.hMul (α := K) (β := K)
        ((algebraMap R[X] K : (a : R[X]) → K)
            (r i ((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) i_1) *
                g i ^ (↑((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) i_1) : ℕ) *
              ∏ k ∈ s.erase i, g k ^ n k) :
          K)
        (∏ i ∈ s, gi i ^ n i : K))
    (∑ j : Fin (n i),
      HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
        (gi i ^ ((↑j : ℕ) + 1)))
⊢ HMul.hMul (α := K) (β := K)
      ((algebraMap R[X] K : (a : R[X]) → K) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ) * ∏ k ∈ s.erase i, g k ^ n k) : K)
      (∏ i ∈ s, gi i ^ n i : K) =
    ∑ j : Fin (n i),
      HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
        (gi i ^ ((↑j : ℕ) + 1))

Tactic:
rw [map_sum, Finset.sum_mul, ← Equiv.sum_comp Fin.revPerm]

Premises used: Equiv.sum_comp, map_sum, Fin.revPerm, 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 : 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
⊢ Eq.{u_2 + 1} (α := K)
    (∑ i_1 : Fin (n i),
      HMul.hMul (α := K) (β := K)
        ((algebraMap R[X] K : (a : R[X]) → K)
            (r i ((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) i_1) *
                g i ^ (↑((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) i_1) : ℕ) *
              ∏ k ∈ s.erase i, g k ^ n k) :
          K)
        (∏ i ∈ s, gi i ^ n i : K))
    (∑ j : Fin (n i),
      HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
        (gi i ^ ((↑j : ℕ) + 1)))

Tactic:
Fintype.sum_congr _ _ fun j => ?_

Premises used: Fintype.sum_congr
-- 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
refine :
  ∀ (j : Fin (n i)),
    HMul.hMul (α := K) (β := K)
        ((algebraMap R[X] K : (a : R[X]) → K)
            (r i ((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) j) *
                g i ^ (↑((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) j) : ℕ) *
              ∏ k ∈ s.erase i, g k ^ n k) :
          K)
        (∏ i ∈ s, gi i ^ n i : K) =
      HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
        (gi i ^ ((↑j : ℕ) + 1))
⊢ Eq.{u_2 + 1} (α := K)
    (∑ i_1 : Fin (n i),
      HMul.hMul (α := K) (β := K)
        ((algebraMap R[X] K : (a : R[X]) → K)
            (r i ((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) i_1) *
                g i ^ (↑((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) i_1) : ℕ) *
              ∏ k ∈ s.erase i, g k ^ n k) :
          K)
        (∏ i ∈ s, gi i ^ n i : K))
    (∑ j : Fin (n i),
      HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
        (gi i ^ ((↑j : ℕ) + 1)))

Tactic:
refine Fintype.sum_congr _ _ fun j => ?_

Premises used: Fintype.sum_congr
-- 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)
rw :
  HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j.rev) : K)
      (gi i ^ n i * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j.rev : ℕ)) =
    HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
      (gi i ^ ((↑j : ℕ) + 1))
⊢ HMul.hMul (α := K) (β := K)
      ((algebraMap R[X] K : (a : R[X]) → K)
          (r i ((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) j) *
              g i ^ (↑((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) j) : ℕ) *
            ∏ k ∈ s.erase i, g k ^ n k) :
        K)
      (∏ i ∈ s, gi i ^ n i : K) =
    HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
      (gi i ^ ((↑j : ℕ) + 1))

Tactic:
rw [Fin.revPerm_apply, map_mul, map_prod, ← Finset.prod_erase_mul s _ hi,
    ← mul_rotate', mul_assoc, ← Finset.prod_mul_distrib,
    Finset.prod_congr rfl fun x hx => hc x (Finset.mem_of_mem_erase hx),
    Finset.prod_const_one, mul_one, map_mul, map_pow, mul_left_comm]

Premises used: Finset.prod_erase_mul, Finset.prod_mul_distrib, mul_assoc, Finset.prod_congr, map_pow, mul_left_comm, map_prod, Finset.prod_const_one, Fin.revPerm_apply, map_mul, mul_rotate', Finset.mem_of_mem_erase, mul_one, 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 : 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)
⊢ HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j.rev) : K)
      (gi i ^ n i * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j.rev : ℕ)) =
    HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
      (gi i ^ ((↑j : ℕ) + 1))

Tactic:
congrArg (_ * ·) ?_

Premises used: HMul.hMul, congrArg
-- 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)
refine :
  gi i ^ n i * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j.rev : ℕ) = gi i ^ ((↑j : ℕ) + 1)
⊢ HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j.rev) : K)
      (gi i ^ n i * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j.rev : ℕ)) =
    HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) ((fun (i : ι) (j : Fin (n i)) ↦ r i j.rev) i j) : K)
      (gi i ^ ((↑j : ℕ) + 1))

Tactic:
refine congrArg (_ * ·) ?_

Premises used: HMul.hMul, congrArg