awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : AddZeroClass M
a b : α →₀ M
i j : M
val : α
⊢ Eq.{u_2 + 1} (α := M) ((optionElim (i + j) (a + b) : (a : Option α) → M) (Option.some val) : M)
    ((optionElim i a + optionElim j b : (a : Option α) → M) (Option.some val) : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedAddMonoid β
f : ι →₀ α
h₁ h₂ : ι → α → β
h : ∀ i ∈ f.support, h₁ i ((f : (a : ι) → α) i) ≤ h₂ i ((f : (a : ι) → α) i)
⊢ f.sum h₁ ≤ f.sum h₂

Tactic:
Finset.sum_le_sum h

Premises used: Finsupp.sum, Finset.sum_le_sum
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedAddMonoid β
f : ι →₀ α
h₁ : ι → α → β
h : ∀ i ∈ f.support, 0 ≤ h₁ i ((f : (a : ι) → α) i)
⊢ 0 ≤ f.sum h₁

Tactic:
Finset.sum_nonneg h

Premises used: Finsupp.sum, Finset.sum_nonneg
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedAddMonoid β
f : ι →₀ α
h₁ : ι → α → β
h : ∀ (i : ι), 0 ≤ h₁ i ((f : (a : ι) → α) i)
⊢ 0 ≤ f.sum h₁

Tactic:
sum_nonneg fun _ _ ↦ h _

Premises used: Finsupp.sum_nonneg
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedAddMonoid β
f : ι →₀ α
h₁ : ι → α → β
h : ∀ i ∈ f.support, h₁ i ((f : (a : ι) → α) i) ≤ 0
⊢ f.sum h₁ ≤ 0

Tactic:
Finset.sum_nonpos h

Premises used: Finsupp.sum, Finset.sum_nonpos
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedCancelAddMonoid β
inst_4 : AddLeftStrictMono β
f : ι →₀ α
g : ι → α → β
h : ∀ i ∈ f.support, 0 < g i ((f : (a : ι) → α) i)
hf : f ≠ 0
⊢ f.support.Nonempty

Tactic:
simpa
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedCancelAddMonoid β
inst_4 : AddLeftStrictMono β
f : ι →₀ α
g : ι → α → β
h : ∀ i ∈ f.support, 0 ≤ g i ((f : (a : ι) → α) i)
hf : ∃ i ∈ f.support, 0 < g i ((f : (a : ι) → α) i)
⊢ 0 < f.sum g

Tactic:
Finset.sum_pos' h hf

Premises used: Finset.sum_pos', Finsupp.sum
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : Zero α
inst_1 : Preorder α
i : ι
a b : α
⊢ LE.le (α := ι →₀ α) (single i a) (single i b) ↔ a ≤ b

Tactic:
Pi.single_le_single

Premises used: Function.update, Pi.single, dite, Pi.single_le_single
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : Zero α
inst_1 : Preorder α
i : ι
a b : α
⊢ LE.le (α := ι →₀ α) (single i a) (single i b) ↔ a ≤ b

Tactic:
exact Pi.single_le_single

Premises used: Pi.single_le_single
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : Zero α
inst_1 : Preorder α
i : ι
a b : α
⊢ LE.le (α := ι →₀ α) (single i a) (single i b) ↔ a ≤ b

Tactic:
classical exact Pi.single_le_single

Premises used: Pi.single_le_single
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : Zero α
inst_1 : Preorder α
i : ι
⊢ Monotone (α := α) (β := ι →₀ α) (single i)

Tactic:
fun _ _ ↦ single_le_single.2

Premises used: Iff.mpr, Monotone, Finsupp.single_le_single
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : Zero α
inst_1 : Preorder α
i : ι
a : α
⊢ LE.le (α := ι →₀ α) 0 (single i a) ↔ 0 ≤ a

Tactic:
Pi.single_nonneg

Premises used: Function.update, Pi.single, dite, Pi.single_nonneg
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : Zero α
inst_1 : Preorder α
i : ι
a : α
⊢ LE.le (α := ι →₀ α) 0 (single i a) ↔ 0 ≤ a

Tactic:
exact Pi.single_nonneg

Premises used: Pi.single_nonneg
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : Zero α
inst_1 : Preorder α
i : ι
a : α
⊢ LE.le (α := ι →₀ α) 0 (single i a) ↔ 0 ≤ a

Tactic:
classical exact Pi.single_nonneg

Premises used: Pi.single_nonneg
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : Zero α
inst_1 : Preorder α
i : ι
a : α
⊢ LE.le (α := ι →₀ α) (single i a) 0 ↔ a ≤ 0

Tactic:
Pi.single_nonpos

Premises used: Function.update, Pi.single_nonpos, Pi.single, dite
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : Zero α
inst_1 : Preorder α
i : ι
a : α
⊢ LE.le (α := ι →₀ α) (single i a) 0 ↔ a ≤ 0

Tactic:
exact Pi.single_nonpos

Premises used: Pi.single_nonpos
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : Zero α
inst_1 : Preorder α
i : ι
a : α
⊢ LE.le (α := ι →₀ α) (single i a) 0 ↔ a ≤ 0

Tactic:
classical exact Pi.single_nonpos

Premises used: Pi.single_nonpos
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
rw :
  LE.le.{u_4} (α := β) (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₁ : (a : ι) → α) x))
    (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₂ : (a : ι) → α) x))
