awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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
⊢ g i ^ n i ≠ 0

Tactic:
((hg i hi).pow (n i)).ne_zero

Premises used: Polynomial.Monic.pow, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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
⊢ g i ^ n i ≠ 0

Tactic:
exact ((hg i hi).pow (n i)).ne_zero

Premises used: Polynomial.Monic.pow, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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 * g i ^ (↑j : ℕ)).degree < (g i ^ n i).degree

Tactic:
(degree_mul_le _ _).trans_lt ?_

Premises used: Polynomial.degree_mul_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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
refine_2 : (r i j).degree + (g i ^ (↑j : ℕ)).degree < (g i ^ n i).degree
⊢ (r i j * g i ^ (↑j : ℕ)).degree < (g i ^ n i).degree

Tactic:
refine (degree_mul_le _ _).trans_lt ?_

Premises used: Polynomial.degree_mul_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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
refine_2 : (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) < (↑(n i * (g i).natDegree) : WithBot ℕ)
⊢ (r i j).degree + (g i ^ (↑j : ℕ)).degree < (g i ^ n i).degree

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

Premises used: Polynomial.degree_eq_natDegree, Polynomial.Monic.natDegree_pow, Fin.val, Polynomial.Monic.pow, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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
rw : (↑((n i - 1 + 1) * (g i).natDegree) : WithBot ℕ)
| (↑(n i * (g i).natDegree) : WithBot ℕ)

Tactic:
rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.2 j.neZero.ne)]

Premises used: Iff.mpr, Nat.sub_add_cancel, Nat.one_le_iff_ne_zero, NeZero.ne
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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
refine_2 :
  (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) < (↑((n i - 1 + 1) * (g i).natDegree) : WithBot ℕ)
⊢ (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) < (↑(n i * (g i).natDegree) : WithBot ℕ)

Tactic:
conv_rhs => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.2 j.neZero.ne)]

Premises used: Iff.mpr, Nat.sub_add_cancel, Nat.one_le_iff_ne_zero, NeZero.ne
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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
refine_2 :
  (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) <
    (g i).degree + (↑((n i - 1) * (g i).natDegree) : WithBot ℕ)
⊢ (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) < (↑((n i - 1 + 1) * (g i).natDegree) : WithBot ℕ)

Tactic:
rw [Nat.add_one_mul, Nat.add_comm, Nat.cast_add, ← degree_eq_natDegree (hg i hi).ne_zero]

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_add, Nat.add_one_mul, Polynomial.Monic.ne_zero, Nat.add_comm
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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 ℕ)

Tactic:
WithBot.add_lt_add_of_lt_of_le (WithBot.natCast_ne_bot _) (hr i hi j) ?_

Premises used: WithBot.natCast_ne_bot, WithBot.add_lt_add_of_lt_of_le
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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
refine_2 :
  LE.le (α := WithBot ℕ) (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) (↑((n i - 1) * (g i).natDegree) : WithBot ℕ)
⊢ (r i j).degree + (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) <
    (g i).degree + (↑((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) ?_

Premises used: WithBot.natCast_ne_bot, WithBot.add_lt_add_of_lt_of_le
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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
⊢ LE.le (α := WithBot ℕ) (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) (↑((n i - 1) * (g i).natDegree) : WithBot ℕ)

Tactic:
Nat.cast_le.2 (Nat.mul_le_mul_right _ (Nat.le_sub_one_of_lt j.isLt))

Premises used: Iff.mpr, Nat.mul_le_mul_right, Fin.isLt, Nat.le_sub_one_of_lt, Nat.cast_le
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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
⊢ LE.le (α := WithBot ℕ) (↑((↑j : ℕ) * (g i).natDegree) : WithBot ℕ) (↑((n i - 1) * (g i).natDegree) : WithBot ℕ)

Tactic:
exact Nat.cast_le.2 (Nat.mul_le_mul_right _ (Nat.le_sub_one_of_lt j.isLt))

Premises used: Iff.mpr, Nat.mul_le_mul_right, Fin.isLt, Nat.le_sub_one_of_lt, Nat.cast_le
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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), 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))
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₂

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

Premises used: IsCoprime.pow, Polynomial.Monic.pow, Polynomial.quo_mul_prod_add_sum_rem_mul_prod_unique, Set.Pairwise.imp
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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₂
⊢ ∀ 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

Premises used: IsCoprime.pow, Polynomial.Monic.pow, Polynomial.quo_mul_prod_add_sum_rem_mul_prod_unique, Set.Pairwise.imp
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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

Tactic:
⟨hq, fun i hi => ?_⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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 : ℕ))
refine : ∀ (i : ι) (hi : i ∈ s), r₁ i = r₂ i
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
refine ⟨hq, fun i hi => ?_⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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 : ℕ))
i : ι
hi : i ∈ s
⊢ r₁ i = r₂ i

Tactic:
(quo_mul_pow_add_sum_rem_mul_pow_unique (hg i hi) (hr₁ i hi) (hr₂ i hi)
    (congrArg (0 * g i ^ n i + ·) (hr i hi))).2

Premises used: HMul.hMul, congrArg, Polynomial.quo_mul_pow_add_sum_rem_mul_pow_unique, HPow.hPow, And.right, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
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 : ℕ))
i : ι
hi : i ∈ s
⊢ r₁ i = r₂ i

Tactic:
exact (quo_mul_pow_add_sum_rem_mul_pow_unique (hg i hi) (hr₁ i hi) (hr₂ i hi)
    (congrArg (0 * g i ^ n i + ·) (hr i hi))).2

Premises used: HMul.hMul, congrArg, Polynomial.quo_mul_pow_add_sum_rem_mul_pow_unique, HPow.hPow, And.right, HAdd.hAdd, OfNat.ofNat