case h
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ x ∈ Ico a b ∪ Ico c d ↔ x ∈ Ico (min a c) (max b d)
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
ext1 x
case h
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
case h
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ x ∈ Ico a b ∪ Ico c d ↔ x ∈ Ico (min a c) (max b d)
simp_rw [mem_union, mem_Ico, min_le_iff, lt_max_iff]
case pos
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)

case neg
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : ¬x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)

case pos
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)

case neg
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : ¬x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
case h
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
by_cases hc : c ≤ x <;> by_cases hd : x < d
no goals
case pos
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
simp only [hc, hd, and_self, or_true]
case neg
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : ¬x < d
hax : a ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
case neg
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : ¬x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
have hax : a ≤ x := h₂.trans (le_of_not_gt hd)
no goals
case neg
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : ¬x < d
hax : a ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
simp only [hax, true_and, hc, or_self]
case pos
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : x < d
hxb : x < b
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
case pos
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
no goals
case pos
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : x < d
hxb : x < b
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
simp only [hxb, and_true, hc, false_and, or_false, true_or]
no goals
case neg
α : Type u_1
β : Type ?u.114474
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : ¬x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
simp only [hc, hd, and_self, or_false]