case inl
α : Type u_1
β : Type ?u.83670
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
h : c ≤ b
⊢ Ico a b ∪ Ici c = Ici (min a c)

case inr
α : Type u_1
β : Type ?u.83670
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
h : c ≤ a
⊢ Ico a b ∪ Ici c = Ici (min a c)
α : Type u_1
β : Type ?u.83670
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
⊢ Ico a b ∪ Ici c = Ici (min a c)
cases' le_total a b with hab hab <;> simp [hab] at h
no goals
case inl
α : Type u_1
β : Type ?u.83670
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
h : c ≤ b
⊢ Ico a b ∪ Ici c = Ici (min a c)
exact Ico_union_Ici' h
no goals
case inr
α : Type u_1
β : Type ?u.83670
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
h : c ≤ a
⊢ Ico a b ∪ Ici c = Ici (min a c)
simp [*]