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

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

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

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

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

case inr.inr
α : Type u_1
β : Type ?u.116141
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
all_goals simp [*]
no goals
case inl.inl
α : Type u_1
β : Type ?u.116141
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a ≤ d
h₂ : c ≤ b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
exact Ico_union_Ico' h₂ h₁
no goals
case inr.inr
α : Type u_1
β : Type ?u.116141
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
simp [*]