case h
α : Type u_1
β : Type ?u.100377
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ∈ Iic b ∪ Ioc c d ↔ x ∈ Iic (max b d)
α : Type u_1
β : Type ?u.100377
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)
ext1 x
case h
α : Type u_1
β : Type ?u.100377
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
case h
α : Type u_1
β : Type ?u.100377
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ∈ Iic b ∪ Ioc c d ↔ x ∈ Iic (max b d)
simp_rw [mem_union, mem_Iic, mem_Ioc, le_max_iff]
case pos
α : Type u_1
β : Type ?u.100377
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : c < x
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

case neg
α : Type u_1
β : Type ?u.100377
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : ¬c < x
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
case h
α : Type u_1
β : Type ?u.100377
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
by_cases hc : c < x
no goals
case pos
α : Type u_1
β : Type ?u.100377
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : c < x
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
simp only [hc, true_and]
case neg
α : Type u_1
β : Type ?u.100377
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : ¬c < x
hxb : x ≤ b
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
case neg
α : Type u_1
β : Type ?u.100377
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : ¬c < x
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
have hxb : x ≤ b := (le_of_not_gt hc).trans h₁.le
no goals
case neg
α : Type u_1
β : Type ?u.100377
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : ¬c < x
hxb : x ≤ b
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
simp only [hxb, true_or]