awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
h : supDegree D (p - q) = supDegree D p
refine_2 : Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) (0 : R)
refine_2₁ :
  HSub.hSub (α := R) (β := R) ((p : (a : A) → R) (Function.invFun D (supDegree D p)) : R)
      ((q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) =
    0
⊢ Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
have refine_2₂ : HSub.hSub (β := R) (leadingCoeff D p) ((q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) = 0
Tactic: rwa [h, Finsupp.sub_apply, ← leadingCoeff, hd, ← leadingCoeff, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
h : supDegree D (p - q) = supDegree D p
refine_2 : Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) (0 : R)
refine_2₁ :
  HSub.hSub (α := R) (β := R) ((p : (a : A) → R) (Function.invFun D (supDegree D p)) : R)
      ((q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) =
    0
refine_2₂ : HSub.hSub (β := R) (leadingCoeff D p) ((q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) = 0
⊢ Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
have refine_2₃ : HSub.hSub (β := R) (leadingCoeff D p) ((q : (a : A) → R) (Function.invFun D (supDegree D q)) : R) = 0
Tactic: rwa [h, Finsupp.sub_apply, ← leadingCoeff, hd, ← leadingCoeff, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
h : supDegree D (p - q) = supDegree D p
refine_2 : Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) (0 : R)
refine_2₁ :
  HSub.hSub (α := R) (β := R) ((p : (a : A) → R) (Function.invFun D (supDegree D p)) : R)
      ((q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) =
    0
refine_2₂ : HSub.hSub (β := R) (leadingCoeff D p) ((q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) = 0
refine_2₃ : HSub.hSub (β := R) (leadingCoeff D p) ((q : (a : A) → R) (Function.invFun D (supDegree D q)) : R) = 0
⊢ Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
have refine_2₄ : leadingCoeff D p - leadingCoeff D q = 0
Tactic: rwa [h, Finsupp.sub_apply, ← leadingCoeff, hd, ← leadingCoeff, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ j ∈ s, f j) = supDegree D (f i) ∧
    leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)
have rw : supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
  leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
Tactic: rw [← s.add_sum_erase _ hi]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
⊢ supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
have pos : ∀ (hs : s.erase i = ∅),
  supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
Tactic: by_cases! hs : s.erase i = ∅
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
pos :
  ∀ (hs : s.erase i = ∅),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
⊢ supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
have neg : ∀ (hs : (s.erase i).Nonempty),
  supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
Tactic: by_cases! hs : s.erase i = ∅
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : s.erase i = ∅
⊢ supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
have pos : supDegree D (f i) = supDegree D (f i) ∧ leadingCoeff D (f i) = leadingCoeff D (f i)
Tactic: rw [hs, Finset.sum_empty, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
⊢ supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
have neg : supDegree.{u_1, u_3, u_5} (R := R) D (∑ x ∈ s.erase i, f x) < supDegree D (f i)
Tactic: suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs neg : (s.erase i).Nonempty
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ x ∈ s.erase i, f x) < supDegree D (f i)
have neg₁ : ∀ (j : ι) (hj : j ∈ s.erase i), supDegree D (f j) < supDegree D (f i)
Tactic: refine supDegree_sum_lt ?_ (fun j hj => ?_)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (hypothesis)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
j : ι
hj : j ∈ s.erase i
⊢ supDegree D (f j) < supDegree D (f i)
have hj₁ : j ≠ i ∧ j ∈ s
Tactic: rw [Finset.mem_erase] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ j ∈ s, f j) = supDegree D (f i) ∧
    leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)
have rw : supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
  leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
Tactic: classical
  rw [← s.add_sum_erase _ hi]
  by_cases! hs : s.erase i = ∅
  · rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩
  suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
  refine supDegree_sum_lt ?_ (fun j hj => ?_)
  · exact hs
  · rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
rw rw₁ rw₂ :
  supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ j ∈ s, f j) = supDegree D (f i) ∧
    leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)
have pos : ∀ (hs : s.erase i = ∅),
  supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
Tactic: classical
  rw [← s.add_sum_erase _ hi]
  by_cases! hs : s.erase i = ∅
  · rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩
  suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
  refine supDegree_sum_lt ?_ (fun j hj => ?_)
  · exact hs
  · rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
rw rw₁ rw₂ :
  supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
pos :
  ∀ (hs : s.erase i = ∅),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ j ∈ s, f j) = supDegree D (f i) ∧
    leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)
have neg : ∀ (hs : (s.erase i).Nonempty),
  supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
Tactic: classical
  rw [← s.add_sum_erase _ hi]
  by_cases! hs : s.erase i = ∅
  · rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩
  suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
  refine supDegree_sum_lt ?_ (fun j hj => ?_)
  · exact hs
  · rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
rw rw₁ rw₂ :
  supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
pos :
  ∀ (hs : s.erase i = ∅),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
neg neg₁ :
  ∀ (hs : (s.erase i).Nonempty),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ j ∈ s, f j) = supDegree D (f i) ∧
    leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)
have neg₂ : ∀ (hs : (s.erase i).Nonempty), supDegree.{u_1, u_3, u_5} (R := R) D (∑ x ∈ s.erase i, f x) < supDegree D (f i)
Tactic: classical
  rw [← s.add_sum_erase _ hi]
  by_cases! hs : s.erase i = ∅
  · rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩
  suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
  refine supDegree_sum_lt ?_ (fun j hj => ?_)
  · exact hs
  · rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
rw rw₁ rw₂ :
  supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
pos :
  ∀ (hs : s.erase i = ∅),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
neg neg₁ :
  ∀ (hs : (s.erase i).Nonempty),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
