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₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
have 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)
Tactic: classical
  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⟩
  intro q r
  simp_rw [add_mul, Finset.sum_mul, map_add, map_sum, map_mul, map_prod, map_pow]
  refine congrArg (_ + ·) (Finset.sum_congr rfl fun i hi => ?_)
  refine (Equiv.sum_comp Fin.revPerm _).symm.trans (Fintype.sum_congr _ _ fun j => ?_)
  rw [Fin.revPerm_apply, ← Finset.mul_prod_erase s _ hi, ← mul_assoc,
    mul_assoc (algebraMap R[X] K (r i j.rev))]
  refine congrArg (algebraMap R[X] K (r i j.rev) * · * _) ?_
  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 (hypothesis)
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)
⊢ ∃ (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))
have this : Nontrivial R
Tactic: have : Nontrivial R :=
    have : Nontrivial R[X] := Module.nontrivial R[X] K
    Module.nontrivial R R[X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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
⊢ ∃ (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))
have 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
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)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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 : ι → 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))
have 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))
Tactic: obtain ⟨q, r, hr, hf⟩ := mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse
    f hg hcop (fun _ => 1) hgi
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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))
have 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))
Tactic: refine ⟨q, fun i => r i 0, fun i hi => hr i hi 0, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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)
⊢ 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))
have 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)
Tactic: simp_rw [Fin.sum_univ_one, Fin.val_zero, zero_add, pow_one, Finset.prod_inv_distrib] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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
ι : 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)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf :
  HAdd.hAdd (α := K) (↑q₁ : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r₁ i) : K) (↑(g i) : K)) =
    HAdd.hAdd (α := K) (↑q₂ : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r₂ i) : K) (↑(g i) : K))
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
have this : Nontrivial R
Tactic: have : Nontrivial R :=
    have : Nontrivial R[X] := Module.nontrivial R[X] K
    Module.nontrivial R R[X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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
ι : 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)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf :
  HAdd.hAdd (α := K) (↑q₁ : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r₁ i) : K) (↑(g i) : K)) =
    HAdd.hAdd (α := K) (↑q₂ : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r₂ i) : K) (↑(g i) : K))
this : Nontrivial R
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
have 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
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)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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
ι : 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)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf :
  HAdd.hAdd (α := K) (↑q₁ : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r₁ i) : K) (↑(g i) : K)) =
    HAdd.hAdd (α := K) (↑q₂ : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r₂ i) : K) (↑(g i) : K))
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₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
have refine : HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₁ : K)
    (∑ i ∈ s,
        ∑ j : Fin ((fun (x : ι) ↦ 1) i),
          HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₁ i) : K)
            (HPow.hPow (α := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) ((↑j : ℕ) + 1)) :
      K) =
  HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₂ : K)
    (∑ i ∈ s,
        ∑ j : Fin ((fun (x : ι) ↦ 1) i),
          HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₂ i) : K)
            (HPow.hPow (α := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) ((↑j : ℕ) + 1)) :
      K)
Tactic: refine (quo_add_sum_rem_mul_pow_inverse_unique (n := fun _ => 1)
      hg hcop hgi (fun i hi _ => hr₁ i hi) (fun i hi _ => hr₂ i hi) ?_).imp_right
      fun h i hi => congrFun (h i hi) 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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
ι : 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)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf :
  HAdd.hAdd (α := K) (↑q₁ : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r₁ i) : K) (↑(g i) : K)) =
    HAdd.hAdd (α := K) (↑q₂ : K) (∑ i ∈ s, HDiv.hDiv (α := K) (↑(r₂ i) : K) (↑(g i) : K))
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
⊢ HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₁ : K)
      (∑ i ∈ s,
          ∑ j : Fin ((fun (x : ι) ↦ 1) i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₁ i) : K)
              (HPow.hPow (α := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) ((↑j : ℕ) + 1)) :
        K) =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₂ : K)
      (∑ i ∈ s,
          ∑ j : Fin ((fun (x : ι) ↦ 1) i),
            HMul.hMul (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₂ i) : K)
              (HPow.hPow (α := K) (((algebraMap R[X] K : (a : R[X]) → K) (g i))⁻¹ : K) ((↑j : ℕ) + 1)) :
        K)
have simp_rw : HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₁ : K)
    (∑ x ∈ s,
        HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₁ x) : K)
          ((algebraMap R[X] K : (a : R[X]) → K) (g x) : K) :
      K) =
  HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) q₂ : K)
    (∑ x ∈ s,
        HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (r₂ x) : 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, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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 g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
g : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) g₂ g₁ t
⊢ ∃ (q : R[X]) (r₁ : R[X]) (r₂ : R[X]),
    r₁.degree < g₁.degree ∧
      r₂.degree < g₂.degree ∧
        (↑f : K) / HMul.hMul (α := K) (↑g₁ : K) (↑g₂ : K) =
          (↑q : K) + HDiv.hDiv (α := K) (↑r₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂ : K) (↑g₂ : K)
have hg : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (g i).Monic
Tactic: have hg (i : Bool) (_ : i ∈ Finset.univ) : (g i).Monic := Bool.rec hg₂ hg₁ i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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 g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
g : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) g₂ g₁ t
hg : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (g i).Monic
⊢ ∃ (q : R[X]) (r₁ : R[X]) (r₂ : R[X]),
    r₁.degree < g₁.degree ∧
      r₂.degree < g₂.degree ∧
        (↑f : K) / HMul.hMul (α := K) (↑g₁ : K) (↑g₂ : K) =
          (↑q : K) + HDiv.hDiv (α := K) (↑r₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂ : K) (↑g₂ : K)
