case intro
α : Type ?u.789991
β : Type ?u.789994
b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
a : ℝ≥0
⊢ ENNReal.toReal (↑a + b) = ENNReal.toReal ↑a + ENNReal.toReal b
α : Type ?u.789991
β : Type ?u.789994
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ ENNReal.toReal (a + b) = ENNReal.toReal a + ENNReal.toReal b
lift a to ℝ≥0 using ha
case intro.intro
α : Type ?u.789991
β : Type ?u.789994
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal (↑a + ↑b) = ENNReal.toReal ↑a + ENNReal.toReal ↑b
case intro
α : Type ?u.789991
β : Type ?u.789994
b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
a : ℝ≥0
⊢ ENNReal.toReal (↑a + b) = ENNReal.toReal ↑a + ENNReal.toReal b
lift b to ℝ≥0 using hb
no goals
case intro.intro
α : Type ?u.789991
β : Type ?u.789994
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal (↑a + ↑b) = ENNReal.toReal ↑a + ENNReal.toReal ↑b
rfl