no goals
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
s : Finset ι
i : ι
a : α i
⊢ (∀ (i_1 : ι), i_1 ∈ {i} → ↑(single i a) i_1 ≤ ↑f i_1) ↔ a ≤ ↑f i
simp