awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
refine_1 : degt 0 ≤ 0
⊢ LE.le (α := Tᵒᵈ)
    (Quot.lift (r := (⇑(List.isSetoid T) : List T → List T → Prop))
      (fun (l : List T) ↦ List.foldr (fun (x1 x2 : T) ↦ x1 ⊓ x2) ⊤ l) ⋯ (Multiset.map degt l.prod.support.val))
    (List.foldr (fun (x1 x2 : T) ↦ x1 + x2) 0 (List.map (fun (f : R[A]) ↦ f.support.inf degt) l))
have refine_2 : ∀ (a b : A), degt (a + b) ≤ degt a + degt b
Tactic: refine sup_support_list_prod_le ?_ ?_ l
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ degt 0 ≤ 0
have refine_1 : LE.le (α := T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) 0 : T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt 0) : T)
Tactic: refine (OrderDual.ofDual_le_ofDual.mp ?_)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ ∀ (a b : A), degt (a + b) ≤ degt a + degt b
have refine_2 : ∀ (a b : A),
  LE.le (α := T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt a + degt b) : T)
    ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt (a + b)) : T)
Tactic: refine (fun a b => OrderDual.ofDual_le_ofDual.mp ?_)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (f ^ n).support.sup degb ≤ n • f.support.sup degb
have rw : (List.replicate n f).prod.support.sup degb ≤ (List.replicate n (f.support.sup degb)).sum
Tactic: rw [← List.prod_replicate, ← List.sum_replicate]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (List.replicate n f).prod.support.sup degb ≤ (List.replicate n (f.support.sup degb)).sum
have refine : List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) (List.replicate n f)) =
  (List.replicate n (f.support.sup degb)).sum
Tactic: refine (sup_support_list_prod_le degb0 degbm _).trans_eq ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) (List.replicate n f)) =
    (List.replicate n (f.support.sup degb)).sum
have rw : (List.replicate n (f.support.sup degb)).sum = (List.replicate n (f.support.sup degb)).sum
Tactic: rw [List.map_replicate]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
⊢ n • f.support.inf degt ≤ (f ^ n).support.inf degt
have refine_1 : LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt 0) : Tᵒᵈ)
  ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) 0 : Tᵒᵈ)
Tactic: refine OrderDual.ofDual_le_ofDual.mpr <| sup_support_pow_le (OrderDual.ofDual_le_ofDual.mp ?_)
      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) n f
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
refine_1 :
  LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt 0) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) 0 : Tᵒᵈ)
⊢ n • f.support.inf degt ≤ (f ^ n).support.inf degt
have refine_2 : ∀ (a b : A),
  LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt (a + b)) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt a + degt b) : Tᵒᵈ)
Tactic: refine OrderDual.ofDual_le_ofDual.mpr <| sup_support_pow_le (OrderDual.ofDual_le_ofDual.mp ?_)
      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) n 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 : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : CommSemiring R
inst_3 : AddCommMonoid A
inst_4 : AddCommMonoid B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
m : Multiset R[A]
⊢ m.prod.support.sup degb ≤ Multiset.sum (Multiset.map (fun (f : R[A]) ↦ f.support.sup degb) m)
have h : ∀ (a : List R[A]),
  (Multiset.prod (Quot.mk (⇑(List.isSetoid R[A]) : List R[A] → List R[A] → Prop) a)).support.sup degb ≤
    Multiset.sum
      (Multiset.map (fun (f : R[A]) ↦ f.support.sup degb)
        (Quot.mk (⇑(List.isSetoid R[A]) : List R[A] → List R[A] → Prop) a))
Tactic: induction m using Quot.inductionOn
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : CommSemiring R
inst_3 : AddCommMonoid A
inst_4 : AddCommMonoid B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a : List R[A]
⊢ (Multiset.prod (Quot.mk (⇑(List.isSetoid R[A]) : List R[A] → List R[A] → Prop) a)).support.sup degb ≤
    Multiset.sum
      (Multiset.map (fun (f : R[A]) ↦ f.support.sup degb)
        (Quot.mk (⇑(List.isSetoid R[A]) : List R[A] → List R[A] → Prop) a))
have h : a.prod.support.sup degb ≤ List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) a)
Tactic: rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sum_coe, Multiset.prod_coe]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : CommSemiring R
inst_3 : AddCommMonoid A
inst_4 : AddCommMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
⊢ Multiset.sum (Multiset.map (fun (f : R[A]) ↦ f.support.inf degt) m) ≤ m.prod.support.inf degt
have refine_1 : LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt 0) : Tᵒᵈ)
  ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) 0 : Tᵒᵈ)