neg₂ : ∀ (hs : (s.erase i).Nonempty), supDegree.{u_1, u_3, u_5} (R := R) D (∑ x ∈ s.erase i, f x) < supDegree D (f i)
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ j ∈ s, f j) = supDegree D (f i) ∧
    leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)
have neg₃ : ∀ (hs : (s.erase i).Nonempty), (s.erase i).Nonempty
Tactic: classical
  rw [← s.add_sum_erase _ hi]
  by_cases! hs : s.erase i = ∅
  · rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩
  suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
  refine supDegree_sum_lt ?_ (fun j hj => ?_)
  · exact hs
  · rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
rw rw₁ rw₂ :
  supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
pos :
  ∀ (hs : s.erase i = ∅),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
neg neg₁ :
  ∀ (hs : (s.erase i).Nonempty),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
neg₂ : ∀ (hs : (s.erase i).Nonempty), supDegree.{u_1, u_3, u_5} (R := R) D (∑ x ∈ s.erase i, f x) < supDegree D (f i)
neg₃ : ∀ (hs : (s.erase i).Nonempty), (s.erase i).Nonempty
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ j ∈ s, f j) = supDegree D (f i) ∧
    leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)
have neg₄ : ∀ (hs : (s.erase i).Nonempty) (j : ι) (hj : j ∈ s.erase i), supDegree D (f j) < supDegree D (f i)
Tactic: classical
  rw [← s.add_sum_erase _ hi]
  by_cases! hs : s.erase i = ∅
  · rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩
  suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
  refine supDegree_sum_lt ?_ (fun j hj => ?_)
  · exact hs
  · rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hs : ∃ i ∈ s, f i ≠ 0
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0
have obtain : ∀ (j : ι) (hj : j ∈ s) (hne : f j ≠ 0), Ne (α := R[A]) (∑ i ∈ s, f i) 0
Tactic: obtain ⟨j, hj, hne⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne : f j ≠ 0
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0
have obtain : ∀ (i : ι) (hi : i ∈ s) (he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i), Ne (α := R[A]) (∑ i ∈ s, f i) 0
Tactic: obtain ⟨i, hi, he⟩ := exists_mem_eq_sup _ ⟨j, hj⟩ (supDegree D ∘ f)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0
have pos : ∀ (h : ∀ k ∈ s, k = i), Ne (α := R[A]) (∑ i ∈ s, f i) 0
Tactic: by_cases! h : ∀ k ∈ s, k = i
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
pos : ∀ (h : ∀ k ∈ s, k = i), Ne (α := R[A]) (∑ i ∈ s, f i) 0
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0
have neg : ∀ (h : ∃ k ∈ s, k ≠ i), Ne (α := R[A]) (∑ i ∈ s, f i) 0
Tactic: by_cases! h : ∀ k ∈ s, k = i
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0
have pos : ∀ (k : ι) (hk : k ∈ s) (hne : k ≠ j), f k = 0
Tactic: refine (sum_eq_single_of_mem j hj (fun k hk hne => ?_)).trans_ne hne
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (hypothesis)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne_1 : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : k ≠ j
⊢ f k = 0
have hne₁ : i ≠ i
Tactic: rw [h k hk, h j hj] at hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∃ k ∈ s, k ≠ i
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0
have neg : ∀ (j : ι) (hj : j ∈ s) (hne : j ≠ i), Ne (α := R[A]) (∑ i ∈ s, f i) 0
Tactic: obtain ⟨j, hj, hne⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j_1 : ι
hj_1 : j_1 ∈ s
hne_1 : f j_1 ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0
have neg : supDegree.{u_1, u_3, u_5} (R := R) D (∑ i ∈ s, f i) ≠ ⊥
Tactic: apply ne_zero_of_supDegree_ne_bot (D := D)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (hypothesis)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j_1 : ι
hj_1 : j_1 ∈ s
hne_1 : f j_1 ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ i ∈ s, f i) ≠ ⊥
have this : ∀ (k : ι) (hk : k ∈ s) (hne : k ≠ i), supDegree D (f k) < supDegree D (f i)
Tactic: have (k) (hk : k ∈ s) (hne : k ≠ i) : supDegree D (f k) < supDegree D (f i) :=
    ((le_sup hk).trans_eq he).lt_of_ne (hd.ne hk hi hne)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j_1 : ι
hj_1 : j_1 ∈ s
hne_1 : f j_1 ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
this : ∀ (k : ι) (hk : k ∈ s) (hne : k ≠ i), supDegree D (f k) < supDegree D (f i)
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ i ∈ s, f i) ≠ ⊥
have neg : supDegree D (f i) ≠ ⊥
Tactic: rw [(supDegree_leadingCoeff_sum_eq hi this).1]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
⊢ (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
have inl : (0 * q : (a : A) → R) (Function.invFun D (supDegree.{u_1, u_3, u_5} (R := R) D 0 + supDegree D q)) =
  leadingCoeff D 0 * leadingCoeff D q
Tactic: obtain rfl | hp := eq_or_ne p 0
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inl :
  (0 * q : (a : A) → R) (Function.invFun D (supDegree.{u_1, u_3, u_5} (R := R) D 0 + supDegree D q)) =
    leadingCoeff D 0 * leadingCoeff D q
⊢ (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
have inr : ∀ (hp : p ≠ 0),
  (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
Tactic: obtain rfl | hp := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
⊢ (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
have inr : (p * 0 : (a : A) → R) (Function.invFun D (supDegree D p + supDegree.{u_1, u_3, u_5} (R := R) D 0)) =
  leadingCoeff D p * leadingCoeff D 0
Tactic: obtain rfl | hq := eq_or_ne q 0
Cleared hypotheses: q