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
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
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
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
h_1 : Membership.mem (γ := Finset (Fin (n i))) Finset.univ j
⊢ (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) <
    (g i).degree + (↑((n i - 1) * (g i).natDegree) : WithBot ℕ)
have refine_2 : LE.le (α := WithBot ℕ) (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) (↑((n i - 1) * (g i).natDegree) : WithBot ℕ)
Tactic: refine WithBot.add_lt_add_of_lt_of_le (WithBot.natCast_ne_bot _) (hr i hi j) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
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
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
have hrd : ∀ {r : (i : ι) → Fin (n i) → R[X]} (hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) (i : ι)
  (hi : i ∈ s), degree.{u_1} (R := R) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ)) < (g i ^ n i).degree
Tactic: have hrd {r : (i : ι) → Fin (n i) → R[X]} (hr : ∀ i ∈ s, ∀ j, (r i j).degree < (g i).degree)
      (i : ι) (hi : i ∈ s) : (∑ j, r i j * g i ^ j.1).degree < (g i ^ n i).degree := by
    refine (degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff ?_).2 fun j _ => ?_)
    · rw [bot_lt_iff_ne_bot, degree_ne_bot]
      exact ((hg i hi).pow (n i)).ne_zero
    · refine (degree_mul_le _ _).trans_lt ?_
      rw [degree_eq_natDegree ((hg i hi).pow j.1).ne_zero, (hg i hi).natDegree_pow,
        degree_eq_natDegree ((hg i hi).pow (n i)).ne_zero, (hg i hi).natDegree_pow]
      conv_rhs => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.2 j.neZero.ne)]
      rw [Nat.add_one_mul, Nat.add_comm, Nat.cast_add, ← degree_eq_natDegree (hg i hi).ne_zero]
      refine WithBot.add_lt_add_of_lt_of_le (WithBot.natCast_ne_bot _) (hr i hi j) ?_
      exact Nat.cast_le.2 (Nat.mul_le_mul_right _ (Nat.le_sub_one_of_lt j.isLt))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
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
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
hrd :
  ∀ {r : (i : ι) → Fin (n i) → R[X]} (hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) (i : ι)
    (hi : i ∈ s), degree.{u_1} (R := R) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ)) < (g i ^ n i).degree
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
have hq : q₁ = q₂
Tactic: obtain ⟨hq, hr⟩ := quo_mul_prod_add_sum_rem_mul_prod_unique
    (fun i hi => (hg i hi).pow (n i)) (hgg.imp fun i j hij => hij.pow) (hrd hr₁) (hrd 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 ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
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
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
hrd :
  ∀ {r : (i : ι) → Fin (n i) → R[X]} (hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) (i : ι)
    (hi : i ∈ s), degree.{u_1} (R := R) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ)) < (g i ^ n i).degree
hq : q₁ = q₂
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
have hr : ∀ i ∈ s, Eq.{u_1 + 1} (α := R[X]) (∑ j : Fin (n i), r₁ i j * g i ^ (↑j : ℕ)) (∑ j : Fin (n i), r₂ i j * g i ^ (↑j : ℕ))
Tactic: obtain ⟨hq, hr⟩ := quo_mul_prod_add_sum_rem_mul_prod_unique
    (fun i hi => (hg i hi).pow (n i)) (hgg.imp fun i j hij => hij.pow) (hrd hr₁) (hrd 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 ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ IsCoprime (g i) (g j)
n : ι → ℕ
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
h : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₁ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i) =
    q₂ * ∏ i ∈ s, g i ^ n i +
      ∑ x ∈ s, HMul.hMul (α := R[X]) (∑ i : Fin (n x), r₂ x i * g x ^ (↑i : ℕ)) (∏ i ∈ s.erase x, g i ^ n i)
hrd :
  ∀ {r : (i : ι) → Fin (n i) → R[X]} (hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) (i : ι)
    (hi : i ∈ s), degree.{u_1} (R := R) (∑ j : Fin (n i), r i j * g i ^ (↑j : ℕ)) < (g i ^ n i).degree
hq : q₁ = q₂
hr :
  ∀ i ∈ s,
    Eq.{u_1 + 1} (α := R[X]) (∑ j : Fin (n i), r₁ i j * g i ^ (↑j : ℕ)) (∑ j : Fin (n i), r₂ i j * g i ^ (↑j : ℕ))
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
have refine : ∀ (i : ι) (hi : i ∈ s), r₁ i = r₂ i
Tactic: refine ⟨hq, 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 : 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]),
    (∀ 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)
have 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)
Tactic: obtain ⟨q, r, hr, hf⟩ := eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow f hg hgg n
-- 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 : 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)
have 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)
Tactic: refine ⟨q, fun i j => r i j.rev, fun i hi j => hr i hi 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 : 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
⊢ 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)
have 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)
Tactic: rw [hf, map_add, map_mul, map_prod, add_mul, mul_assoc, ← Finset.prod_mul_distrib]
-- 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 : 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
have rw : HPow.hPow (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (n x) * gi x ^ n x = 1
Tactic: rw [map_pow, ← mul_pow, mul_comm, hgi x hx, one_pow]
-- 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 : 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
⊢ HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x ^ n x) : K) (gi x ^ n x) = 1
have rw₁ : HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) (gi x) ^ n x = 1
Tactic: rw [map_pow, ← mul_pow, mul_comm, hgi x hx, one_pow]
-- 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 : 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
⊢ HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x ^ n x) : K) (gi x ^ n x) = 1
have rw₂ : HMul.hMul (β := K) (gi x) ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) ^ n x = 1
Tactic: rw [map_pow, ← mul_pow, mul_comm, hgi x hx, one_pow]
-- 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 : 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
⊢ HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x ^ n x) : K) (gi x ^ n x) = 1
have rw₃ : HPow.hPow (α := K) 1 (n x) = 1
Tactic: rw [map_pow, ← mul_pow, mul_comm, hgi x hx, one_pow]
-- 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 : 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
⊢ HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (g x ^ n x) : K) (gi x ^ n x) = 1
have rw₄ : Eq.{u_2 + 1} (α := K) 1 1
Tactic: rw [map_pow, ← mul_pow, mul_comm, hgi x hx, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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
⊢ 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)
have 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
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]
-- 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 : 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
⊢ 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)
have 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)))
Tactic: rw [Finset.prod_congr rfl hc, Finset.prod_const_one,
    mul_one, add_right_inj, map_sum, Finset.sum_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 : 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)))
have 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))
Tactic: refine Finset.sum_congr rfl fun i hi => ?_