Tactic: refine OrderDual.ofDual_le_ofDual.mpr <|
    sup_support_multiset_prod_le (OrderDual.ofDual_le_ofDual.mp ?_)
      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) m
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : CommSemiring R
inst_3 : AddCommMonoid A
inst_4 : AddCommMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
refine_1 :
  LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt 0) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) 0 : Tᵒᵈ)
⊢ Multiset.sum (Multiset.map (fun (f : R[A]) ↦ f.support.inf degt) m) ≤ m.prod.support.inf degt
have refine_2 : ∀ (a b : A),
  LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt (a + b)) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt a + degt b) : Tᵒᵈ)
Tactic: refine OrderDual.ofDual_le_ofDual.mpr <|
    sup_support_multiset_prod_le (OrderDual.ofDual_le_ofDual.mp ?_)
      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) m
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
ι : Type u_6
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : CommSemiring R
inst_3 : AddCommMonoid A
inst_4 : AddCommMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → R[A]
⊢ Eq.{u_4 + 1} (α := T) (∑ i ∈ s, (f i).support.inf degt)
    (Multiset.sum (Multiset.map (fun (f : R[A]) ↦ f.support.inf degt) (Multiset.map (fun (i : ι) ↦ f i) s.val)))
have rw : Eq.{u_4 + 1} (α := T) (∑ i ∈ s, (f i).support.inf degt)
  (Multiset.sum (Multiset.map ((fun (f : R[A]) ↦ f.support.inf degt) ∘ fun (i : ι) ↦ f i) s.val))
Tactic: rw [Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R' : Type u_2
A : Type u_3
B : Type u_5
inst : Ring R'
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
f : R'[A]
⊢ supDegree D (-f) = supDegree D f
have rw : (-f).support.sup D = supDegree D f
Tactic: rw [supDegree, supDegree, Finsupp.support_neg]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R' : Type u_2
A : Type u_3
B : Type u_5
inst : Ring R'
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
f : R'[A]
rw : (-f).support.sup D = supDegree D f
⊢ supDegree D (-f) = supDegree D f
have rw₁ : (-f).support.sup D = f.support.sup D
Tactic: rw [supDegree, supDegree, Finsupp.support_neg]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R' : Type u_2
A : Type u_3
B : Type u_5
inst : Ring R'
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
f : R'[A]
rw : (-f).support.sup D = supDegree D f
rw₁ : (-f).support.sup D = f.support.sup D
⊢ supDegree D (-f) = supDegree D f
have rw₂ : f.support.sup D = f.support.sup D
Tactic: rw [supDegree, supDegree, Finsupp.support_neg]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R' : Type u_2
A : Type u_3
B : Type u_5
inst : Ring R'
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f - g) ≤ supDegree D f ⊔ supDegree D g
have rw : supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D (-g)
Tactic: rw [sub_eq_add_neg, ← supDegree_neg (f := g)]
-- 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
a : A
r : R
hr : r ≠ 0
⊢ supDegree D (single a r) = D a
have rw : (Finsupp.support (single a r)).sup D = D a
Tactic: rw [supDegree, Finsupp.support_single a hr, Finset.sup_singleton]
-- 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
a : A
r : R
hr : r ≠ 0
rw : (Finsupp.support (single a r)).sup D = D a
⊢ supDegree D (single a r) = D a
have rw₁ : Finset.sup {a} D = D a
Tactic: rw [supDegree, Finsupp.support_single a hr, Finset.sup_singleton]
-- 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
a : A
r : R
hr : r ≠ 0
rw : (Finsupp.support (single a r)).sup D = D a
rw₁ : Finset.sup {a} D = D a
⊢ supDegree D (single a r) = D a
have rw₂ : D a = D a
Tactic: rw [supDegree, Finsupp.support_single a hr, Finset.sup_singleton]
-- 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
a : A
r : R
⊢ supDegree D (single a r) = if r = 0 then ⊥ else D a
have pos : ∀ (hr : r = 0), supDegree D (single a r) = ⊥
Tactic: split_ifs with hr
-- 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
a : A
r : R
pos : ∀ (hr : r = 0), supDegree D (single a r) = ⊥
⊢ supDegree D (single a r) = if r = 0 then ⊥ else D a
have neg : ∀ (hr : ¬r = 0), supDegree D (single a r) = D a
Tactic: split_ifs with hr
-- 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p : R[A]
a : A
hlt : ¬D a ≤ supDegree D p
⊢ Eq.{u_1 + 1} (α := R) ((p : (a : A) → R) a : R) (0 : R)
have contrapose! : ∀ (hlt : Ne.{u_1 + 1} (α := R) ((p : (a : A) → R) a : R) (0 : R)), D a ≤ supDegree D p
Tactic: contrapose! hlt
Cleared hypotheses: hlt
-- 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
s : R[A]
hs : s.support.Nonempty
⊢ s.support.sup (WithBot.some ∘ D) = (↑(s.support.sup D) : WithBot B)
have rw : (↑(s.support.sup' hs D) : WithBot B) = (↑(s.support.sup D) : WithBot B)
Tactic: rw [← Finset.coe_sup' hs, Finset.sup'_eq_sup]
-- 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
s : R[A]
hs : s.support.Nonempty
rw : (↑(s.support.sup' hs D) : WithBot B) = (↑(s.support.sup D) : WithBot B)
⊢ s.support.sup (WithBot.some ∘ D) = (↑(s.support.sup D) : WithBot B)
have rw₁ : (↑(s.support.sup D) : WithBot B) = (↑(s.support.sup D) : WithBot B)
Tactic: rw [← Finset.coe_sup' hs, Finset.sup'_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
have refine_1 : supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)
Tactic: refine s.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
refine_1 : supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)
⊢ supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
      supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ insert a s, f i) ≤ ∑ i ∈ insert a s, supDegree D (f i)
Tactic: refine s.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)
have refine_1 : (if Eq.{u_7 + 1} (α := R) 1 0 then ⊥ else D 0) ≤ 0
Tactic: rw [Finset.prod_empty, Finset.sum_empty, one_def, supDegree_single]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ (if Eq.{u_7 + 1} (α := R) 1 0 then ⊥ else D 0) ≤ 0
have pos : Eq.{u_7 + 1} (α := R) 1 0 → LE.le.{u_9} (α := B) ⊥ 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
pos : Eq.{u_7 + 1} (α := R) 1 0 → LE.le.{u_9} (α := B) ⊥ 0
⊢ (if Eq.{u_7 + 1} (α := R) 1 0 then ⊥ else D 0) ≤ 0
have neg : ¬Eq.{u_7 + 1} (α := R) 1 0 → D 0 ≤ 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s_1 : Finset ι
f : ι → R[A]
i : ι
s : Finset ι
his : i ∉ s
ih : supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
⊢ supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ insert i s, f i) ≤ ∑ i ∈ insert i s, supDegree D (f i)
have refine_2 : supDegree D (f i * ∏ x ∈ s, f x) ≤ supDegree D (f i) + ∑ x ∈ s, supDegree D (f x)
Tactic: rw [Finset.prod_insert his, Finset.sum_insert his]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
have refine_1 : supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)
Tactic: classical
  refine s.induction ?_ ?_
  · rw [Finset.prod_empty, Finset.sum_empty, one_def, supDegree_single]
    split_ifs; exacts [bot_le, hzero.le]
  · intro i s his ih
    rw [Finset.prod_insert his, Finset.sum_insert his]
    exact (supDegree_mul_le hadd).trans (by gcongr)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
