α : Type ?u.797651
β : Type ?u.797654
a b c d : ℝ≥0∞
r p q : ℝ≥0
hle : a ≤ b + c
hb : b = ⊤ → a = ⊤
hc : c = ⊤ → a = ⊤
⊢ b + c = ⊤ → a = ⊤
α : Type ?u.797651
β : Type ?u.797654
a b c d : ℝ≥0∞
r p q : ℝ≥0
hle : a ≤ b + c
hb : b = ⊤ → a = ⊤
hc : c = ⊤ → a = ⊤
⊢ ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c
refine le_trans (toReal_mono' hle ?_) toReal_add_le
no goals
α : Type ?u.797651
β : Type ?u.797654
a b c d : ℝ≥0∞
r p q : ℝ≥0
hle : a ≤ b + c
hb : b = ⊤ → a = ⊤
hc : c = ⊤ → a = ⊤
⊢ b + c = ⊤ → a = ⊤
simpa only [add_eq_top, or_imp] using And.intro hb hc