no goals
α : Type ?u.801082
β : Type ?u.801085
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : a ≠ ⊤
hp : b ≠ ⊤
h : a ≤ b
⊢ ENNReal.toReal (max a b) = max (ENNReal.toReal a) (ENNReal.toReal b)
simp only [h, (ENNReal.toReal_le_toReal hr hp).2 h, max_eq_right]
no goals
α : Type ?u.801082
β : Type ?u.801085
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : a ≠ ⊤
hp : b ≠ ⊤
h : b ≤ a
⊢ ENNReal.toReal (max a b) = max (ENNReal.toReal a) (ENNReal.toReal b)
simp only [h, (ENNReal.toReal_le_toReal hp hr).2 h, max_eq_left]