no goals
α : Type ?u.801740
β : Type ?u.801743
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
hr : a ≠ ⊤
hp : b ≠ ⊤
h : a ≤ b
⊢ ENNReal.toReal (min a b) = min (ENNReal.toReal a) (ENNReal.toReal b)
simp only [h, (ENNReal.toReal_le_toReal hr hp).2 h, min_eq_left]
no goals
α : Type ?u.801740
β : Type ?u.801743
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
hr : a ≠ ⊤
hp : b ≠ ⊤
h : b ≤ a
⊢ ENNReal.toReal (min a b) = min (ENNReal.toReal a) (ENNReal.toReal b)
simp only [h, (ENNReal.toReal_le_toReal hp hr).2 h, min_eq_right]