refine_1 : supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)
⊢ supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
      supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ insert a s, f i) ≤ ∑ i ∈ insert a s, supDegree D (f i)
Tactic: classical
  refine s.induction ?_ ?_
  · rw [Finset.prod_empty, Finset.sum_empty, one_def, supDegree_single]
    split_ifs; exacts [bot_le, hzero.le]
  · intro i s his ih
    rw [Finset.prod_insert his, Finset.sum_insert his]
    exact (supDegree_mul_le hadd).trans (by gcongr)
-- 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
have simp_rw : (∑ x ∈ p.support,
    ∑ x_1 ∈ q.support,
      if x + x_1 = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) x : R) ((q : (a : A) → R) x_1 : R)
      else 0) =
  HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
Tactic: simp_rw [mul_apply, Finsupp.sum]
-- 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ (∑ x ∈ p.support,
      ∑ x_1 ∈ q.support,
        if x + x_1 = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) x : R) ((q : (a : A) → R) x_1 : R)
        else 0) =
    HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
have h₀ : ∀ b ∈ q.support,
  b ≠ aq →
    (if ap + b = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) b : R) else 0) =
      0
Tactic: rw [Finset.sum_eq_single ap, Finset.sum_eq_single aq, if_pos rfl]
-- 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
h₀ :
  ∀ b ∈ q.support,
    b ≠ aq →
      (if ap + b = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) b : R)
        else 0) =
        0
⊢ (∑ x ∈ p.support,
      ∑ x_1 ∈ q.support,
        if x + x_1 = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) x : R) ((q : (a : A) → R) x_1 : R)
        else 0) =
    HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
have h₁ : aq ∉ q.support →
  (if ap + aq = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R) else 0) =
    0
Tactic: rw [Finset.sum_eq_single ap, Finset.sum_eq_single aq, if_pos rfl]