⊢ f₁.sum h ≤ f₂.sum h

Tactic:
rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀,
    sum_of_support_subset _ Finset.subset_union_right _ hh₀]

Premises used: Finset.subset_union_left, Finset.subset_union_right, Finsupp.sum_of_support_subset
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
h₁ : ∀ (i : ι) (hi : i ∈ f₁.support ∪ f₂.support), h i ((f₁ : (a : ι) → α) i) ≤ h i ((f₂ : (a : ι) → α) i)
⊢ LE.le.{u_4} (α := β) (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₁ : (a : ι) → α) x))
    (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₂ : (a : ι) → α) x))

Tactic:
gcongr with i hi
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
i : ι
hi : i ∈ f₁.support ∪ f₂.support
⊢ h i ((f₁ : (a : ι) → α) i) ≤ h i ((f₂ : (a : ι) → α) i)

Tactic:
hh _ hi <| hf _
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
i : ι
hi : i ∈ f₁.support ∪ f₂.support
⊢ h i ((f₁ : (a : ι) → α) i) ≤ h i ((f₂ : (a : ι) → α) i)

Tactic:
exact hh _ hi <| hf _
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
rw : ∑ x ∈ f₁.support ∪ f₂.support, h x ((f₁ : (a : ι) → α) x) ≤ f₂.sum h
rw₁ rw₂ rw₃ :
  LE.le.{u_4} (α := β) (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₁ : (a : ι) → α) x))
    (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₂ : (a : ι) → α) x))
h₁ : ∀ (i : ι) (hi : i ∈ f₁.support ∪ f₂.support), h i ((f₁ : (a : ι) → α) i) ≤ h i ((f₂ : (a : ι) → α) i)
⊢ f₁.sum h ≤ f₂.sum h

Tactic:
classical
  rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀,
    sum_of_support_subset _ Finset.subset_union_right _ hh₀]
  gcongr with i hi
  exact hh _ hi <| hf _

Premises used: Finset.subset_union_left, Finset.subset_union_right, Finsupp.sum_of_support_subset
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : Zero α
inst_1 : LE α
inst_2 : Std.Refl fun (x1 x2 : α) ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
mp : embDomain f g₁ ≤ embDomain f g₂ → g₁ ≤ g₂
mpr : g₁ ≤ g₂ → embDomain f g₁ ≤ embDomain f g₂
⊢ embDomain f g₁ ≤ embDomain f g₂ ↔ g₁ ≤ g₂

Tactic:
constructor
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : Zero α
inst_1 : LE α
inst_2 : Std.Refl fun (x1 x2 : α) ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
h' : ∀ (i : κ), LE.le.{u_3} (α := α) ((embDomain f g₁ : (a : κ) → α) i : α) ((embDomain f g₂ : (a : κ) → α) i : α)
x : ι
⊢ LE.le.{u_3} (α := α) ((g₁ : (a : ι) → α) x : α) ((g₂ : (a : ι) → α) x : α)

