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 : 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))

Tactic:
(Equiv.sum_comp Fin.revPerm _).symm.trans (Fintype.sum_congr _ _ fun j => ?_)

Premises used: Equiv.sum_comp, Fintype.sum_congr, Eq.symm, Fin.revPerm, Eq.trans
-- 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]
i : ι
hi : i ∈ s
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)
⊢ 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 (Equiv.sum_comp Fin.revPerm _).symm.trans (Fintype.sum_congr _ _ fun j => ?_)

Premises used: Equiv.sum_comp, Fintype.sum_congr, Eq.symm, Fin.revPerm, Eq.trans
-- 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]
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 ^ ((↑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)
⊢ 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:
rw [Fin.revPerm_apply, ← Finset.mul_prod_erase s _ hi, ← mul_assoc,
    mul_assoc (algebraMap R[X] K (r i j.rev))]

Premises used: Algebra.algebraMap, mul_assoc, Finset.mul_prod_erase, Polynomial, Fin.revPerm_apply, Fin.rev, 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
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)

Tactic:
congrArg (algebraMap R[X] K (r i j.rev) * · * _) ?_

Premises used: HMul.hMul, Algebra.algebraMap, congrArg, Polynomial, Fin.rev, 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
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)
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 : ℕ)
⊢ 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:
refine congrArg (algebraMap R[X] K (r i j.rev) * · * _) ?_

Premises used: HMul.hMul, Algebra.algebraMap, congrArg, Polynomial, Fin.rev, 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
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)
⊢ (↑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 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
⊢ Nontrivial R

Tactic:
have : Nontrivial R :=
    have : Nontrivial R[X] := Module.nontrivial R[X] K
    Module.nontrivial R R[X]
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
this : Nontrivial R
i : ι
hi : i ∈ s
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) (0 : K)

Tactic:
simpa using (hg i hi).ne_zero

Premises used: Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
this : Nontrivial R
⊢ ∀ (i : ι) (hi : i ∈ s),
    HMul.hMul (α := K) (β := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) =
      1

Tactic:
have hgi (i : ι) (hi : i ∈ s) : (algebraMap R[X] K (g i))⁻¹ * algebraMap R[X] K (g i) = 1 :=
    inv_mul_cancel₀ (by simpa using (hg i hi).ne_zero)
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi :
  ∀ (i : ι) (hi : i ∈ s),
    HMul.hMul (α := K) (β := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) =
      1
obtain :
  ∀ (q : R[X]) (r : (i : ι) → Fin 1 → R[X]) (hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree)
    (hf :
      HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
          (∏ i ∈ s, HPow.hPow (α := K) (β := ℕ) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) 1 : K) =
        HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
          (∑ i ∈ s,
              ∑ j : Fin 1,
                HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K)
                  (HPow.hPow (α := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) ((↑j : ℕ) + 1)) :
            K)),
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧
        HDiv.hDiv (α := K) (↑f : K) (∏ i ∈ s, (↑(g i) : K)) =
          HAdd.hAdd (α := K) (↑q : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r i) : K) (↑(g i) : K))
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i ∈ s, (r i).degree < (g i).degree) ∧
      HDiv.hDiv (α := K) (↑f : K) (∏ i ∈ s, (↑(g i) : K)) =
        HAdd.hAdd (α := K) (↑q : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r i) : K) (↑(g i) : K))

Tactic:
obtain ⟨q, r, hr, hf⟩ := mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse
    f hg hcop (fun _ => 1) hgi

Premises used: OfNat.ofNat, Polynomial.mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi :
  ∀ (i : ι) (hi : i ∈ s),
    HMul.hMul (α := K) (β := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) =
      1
q : R[X]
r : (i : ι) → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
      (∏ i ∈ s, HPow.hPow (α := K) (β := ℕ) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) 1 : K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
      (∑ i ∈ s,
          ∑ j : Fin 1,
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K)
              (HPow.hPow (α := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) ((↑j : ℕ) + 1)) :
        K)
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i ∈ s, (r i).degree < (g i).degree) ∧
      HDiv.hDiv (α := K) (↑f : K) (∏ i ∈ s, (↑(g i) : K)) =
        HAdd.hAdd (α := K) (↑q : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r i) : K) (↑(g i) : K))

