Theorem: uIoo_eq_uIcc_sdiff_ends (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ uIoo a b = uIcc a b \ {a, b}
Tactic:
cases le_total a b
State after:
case inl
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
h✝ : a ≤ b
⊢ uIoo a b = uIcc a b \ {a, b}

case inr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
h✝ : b ≤ a
⊢ uIoo a b = uIcc a b \ {a, b}

State before:
case inl
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
h✝ : a ≤ b
⊢ uIoo a b = uIcc a b \ {a, b}
Tactic:
simp [uIoo, uIcc, *]
State after:
no goals

State before:
case inr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
h✝ : b ≤ a
⊢ uIoo a b = uIcc a b \ {a, b}
Tactic:
simp [uIoo, uIcc, *, pair_comm a b]
State after:
no goals