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 : 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:
exact hf
-- 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
ι : 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))
⊢ 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
ι : 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
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
ι : 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
⊢ ∀ (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
ι : 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

Tactic:
(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

Premises used: And.imp_right, Polynomial.quo_add_sum_rem_mul_pow_inverse_unique
-- 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
ι : 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
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)
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

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

Premises used: And.imp_right, Polynomial.quo_add_sum_rem_mul_pow_inverse_unique
-- 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
ι : 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
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)
⊢ 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:
simp_rw [Fin.sum_univ_one, Fin.val_zero, zero_add, pow_one, ← div_eq_mul_inv]

Premises used: Fin.sum_univ_one, zero_add, div_eq_mul_inv, 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
ι : 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)
      (∑ 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:
hf
-- 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
ι : 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)
      (∑ 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:
exact hf
-- 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 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
⊢ ∀ (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
-- 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 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
⊢ (↑Finset.univ : Set Bool).Pairwise fun (i j : Bool) ↦ IsCoprime (g i) (g j)

Tactic:
simp [g, Set.pairwise_insert, hcoprime, hcoprime.symm]

Premises used: IsCoprime.symm, Set.pairwise_insert
-- 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 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
⊢ (↑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]
-- 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 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)
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)
⊢ ∃ (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

Premises used: Polynomial.div_prod_eq_quo_add_sum_rem_div
-- 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 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)

Tactic:
⟨q, r true, r false, hr true (Finset.mem_univ true), hr false (Finset.mem_univ false), ?_⟩

Premises used: Finset.mem_univ, Bool.true, And.intro, Exists.intro, Bool.false
-- 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 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))
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)
⊢ ∃ (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:
refine ⟨q, r true, r false, hr true (Finset.mem_univ true), hr false (Finset.mem_univ false), ?_⟩
-- 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 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))
⊢ (↑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:
simpa [g, add_assoc] using hf

Premises used: add_assoc
-- 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
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
⊢ ∀ (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
-- 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
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
⊢ (↑Finset.univ : Set Bool).Pairwise fun (i j : Bool) ↦ IsCoprime (g i) (g j)

Tactic:
simp [g, Set.pairwise_insert, hcoprime, hcoprime.symm]

Premises used: IsCoprime.symm, Set.pairwise_insert
-- 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
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
⊢ (↑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]
-- 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
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)
⊢ ∀ (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