no goals
ι : 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
classical exact
    if H : s ∈ f.support then h s (hf H) else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)
no goals
ι : 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
exact
if H : s ∈ f.support then h s (hf H) else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)