case intro
α : Type ?u.790750
β : Type ?u.790753
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
ha : a ≠ ⊤
b : ℝ≥0
h : ↑b ≤ a
⊢ ENNReal.toReal (a - ↑b) = ENNReal.toReal a - ENNReal.toReal ↑b
α : Type ?u.790750
β : Type ?u.790753
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : b ≤ a
ha : a ≠ ⊤
⊢ ENNReal.toReal (a - b) = ENNReal.toReal a - ENNReal.toReal b
lift b to ℝ≥0 using ne_top_of_le_ne_top ha h
case intro.intro
α : Type ?u.790750
β : Type ?u.790753
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑b ≤ ↑a
⊢ ENNReal.toReal (↑a - ↑b) = ENNReal.toReal ↑a - ENNReal.toReal ↑b
case intro
α : Type ?u.790750
β : Type ?u.790753
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
ha : a ≠ ⊤
b : ℝ≥0
h : ↑b ≤ a
⊢ ENNReal.toReal (a - ↑b) = ENNReal.toReal a - ENNReal.toReal ↑b
lift a to ℝ≥0 using ha
no goals
case intro.intro
α : Type ?u.790750
β : Type ?u.790753
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑b ≤ ↑a
⊢ ENNReal.toReal (↑a - ↑b) = ENNReal.toReal ↑a - ENNReal.toReal ↑b
simp only [← ENNReal.coe_sub, ENNReal.coe_toReal, NNReal.coe_sub (ENNReal.coe_le_coe.mp h)]