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

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

case inr.inr
α : Type u_1
β : Type ?u.92706
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
case inr
α : Type u_1
β : Type ?u.92706
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ a ∨ c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
cases' h with h h
no goals
case inr.inl
α : Type u_1
β : Type ?u.92706
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ a
⊢ Icc a b ∪ Ici c = Ici (min a c)
simp [*]
case inr.inr
α : Type u_1
β : Type ?u.92706
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ b
hca : c ≤ a
⊢ Icc a b ∪ Ici c = Ici (min a c)
case inr.inr
α : Type u_1
β : Type ?u.92706
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
have hca : c ≤ a := h.trans hab.le
no goals
case inr.inr
α : Type u_1
β : Type ?u.92706
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ b
hca : c ≤ a
⊢ Icc a b ∪ Ici c = Ici (min a c)
simp [*]