no goals
x z : ℝ
h : ↑x + ⊤ ≤ ↑x + ↑z
⊢ ⊤ ≤ ↑z
simp only [coe_add_top, ← coe_add, top_le_iff, coe_ne_top] at h
no goals
x : ℝ
x✝ : EReal
h : ↑x + x✝ ≤ ↑x + ⊥
⊢ x✝ ≤ ⊥
simpa using h
no goals
x y z : ℝ
h : ↑x + ↑y ≤ ↑x + ↑z
⊢ ↑y ≤ ↑z
simpa only [← coe_add, EReal.coe_le_coe_iff, add_le_add_iff_left] using h