case inl
α : Type u_1
β : Type ?u.106002
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : c ≤ d
h : c < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)

case inr
α : Type u_1
β : Type ?u.106002
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
α : Type u_1
β : Type ?u.106002
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
cases' le_total c d with hcd hcd <;> simp [hcd] at h
no goals
case inl
α : Type u_1
β : Type ?u.106002
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : c ≤ d
h : c < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
exact Iio_union_Ioo' h
case inr
α : Type u_1
β : Type ?u.106002
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (max d b)
case inr
α : Type u_1
β : Type ?u.106002
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
rw [max_comm]
no goals
case inr
α : Type u_1
β : Type ?u.106002
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (max d b)
simp [*, max_eq_right_of_lt h]