case inl
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + z

case inr
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + t
rcases h'.eq_or_lt with (rfl | hlt)
case inl.inl
x y : EReal
h : x < y
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
htop : ⊤ = ⊤ → ⊤ = ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤

case inl.inr
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
⊢ x + z < y + z
case inl
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + z
rcases eq_or_ne z ⊤ with (rfl | hz)
case inl.inr.intro
x y : EReal
h : x < y
z : ℝ
h' : ↑z ≤ ↑z
hbot : ↑z ≠ ⊥
htop : ↑z = ⊤ → ↑z = ⊤ → x = ⊥
hz : ↑z ≠ ⊤
⊢ x + ↑z < y + ↑z
case inl.inr
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
⊢ x + z < y + z
lift z to ℝ using ⟨hz, hbot⟩
no goals
case inl.inr.intro
x y : EReal
h : x < y
z : ℝ
h' : ↑z ≤ ↑z
hbot : ↑z ≠ ⊥
htop : ↑z = ⊤ → ↑z = ⊤ → x = ⊥
hz : ↑z ≠ ⊤
⊢ x + ↑z < y + ↑z
exact add_lt_add_right_coe h z
case inl.inl
y : EReal
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
h : ⊥ < y
htop : ⊤ = ⊤ → ⊤ = ⊤ → ⊥ = ⊥
⊢ ⊥ + ⊤ < y + ⊤
case inl.inl
x y : EReal
h : x < y
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
htop : ⊤ = ⊤ → ⊤ = ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤
obtain rfl := htop rfl rfl
no goals
case inl.inl
y : EReal
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
h : ⊥ < y
htop : ⊤ = ⊤ → ⊤ = ⊤ → ⊥ = ⊥
⊢ ⊥ + ⊤ < y + ⊤
simpa
no goals
case inr
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t
exact add_lt_add h hlt