ι : Type ?u.128088
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
ι : Type ?u.128088
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ Ico a c ⊆ Ico a b ∪ Ico b c
rw [← coe_subset, coe_union, coe_Ico, coe_Ico, coe_Ico]
no goals
ι : Type ?u.128088
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
exact Set.Ico_subset_Ico_union_Ico