α : Type ?u.857372
β : Type ?u.857375
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ (⨅ (i : ι), f i + a) = ⨅ (b : ι), a + f b
α : Type ?u.857372
β : Type ?u.857375
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a + iInf f = ⨅ (b : ι), a + f b
rw [add_comm, iInf_add]
no goals
α : Type ?u.857372
β : Type ?u.857375
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ (⨅ (i : ι), f i + a) = ⨅ (b : ι), a + f b
simp [add_comm]