no goals
α : Type ?u.793099
β : Type ?u.793102
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a = ⊤
⊢ ENNReal.toReal (a + b) ≤ ENNReal.toReal a + ENNReal.toReal b
simp only [ha, top_add, top_toReal, zero_add, toReal_nonneg]
no goals
α : Type ?u.793099
β : Type ?u.793102
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : ¬a = ⊤
hb : b = ⊤
⊢ ENNReal.toReal (a + b) ≤ ENNReal.toReal a + ENNReal.toReal b
simp only [hb, add_top, top_toReal, add_zero, toReal_nonneg]