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

State before:
α : Type u_1
inst✝ : Lattice α
x y : α
⊢ uIoo x y = uIoo y x
Tactic:
rw [uIoo, uIoo, inf_comm, sup_comm]
State after:
no goals