Tactic:
simpa [Finsupp.embDomain_apply] using h' (f x)

Premises used: Finsupp.embDomain_apply, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : Zero α
inst_1 : LE α
inst_2 : Std.Refl fun (x1 x2 : α) ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
h : g₁ ≤ g₂
⊢ embDomain f g₁ ≤ embDomain f g₂

Tactic:
simp [Finsupp.le_def, embDomain_apply, apply_dite₂, Finsupp.le_def.mp h]

Premises used: Finsupp.embDomain_apply, Finsupp.le_def, Iff.mp, apply_dite₂
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : Zero α
inst_1 : Preorder α
f : ι ↪ κ
⊢ Monotone (α := ι →₀ α) (embDomain f)

Tactic:
fun _ _ ↦ (embDomain_le_embDomain_iff_le f _ _).mpr

Premises used: Iff.mpr, Monotone, Finsupp.embDomain_le_embDomain_iff_le
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : Zero α
inst_1 : Preorder α
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ embDomain f g₁ < embDomain f g₂ ↔ g₁ < g₂

Tactic:
simp [lt_iff_le_not_ge, embDomain_le_embDomain_iff_le]

Premises used: lt_iff_le_not_ge, Finsupp.embDomain_le_embDomain_iff_le
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : LE α
inst_2 : Std.Refl fun (x1 x2 : α) ↦ x1 ≤ x2
f : ι → κ
h : Function.Injective f
g₁ g₂ : ι →₀ α
⊢ mapDomain f g₁ ≤ mapDomain f g₂ ↔ g₁ ≤ g₂

Tactic:
simpa [Finsupp.embDomain_eq_mapDomain] using Finsupp.embDomain_le_embDomain_iff_le ⟨f, h⟩ g₁ g₂

Premises used: Function.Embedding.mk, Finsupp.embDomain_eq_mapDomain, Finsupp.embDomain_le_embDomain_iff_le
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : Preorder α
f : ι → κ
h : Function.Injective f
g₁ g₂ : ι →₀ α
⊢ mapDomain f g₁ < mapDomain f g₂ ↔ g₁ < g₂

Tactic:
simpa [Finsupp.embDomain_eq_mapDomain] using Finsupp.embDomain_lt_embDomain_iff_lt ⟨f, h⟩ g₁ g₂

Premises used: Function.Embedding.mk, Finsupp.embDomain_lt_embDomain_iff_lt, Finsupp.embDomain_eq_mapDomain
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst : AddCommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedAddMonoid α
i : ι
f : ι → κ
g g₁ g₂ : ι →₀ α
⊢ IsOrderedAddMonoid (ι →₀ α)

Tactic:
{ add_le_add_left := fun _a _b h c s => add_le_add_left (h s) (c s) }

Premises used: add_le_add_left, IsOrderedAddMonoid._proof_1, DFunLike.coe, Finsupp, IsOrderedAddMonoid.mk
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedAddMonoid α
f : ι → κ
g₁ g₂ : ι →₀ α
h : g₁ ≤ g₂
⊢ ∀ i ∈ g₁.support ∪ g₂.support, Eq (α := κ →₀ α) (single (f i) 0) 0

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedAddMonoid α
f : ι → κ
⊢ Monotone (α := ι →₀ α) (mapDomain f)

Tactic:
exact fun g₁ g₂ h ↦ sum_le_sum_index h (fun _ _ ↦ single_mono) (by simp)

Premises used: Finsupp.single_mono, Finsupp.sum_le_sum_index
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedAddMonoid α
f : ι → κ
⊢ Monotone (α := ι →₀ α) (mapDomain f)

Tactic:
classical exact fun g₁ g₂ h ↦ sum_le_sum_index h (fun _ _ ↦ single_mono) (by simp)

Premises used: Finsupp.single_mono, Finsupp.sum_le_sum_index
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : 0 ≤ g
⊢ 0 ≤ mapDomain f g

Tactic:
simpa using mapDomain_mono hg

