case intro
α : Type ?u.791480
β : Type ?u.791483
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
b : ℝ≥0
⊢ ENNReal.toReal a - ENNReal.toReal ↑b ≤ ENNReal.toReal (a - ↑b)
α : Type ?u.791480
β : Type ?u.791483
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
hb : b ≠ ⊤
⊢ ENNReal.toReal a - ENNReal.toReal b ≤ ENNReal.toReal (a - b)
lift b to ℝ≥0 using hb
case intro.top
α : Type ?u.791480
β : Type ?u.791483
a b✝ c d : ℝ≥0∞
r p q b : ℝ≥0
⊢ ENNReal.toReal ⊤ - ENNReal.toReal ↑b ≤ ENNReal.toReal (⊤ - ↑b)

case intro.coe
α : Type ?u.791480
β : Type ?u.791483
a b✝ c d : ℝ≥0∞
r p q b x✝ : ℝ≥0
⊢ ENNReal.toReal ↑x✝ - ENNReal.toReal ↑b ≤ ENNReal.toReal (↑x✝ - ↑b)
case intro
α : Type ?u.791480
β : Type ?u.791483
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
b : ℝ≥0
⊢ ENNReal.toReal a - ENNReal.toReal ↑b ≤ ENNReal.toReal (a - ↑b)
induction a using recTopCoe
no goals
case intro.top
α : Type ?u.791480
β : Type ?u.791483
a b✝ c d : ℝ≥0∞
r p q b : ℝ≥0
⊢ ENNReal.toReal ⊤ - ENNReal.toReal ↑b ≤ ENNReal.toReal (⊤ - ↑b)
simp
case intro.coe
α : Type ?u.791480
β : Type ?u.791483
a b✝ c d : ℝ≥0∞
r p q b x✝ : ℝ≥0
⊢ ↑x✝ - ↑b ≤ max (↑x✝ - ↑b) 0
case intro.coe
α : Type ?u.791480
β : Type ?u.791483
a b✝ c d : ℝ≥0∞
r p q b x✝ : ℝ≥0
⊢ ENNReal.toReal ↑x✝ - ENNReal.toReal ↑b ≤ ENNReal.toReal (↑x✝ - ↑b)
simp only [← coe_sub, NNReal.sub_def, Real.coe_toNNReal', coe_toReal]
no goals
case intro.coe
α : Type ?u.791480
β : Type ?u.791483
a b✝ c d : ℝ≥0∞
r p q b x✝ : ℝ≥0
⊢ ↑x✝ - ↑b ≤ max (↑x✝ - ↑b) 0
exact le_max_left _ _