-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_union_Ioo' (h₁ : c < b) (h₂ : a < d) : Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a 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)

Tactic:
simp only [hxb, and_true, hc, false_and, or_false, true_or]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a 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)

Tactic:
simp only [hax, true_and, hc, or_self]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a 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)

Tactic:
by_cases hc : c < x <;> by_cases hd : x < d

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
a 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
inst✝ : LinearOrder α
a 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
inst✝ : LinearOrder α
a 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
inst✝ : LinearOrder α
a 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)

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : c < b
h₂ : a < d
x : α
⊢ x ∈ Ioo a b ∪ Ioo c d ↔ x ∈ Ioo (a ⊓ c) (b ⊔ d)

Tactic:
simp_rw [mem_union, mem_Ioo, min_lt_iff, lt_max_iff]

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a 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)

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a 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)

Tactic:
simp only [hc, hd, and_self, or_true]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a 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)

Tactic:
have hxb : x < b := (le_of_not_lt hc).trans_lt h₁

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
a 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)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : c < b
h₂ : a < d
⊢ Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (b ⊔ d)

Tactic:
ext1 x

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : c < b
h₂ : a < d
x : α
⊢ x ∈ Ioo a b ∪ Ioo c d ↔ x ∈ Ioo (a ⊓ c) (b ⊔ d)

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a 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)

Tactic:
simp only [hc, hd, and_self, or_false]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a 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)

Tactic:
have hax : a < x := h₂.trans_le (le_of_not_lt hd)

Result:
case neg
α : Type u_1
inst✝ : LinearOrder α
a 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)