have hcoprime₁ : (↑Finset.univ : Set Bool).Pairwise fun (i j : Bool) ↦ IsCoprime (g i) (g j)
Tactic: have hcoprime : Set.Pairwise (Finset.univ : Finset Bool) fun i j => IsCoprime (g i) (g j) := by
    simp [g, Set.pairwise_insert, hcoprime, hcoprime.symm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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 g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime_1 : IsCoprime g₁ g₂
g : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) g₂ g₁ t
hg : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (g i).Monic
hcoprime : (↑Finset.univ : Set Bool).Pairwise fun (i j : Bool) ↦ IsCoprime (g i) (g j)
⊢ ∃ (q : R[X]) (r₁ : R[X]) (r₂ : R[X]),
    r₁.degree < g₁.degree ∧
      r₂.degree < g₂.degree ∧
        (↑f : K) / HMul.hMul (α := K) (↑g₁ : K) (↑g₂ : K) =
          (↑q : K) + HDiv.hDiv (α := K) (↑r₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂ : K) (↑g₂ : K)
have obtain : ∀ (q : R[X]) (r : Bool → R[X])
  (hr : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (r i).degree < (g i).degree)
  (hf :
    HDiv.hDiv (α := K) (↑f : K) (∏ i : Bool, (↑(g i) : K)) =
      HAdd.hAdd (α := K) (↑q : K) (∑ i : Bool, HDiv.hDiv (α := K) (↑(r i) : K) (↑(g i) : K))),
  ∃ (q : R[X]) (r₁ : R[X]) (r₂ : R[X]),
    r₁.degree < g₁.degree ∧
      r₂.degree < g₂.degree ∧
        (↑f : K) / HMul.hMul (α := K) (↑g₁ : K) (↑g₂ : K) =
          (↑q : K) + HDiv.hDiv (α := K) (↑r₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂ : K) (↑g₂ : K)
Tactic: obtain ⟨q, r, hr, hf⟩ := div_prod_eq_quo_add_sum_rem_div K f hg hcoprime
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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 g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime_1 : IsCoprime g₁ g₂
g : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) g₂ g₁ t
hg : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (g i).Monic
hcoprime : (↑Finset.univ : Set Bool).Pairwise fun (i j : Bool) ↦ IsCoprime (g i) (g j)
q : R[X]
r : Bool → R[X]
hr : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (r i).degree < (g i).degree
hf :
  HDiv.hDiv (α := K) (↑f : K) (∏ i : Bool, (↑(g i) : K)) =
    HAdd.hAdd (α := K) (↑q : K) (∑ i : Bool, HDiv.hDiv (α := K) (↑(r i) : K) (↑(g i) : K))
⊢ ∃ (q : R[X]) (r₁ : R[X]) (r₂ : R[X]),
    r₁.degree < g₁.degree ∧
      r₂.degree < g₂.degree ∧
        (↑f : K) / HMul.hMul (α := K) (↑g₁ : K) (↑g₂ : K) =
          (↑q : K) + HDiv.hDiv (α := K) (↑r₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂ : K) (↑g₂ : K)
have refine : (↑f : K) / HMul.hMul (α := K) (↑g₁ : K) (↑g₂ : K) =
  (↑q : K) + HDiv.hDiv (α := K) (↑(r true) : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑(r false) : K) (↑g₂ : K)
Tactic: refine ⟨q, r true, r false, hr true (Finset.mem_univ true), hr false (Finset.mem_univ false), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf :
  (↑q₁ : K) + HDiv.hDiv (α := K) (↑r₁₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₁ : K) (↑g₂ : K) =
    (↑q₂ : K) + HDiv.hDiv (α := K) (↑r₁₂ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₂ : K) (↑g₂ : K)
g : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) g₂ g₁ t
r₁ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₂ r₁₂ t
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂
have hg : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (g i).Monic
Tactic: have hg (i : Bool) (_ : i ∈ Finset.univ) : (g i).Monic := Bool.rec hg₂ hg₁ i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf :
  (↑q₁ : K) + HDiv.hDiv (α := K) (↑r₁₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₁ : K) (↑g₂ : K) =
    (↑q₂ : K) + HDiv.hDiv (α := K) (↑r₁₂ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₂ : K) (↑g₂ : K)
g : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) g₂ g₁ t
r₁ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₂ r₁₂ t
hg : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (g i).Monic
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂
have hcoprime₁ : (↑Finset.univ : Set Bool).Pairwise fun (i j : Bool) ↦ IsCoprime (g i) (g j)
Tactic: have hcoprime : Set.Pairwise (Finset.univ : Finset Bool) fun i j => IsCoprime (g i) (g j) := by
    simp [g, Set.pairwise_insert, hcoprime, hcoprime.symm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime_1 : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf :
  (↑q₁ : K) + HDiv.hDiv (α := K) (↑r₁₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₁ : K) (↑g₂ : K) =
    (↑q₂ : K) + HDiv.hDiv (α := K) (↑r₁₂ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₂ : K) (↑g₂ : K)
g : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) g₂ g₁ t
r₁ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₂ r₁₂ t
hg : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (g i).Monic
hcoprime : (↑Finset.univ : Set Bool).Pairwise fun (i j : Bool) ↦ IsCoprime (g i) (g j)
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂
have hr₁ : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (r₁ i).degree < (g i).degree
Tactic: have hr₁ (i : Bool) (_ : i ∈ Finset.univ) : (r₁ i).degree < (g i).degree := Bool.rec hr₂₁ hr₁₁ i