no goals
α : Type ?u.859696
β : Type ?u.859699
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ (⨅ (a : ι) (a' : ι), f a + g a') = iInf f + iInf g
simp_rw [iInf_add, add_iInf]