Theorem: uIoo_of_le (ExponentialRamsey/Prereq/Mathlib/Analysis/Calculus/Taylor.lean)

State before:
α : Type u_1
inst✝ : Lattice α
x y : α
h : x ≤ y
⊢ uIoo x y = Ioo x y
Tactic:
rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]
State after:
no goals