Premises used: Finsupp.mapDomain_mono
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : g ≤ 0
⊢ mapDomain f g ≤ 0

Tactic:
simpa using mapDomain_mono hg

Premises used: Finsupp.mapDomain_mono
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
inl : ∀ (H : Eq.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)), sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g
inr : ∀ (H : Ne.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)), sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g
⊢ sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g

Tactic:
rcases eq_or_ne (f a) 0 with H | H

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
H : Eq.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
inl : 0 ≤ f.sum g
⊢ sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g

Tactic:
rw [H, single_zero, sum_zero_index]

Premises used: Finsupp.sum_zero_index, Finsupp.single_zero
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
H : Eq.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ 0 ≤ f.sum g

Tactic:
sum_nonneg' (fun i ↦ h i (f i))

Premises used: Finsupp.sum_nonneg', DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
H : Eq.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ 0 ≤ f.sum g

Tactic:
exact sum_nonneg' (fun i ↦ h i (f i))

Premises used: Finsupp.sum_nonneg', DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
H : Ne.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
inr : g a ((f : (a : α) → M) a) ≤ f.sum g
⊢ sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g

Tactic:
rw [sum, support_single _ H, sum_singleton, single_eq_same]

Premises used: Finsupp.support_single, Finsupp.single_eq_same, Finsupp.sum, Finset.sum_singleton
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
H : Ne.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
inr : a ∈ f.support
⊢ g a ((f : (a : α) → M) a) ≤ f.sum g

Tactic:
apply Finset.single_le_sum (fun i hi ↦ h i (f i))

Premises used: Finset.single_le_sum, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
H : Ne.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ a ∈ f.support

Tactic:
simpa [mem_support_iff, ne_eq] using H

Premises used: Finsupp.mem_support_iff, ne_eq
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : M → N
hg : g 0 = 0
h : LE.le (α := M → N) 0 fun (x : M) ↦ g x
a : α
simp :
  LE.le.{u_7} (α := N)
    (sum.{u_5, u_6, u_7} (M := M) (single a ((f : (a : α) → M) a) : α →₀ M) fun (x : α) (m : M) ↦ g m)
    (f.sum fun (x : α) (m : M) ↦ g m)
⊢ g ((f : (a : α) → M) a) ≤ f.sum fun (x : α) (m : M) ↦ g m

Tactic:
simp only [← sum_single_index (h := fun (_ : α) m ↦ g m) (a := a) (b := f a) hg]

Premises used: Finsupp.sum_single_index
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : M → N
hg : g 0 = 0
h : LE.le (α := M → N) 0 fun (x : M) ↦ g x
a : α
⊢ LE.le.{u_7} (α := N)
    (sum.{u_5, u_6, u_7} (M := M) (single a ((f : (a : α) → M) a) : α →₀ M) fun (x : α) (m : M) ↦ g m)
    (f.sum fun (x : α) (m : M) ↦ g m)

Tactic:
apply single_le_sum _ (fun _ m ↦ h m)

Premises used: Finsupp.single_le_sum
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst : AddCommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelAddMonoid α
⊢ IsOrderedCancelAddMonoid (ι →₀ α)

Tactic:
{ le_of_add_le_add_left := fun _f _g _i h s => le_of_add_le_add_left (h s) }

Premises used: le_of_add_le_add_left, IsOrderedCancelAddMonoid.mk, IsOrderedCancelAddMonoid._proof_1, Finsupp
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : Zero β
inst_3 : Preorder β
inst_4 : SMulZeroClass α β
inst_5 : PosSMulMono α β
⊢ PosSMulMono α (ι →₀ β)

Tactic:
PosSMulMono.lift _ coe_le_coe coe_smul

Premises used: PosSMulMono.lift, Finsupp.coe_smul
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : Zero β
inst_3 : Preorder β
inst_4 : SMulZeroClass α β
inst_5 : SMulPosMono α β
⊢ SMulPosMono α (ι →₀ β)

Tactic:
SMulPosMono.lift _ coe_le_coe coe_smul coe_zero