Tactic:
⟨q, fun i => r i 0, fun i hi => hr i hi 0, ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi :
  ∀ (i : ι) (hi : i ∈ s),
    HMul.hMul (α := K) (β := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) =
      1
q : R[X]
r : (i : ι) → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
      (∏ i ∈ s, HPow.hPow (α := K) (β := ℕ) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) 1 : K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
      (∑ i ∈ s,
          ∑ j : Fin 1,
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K)
              (HPow.hPow (α := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) ((↑j : ℕ) + 1)) :
        K)
refine :
  HDiv.hDiv (α := K) (↑f : K) (∏ i ∈ s, (↑(g i) : K)) =
    HAdd.hAdd (α := K) (↑q : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑((fun (i : ι) ↦ r i 0) i) : K) (↑(g i) : K))
⊢ ∃ (q : R[X]) (r : ι → R[X]),
    (∀ i ∈ s, (r i).degree < (g i).degree) ∧
      HDiv.hDiv (α := K) (↑f : K) (∏ i ∈ s, (↑(g i) : K)) =
        HAdd.hAdd (α := K) (↑q : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r i) : K) (↑(g i) : K))

Tactic:
refine ⟨q, fun i => r i 0, fun i hi => hr i hi 0, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi :
  ∀ (i : ι) (hi : i ∈ s),
    HMul.hMul (α := K) (β := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) =
      1
q : R[X]
r : (i : ι) → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
      (∏ i ∈ s, HPow.hPow (α := K) (β := ℕ) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) 1 : K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
      (∑ i ∈ s,
          ∑ j : Fin 1,
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r i j) : K)
              (HPow.hPow (α := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) ((↑j : ℕ) + 1)) :
        K)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
      ((∏ x ∈ s, (algebraMap R[X] K : (a : R[X]) → K) (g x))⁻¹ : K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
      (∑ x ∈ s,
          HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (r x 0) : K)
            (((algebraMap R[X] K : (a : R[X]) → K) (g x))⁻¹ : K) :
        K)

Tactic:
simp_rw [Fin.sum_univ_one, Fin.val_zero, zero_add, pow_one, Finset.prod_inv_distrib] at hf

Premises used: Finset.prod_inv_distrib, Fin.sum_univ_one, zero_add, pow_one, Fin.val_zero
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi :
  ∀ (i : ι) (hi : i ∈ s),
    HMul.hMul (α := K) (β := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) =
      1
q : R[X]
r : (i : ι) → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
      ((∏ x ∈ s, (algebraMap R[X] K : (a : R[X]) → K) (g x))⁻¹ : K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
      (∑ x ∈ s,
          HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (r x 0) : K)
            (((algebraMap R[X] K : (a : R[X]) → K) (g x))⁻¹ : K) :
        K)
simp_rw :
  HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
      ((∏ x ∈ s, (algebraMap R[X] K : (a : R[X]) → K) (g x))⁻¹ : K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
      (∑ x ∈ s,
          HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (r x 0) : K)
            (((algebraMap R[X] K : (a : R[X]) → K) (g x))⁻¹ : K) :
        K)
⊢ HDiv.hDiv (α := K) (↑f : K) (∏ i ∈ s, (↑(g i) : K)) =
    HAdd.hAdd (α := K) (↑q : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑((fun (i : ι) ↦ r i 0) i) : K) (↑(g i) : K))

Tactic:
simp_rw [Algebra.cast, div_eq_mul_inv]

Premises used: Algebra.cast, div_eq_mul_inv
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi :
  ∀ (i : ι) (hi : i ∈ s),
    HMul.hMul (α := K) (β := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (g i) : K) =
      1
q : R[X]
r : (i : ι) → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
      ((∏ x ∈ s, (algebraMap R[X] K : (a : R[X]) → K) (g x))⁻¹ : K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
      (∑ x ∈ s,
          HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (r x 0) : K)
            (((algebraMap R[X] K : (a : R[X]) → K) (g x))⁻¹ : K) :
        K)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
      ((∏ x ∈ s, (algebraMap R[X] K : (a : R[X]) → K) (g x))⁻¹ : K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
      (∑ x ∈ s,
          HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (r x 0) : K)
            (((algebraMap R[X] K : (a : R[X]) → K) (g x))⁻¹ : K) :
        K)

Tactic:
hf