case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
cases' lt_or_le x y with h' h'
case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ x ∈ Ico x (x + dx) \ Ico y (y + dy)
case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
use x
no goals
case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ x ∈ Ico x (x + dx) \ Ico y (y + dy)
simp [*, not_le.2 h']
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ max x (x + dy) ∈ Ico x (x + dx) \ Ico y (y + dy)
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
use max x (x + dy)
no goals
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ max x (x + dy) ∈ Ico x (x + dx) \ Ico y (y + dy)
simp [*, le_refl]