Premises used: SMulPosMono.lift, Finsupp.coe_smul, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : Zero β
inst_3 : Preorder β
inst_4 : SMulZeroClass α β
inst_5 : PosSMulReflectLE α β
⊢ PosSMulReflectLE α (ι →₀ β)

Tactic:
PosSMulReflectLE.lift _ coe_le_coe coe_smul

Premises used: Finsupp.coe_smul, PosSMulReflectLE.lift
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : Zero β
inst_3 : Preorder β
inst_4 : SMulZeroClass α β
inst_5 : SMulPosReflectLE α β
⊢ SMulPosReflectLE α (ι →₀ β)

Tactic:
SMulPosReflectLE.lift _ coe_le_coe coe_smul coe_zero

Premises used: SMulPosReflectLE.lift, Finsupp.coe_smul, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : PartialOrder α
inst_2 : Zero β
inst_3 : PartialOrder β
inst_4 : SMulWithZero α β
inst_5 : PosSMulStrictMono α β
⊢ PosSMulStrictMono α (ι →₀ β)

Tactic:
PosSMulStrictMono.lift _ coe_le_coe coe_smul

Premises used: PosSMulStrictMono.lift, Finsupp.coe_smul
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : PartialOrder α
inst_2 : Zero β
inst_3 : PartialOrder β
inst_4 : SMulWithZero α β
inst_5 : SMulPosStrictMono α β
⊢ SMulPosStrictMono α (ι →₀ β)

Tactic:
SMulPosStrictMono.lift _ coe_le_coe coe_smul coe_zero

Premises used: SMulPosStrictMono.lift, Finsupp.coe_smul, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : PartialOrder α
inst_2 : Zero β
inst_3 : PartialOrder β
inst_4 : SMulWithZero α β
inst_5 : SMulPosReflectLT α β
⊢ SMulPosReflectLT α (ι →₀ β)

Tactic:
SMulPosReflectLT.lift _ coe_le_coe coe_smul coe_zero

Premises used: SMulPosReflectLT.lift, Finsupp.coe_smul, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
f g : ι →₀ α
inst_2 : IsBotZeroClass α
⊢ ∀ (a : ι →₀ α), 0 ≤ a

Tactic:
simp [le_def]

Premises used: Finsupp.le_def
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsBotZeroClass α
⊢ Eq (α := ι →₀ α) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
⊢ f + g = 0 ↔ f = 0 ∧ g = 0

Tactic:
simp [DFunLike.ext_iff, forall_and]

Premises used: DFunLike.ext_iff, forall_and
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
s : Finset ι
hf : f.support ⊆ s
⊢ f ≤ g ↔ ∀ i ∈ s, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)

Tactic:
⟨fun h s _ ↦ h s, fun h s ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
s : Finset ι
hf : f.support ⊆ s
refine :
  ∀ (h : ∀ i ∈ s, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)) (s : ι),
    LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)
⊢ f ≤ g ↔ ∀ i ∈ s, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)

Tactic:
refine ⟨fun h s _ ↦ h s, fun h s ↦ ?_⟩
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
s_1 : Finset ι
hf : f.support ⊆ s_1
h : ∀ i ∈ s_1, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)
s : ι
pos : ∀ (H : s ∈ f.support), LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)
neg : ∀ (H : s ∉ f.support), LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)
⊢ LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)

Tactic:
by_cases H : s ∈ f.support

Premises used: Finsupp.support
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
s_1 : Finset ι
hf : f.support ⊆ s_1
h : ∀ i ∈ s_1, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)
s : ι
H : s ∈ f.support
⊢ LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)

Tactic:
h s (hf H)
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
s_1 : Finset ι
hf : f.support ⊆ s_1
h : ∀ i ∈ s_1, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)
s : ι
H : s ∈ f.support
⊢ LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)

Tactic:
exact h s (hf H)
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
s_1 : Finset ι
hf : f.support ⊆ s_1
h : ∀ i ∈ s_1, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)
s : ι
H : s ∉ f.support
⊢ LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)

Tactic:
notMem_support_iff.1 H ▸ zero_le

Premises used: zero_le, Finsupp.notMem_support_iff, Eq.rec, Iff.mp, Eq.symm