[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
inst✝ : LE α
f g : ι →₀ α
h : (fun f => ↑f) f = (fun f => ↑f) g
i : ι
⊢ ↑f i = ↑g i
[PROOFSTEP]
dsimp at h 
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
inst✝ : LE α
f g : ι →₀ α
h : ↑f = ↑g
i : ι
⊢ ↑f i = ↑g i
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Zero α
inst✝¹ : DecidableEq ι
inst✝ : Lattice α
f g : ι →₀ α
⊢ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ = (↑(f.support ∪ g.support))ᶜ
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
inst✝² : Zero α
inst✝¹ : DecidableEq ι
inst✝ : Lattice α
f g : ι →₀ α
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ
[PROOFSTEP]
simp [inf_eq_and_sup_eq_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyOrderedAddMonoid α
⊢ ∀ (a : ι →₀ α), ⊥ ≤ a
[PROOFSTEP]
simp only [le_def, coe_zero, Pi.zero_apply, imp_true_iff, zero_le]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyOrderedAddMonoid α
f g : ι →₀ α
⊢ f + g = 0 ↔ f = 0 ∧ g = 0
[PROOFSTEP]
simp [FunLike.ext_iff, forall_and]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyOrderedAddMonoid α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ (i : ι), i ∈ s✝ → ↑f i ≤ ↑g i
s : ι
⊢ ↑f s ≤ ↑g s
[PROOFSTEP]
classical exact if H : s ∈ f.support then h s (hf H) else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyOrderedAddMonoid α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ (i : ι), i ∈ s✝ → ↑f i ≤ ↑g i
s : ι
⊢ ↑f s ≤ ↑g s
[PROOFSTEP]
exact if H : s ∈ f.support then h s (hf H) else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyOrderedAddMonoid α
i : ι
x : α
f : ι →₀ α
⊢ (∀ (i_1 : ι), i_1 ∈ {i} → ↑(single i x) i_1 ≤ ↑f i_1) ↔ x ≤ ↑f i
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
⊢ single i (a - b) = single i a - single i b
[PROOFSTEP]
ext j
[GOAL]
case h
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
j : ι
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
[PROOFSTEP]
obtain rfl | h := eq_or_ne i j
[GOAL]
case h.inl
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
⊢ ↑(single i (a - b)) i = ↑(single i a - single i b) i
[PROOFSTEP]
rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
[GOAL]
case h.inr
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
j : ι
h : i ≠ j
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
[PROOFSTEP]
rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
f1 f2 : ι →₀ α
⊢ (f1 - f2).support ⊆ f1.support
[PROOFSTEP]
simp (config := { contextual := true }) only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff, Ne.def, coe_tsub,
  Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
inst✝ : DecidableEq ι
f1 f2 : ι →₀ α
⊢ f1.support \ f2.support ⊆ (f1 - f2).support
[PROOFSTEP]
simp (config := { contextual := true }) [subset_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊓ g).support = f.support ∩ g.support
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support
[PROOFSTEP]
simp only [inf_apply, mem_support_iff, Ne.def, Finset.mem_union, Finset.mem_filter, Finset.mem_inter]
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ ¬↑f a✝ ⊓ ↑g a✝ = 0 ↔ ¬↑f a✝ = 0 ∧ ¬↑g a✝ = 0
[PROOFSTEP]
simp only [inf_eq_min, ← nonpos_iff_eq_zero, min_le_iff, not_or]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊔ g).support = f.support ∪ g.support
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊔ g).support ↔ a✝ ∈ f.support ∪ g.support
[PROOFSTEP]
simp only [Finset.mem_union, mem_support_iff, sup_apply, Ne.def, ← bot_eq_zero]
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ ¬↑f a✝ ⊔ ↑g a✝ = ⊥ ↔ ¬↑f a✝ = ⊥ ∨ ¬↑g a✝ = ⊥
[PROOFSTEP]
rw [_root_.sup_eq_bot_iff, not_and_or]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyLinearOrderedAddMonoid α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support
[PROOFSTEP]
classical
rw [disjoint_iff, disjoint_iff, Finsupp.bot_eq_zero, ← Finsupp.support_eq_empty, Finsupp.support_inf]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyLinearOrderedAddMonoid α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support
[PROOFSTEP]
rw [disjoint_iff, disjoint_iff, Finsupp.bot_eq_zero, ← Finsupp.support_eq_empty, Finsupp.support_inf]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyLinearOrderedAddMonoid α
f g : ι →₀ α
⊢ f.support ∩ g.support = ∅ ↔ f.support ⊓ g.support = ⊥
[PROOFSTEP]
rfl
