case h
α : Type u_1
β : Type ?u.77673
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ∈ Ioo a b ∪ Ioi c ↔ x ∈ Ioi (min a c)
α : Type u_1
β : Type ?u.77673
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
ext1 x
case h
α : Type u_1
β : Type ?u.77673
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x
case h
α : Type u_1
β : Type ?u.77673
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ∈ Ioo a b ∪ Ioi c ↔ x ∈ Ioi (min a c)
simp_rw [mem_union, mem_Ioo, mem_Ioi, min_lt_iff]
case pos
α : Type u_1
β : Type ?u.77673
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : c < x
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x

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