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

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

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