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
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)
have 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))
Tactic: refine congrArg (_ + ·) (Finset.sum_congr rfl fun i hi => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
Goal:
R : Type u_1
inst : CommRing R
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]
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))
have refine : ∀ (j : Fin (n i)),
  HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i ((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) j)) : K)
        (gi i ^ ((↑((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) j) : ℕ) + 1)) *
      ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j.rev) : K)
        (HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)) *
      ∏ x ∈ s.erase i, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x)
Tactic: refine (Equiv.sum_comp Fin.revPerm _).symm.trans (Fintype.sum_congr _ _ fun j => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i ((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) j)) : K)
        (gi i ^ ((↑((Fin.revPerm : (a : Fin (n i)) → Fin (n i)) j) : ℕ) + 1)) *
      ∏ i ∈ s, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j.rev) : K)
        (HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)) *
      ∏ x ∈ s.erase i, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x)
have rw : HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j.rev) : K)
      (gi i ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i)) *
    ∏ x ∈ s.erase i, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x) =
  HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j.rev) : K)
      (HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)) *
    ∏ x ∈ s.erase i, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x)
Tactic: rw [Fin.revPerm_apply, ← Finset.mul_prod_erase s _ hi, ← mul_assoc,
    mul_assoc (algebraMap R[X] K (r i j.rev))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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]
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 ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i)) *
      ∏ x ∈ s.erase i, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x) =
    HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j.rev) : K)
        (HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)) *
      ∏ x ∈ s.erase i, HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x)
have refine : gi i ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
  HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
Tactic: refine congrArg (algebraMap R[X] K (r i j.rev) * · * _) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
have rw : gi i ^ ((↑j.rev : ℕ) + 1) * 1 * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
  HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
Tactic: rw [← mul_one (gi i ^ (j.rev.1 + 1)), ← @one_pow K _ j, ← hgi i hi,
    mul_pow, ← mul_assoc, ← pow_add, Fin.val_rev, Nat.add_right_comm, Nat.add_assoc,
    Nat.sub_add_cancel (by lia), mul_right_comm, ← mul_pow, hgi i hi, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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]
i : ι
hi : i ∈ s
j : Fin (n i)
rw :
  gi i ^ ((↑j.rev : ℕ) + 1) * 1 * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
⊢ gi i ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
have rw₁ : gi i ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) 1 (↑j : ℕ) *
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
  HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
Tactic: rw [← mul_one (gi i ^ (j.rev.1 + 1)), ← @one_pow K _ j, ← hgi i hi,
    mul_pow, ← mul_assoc, ← pow_add, Fin.val_rev, Nat.add_right_comm, Nat.add_assoc,
    Nat.sub_add_cancel (by lia), mul_right_comm, ← mul_pow, hgi i hi, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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]
i : ι
hi : i ∈ s
j : Fin (n i)
rw :
  gi i ^ ((↑j.rev : ℕ) + 1) * 1 * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
rw₁ :
  gi i ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) 1 (↑j : ℕ) *
      HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
⊢ gi i ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
have rw₂ : gi i ^ ((↑j.rev : ℕ) + 1) * HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) ^ (↑j : ℕ) *
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
  HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
Tactic: rw [← mul_one (gi i ^ (j.rev.1 + 1)), ← @one_pow K _ j, ← hgi i hi,
    mul_pow, ← mul_assoc, ← pow_add, Fin.val_rev, Nat.add_right_comm, Nat.add_assoc,
    Nat.sub_add_cancel (by lia), mul_right_comm, ← mul_pow, hgi i hi, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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]
i : ι
hi : i ∈ s
j : Fin (n i)
rw :
  gi i ^ ((↑j.rev : ℕ) + 1) * 1 * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
rw₁ :
  gi i ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) 1 (↑j : ℕ) *
      HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
rw₂ :
  gi i ^ ((↑j.rev : ℕ) + 1) * HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) ^ (↑j : ℕ) *
      HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
⊢ gi i ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
have rw₃ : gi i ^ ((↑j.rev : ℕ) + 1) *
      (gi i ^ (↑j : ℕ) * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)) *
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
  HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
Tactic: rw [← mul_one (gi i ^ (j.rev.1 + 1)), ← @one_pow K _ j, ← hgi i hi,
    mul_pow, ← mul_assoc, ← pow_add, Fin.val_rev, Nat.add_right_comm, Nat.add_assoc,
    Nat.sub_add_cancel (by lia), mul_right_comm, ← mul_pow, hgi i hi, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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]
i : ι
hi : i ∈ s
j : Fin (n i)
rw :
  gi i ^ ((↑j.rev : ℕ) + 1) * 1 * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
rw₁ :
  gi i ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) 1 (↑j : ℕ) *
      HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
rw₂ :
  gi i ^ ((↑j.rev : ℕ) + 1) * HMul.hMul (β := K) (gi i) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) ^ (↑j : ℕ) *
      HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
rw₃ :
  gi i ^ ((↑j.rev : ℕ) + 1) *
        (gi i ^ (↑j : ℕ) * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)) *
      HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
⊢ gi i ^ ((↑j.rev : ℕ) + 1) * HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
have rw₄ : gi i ^ ((↑j.rev : ℕ) + 1) * gi i ^ (↑j : ℕ) *
      HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ) *
    HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (n i) =
  HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (↑j : ℕ)
Tactic: rw [← mul_one (gi i ^ (j.rev.1 + 1)), ← @one_pow K _ j, ← hgi i hi,
    mul_pow, ← mul_assoc, ← pow_add, Fin.val_rev, Nat.add_right_comm, Nat.add_assoc,
    Nat.sub_add_cancel (by lia), mul_right_comm, ← mul_pow, hgi i hi, one_pow, one_mul]