[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a < x ∧ x < b)
⊢ Decidable (x ∈ Ioo a b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a ≤ x ∧ x < b)
⊢ Decidable (x ∈ Ico a b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (x < b)
⊢ Decidable (x ∈ Iio b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a ≤ x ∧ x ≤ b)
⊢ Decidable (x ∈ Icc a b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (x ≤ b)
⊢ Decidable (x ∈ Iic b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a < x ∧ x ≤ b)
⊢ Decidable (x ∈ Ioc a b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a ≤ x)
⊢ Decidable (x ∈ Ici a)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a < x)
⊢ Decidable (x ∈ Ioi a)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ioo a b ↔ False
[PROOFSTEP]
simp [lt_irrefl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ico a b ↔ a < b
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Icc a b ↔ a ≤ b
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ioc a b ↔ False
[PROOFSTEP]
simp [lt_irrefl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ici a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ioo a b ↔ False
[PROOFSTEP]
simp [lt_irrefl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ico a b ↔ False
[PROOFSTEP]
simp [lt_irrefl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Icc a b ↔ a ≤ b
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ioc a b ↔ a < b
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Iic a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Icc a b = ∅ ↔ ¬a ≤ b
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Icc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ico a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ico]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ioc a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioo]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a✝ b c a : α
⊢ ∀ (x : α), x ∈ Icc a a ↔ x ∈ {a}
[PROOFSTEP]
simp [Icc, le_antisymm_iff, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
⊢ a = c ∧ b = c
[PROOFSTEP]
have hab : a ≤ b := nonempty_Icc.1 (h.symm.subst <| singleton_nonempty c)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
hab : a ≤ b
⊢ a = c ∧ b = c
[PROOFSTEP]
exact ⟨eq_of_mem_singleton <| h.subst <| left_mem_Icc.2 hab, eq_of_mem_singleton <| h.subst <| right_mem_Icc.2 hab⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case refine'_2.intro
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
b : α
⊢ Icc b b = {b}
[PROOFSTEP]
exact Icc_self _
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α✝
a✝ b✝ c : α✝
α : Type u_3
inst✝ : LinearOrder α
a b : α
⊢ Set.Subsingleton (Icc a b) ↔ b ≤ a
[PROOFSTEP]
refine' ⟨fun h ↦ _, subsingleton_Icc_of_ge⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α✝
a✝ b✝ c : α✝
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : Set.Subsingleton (Icc a b)
⊢ b ≤ a
[PROOFSTEP]
contrapose! h
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α✝
a✝ b✝ c : α✝
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ¬Set.Subsingleton (Icc a b)
[PROOFSTEP]
simp only [ge_iff_le, gt_iff_lt, not_subsingleton_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α✝
a✝ b✝ c : α✝
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ Set.Nontrivial (Icc a b)
[PROOFSTEP]
exact ⟨a, ⟨le_refl _, h.le⟩, b, ⟨h.le, le_refl _⟩, h.ne⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Icc a b \ {a} ↔ x ∈ Ioc a b
[PROOFSTEP]
simp [lt_iff_le_and_ne, eq_comm, and_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Icc a b \ {b} ↔ x ∈ Ico a b
[PROOFSTEP]
simp [lt_iff_le_and_ne, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Ico a b \ {a} ↔ x ∈ Ioo a b
[PROOFSTEP]
simp [and_right_comm, ← lt_iff_le_and_ne, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Ioc a b \ {b} ↔ x ∈ Ioo a b
[PROOFSTEP]
simp [and_assoc, ← lt_iff_le_and_ne]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
⊢ Icc a b \ {a, b} = Ioo a b
[PROOFSTEP]
rw [insert_eq, ← diff_diff, Icc_diff_left, Ioc_diff_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Ici a \ {a} ↔ x ∈ Ioi a
[PROOFSTEP]
simp [lt_iff_le_and_ne, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Iic a \ {a} ↔ x ∈ Iio a
[PROOFSTEP]
simp [lt_iff_le_and_ne]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a < b
⊢ Ico a b \ Ioo a b = {a}
[PROOFSTEP]
rw [← Ico_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Ico.2 h)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a < b
⊢ Ioc a b \ Ioo a b = {b}
[PROOFSTEP]
rw [← Ioc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 <| right_mem_Ioc.2 h)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ Icc a b \ Ico a b = {b}
[PROOFSTEP]
rw [← Icc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 <| right_mem_Icc.2 h)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ Icc a b \ Ioc a b = {a}
[PROOFSTEP]
rw [← Icc_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Icc.2 h)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ Icc a b \ Ioo a b = {a, b}
[PROOFSTEP]
rw [← Icc_diff_both, diff_diff_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ {a, b} ⊆ Icc a b
[PROOFSTEP]
simp [insert_subset_iff, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
⊢ Ici a \ Ioi a = {a}
[PROOFSTEP]
rw [← Ici_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 left_mem_Ici)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
⊢ Iic a \ Iio a = {a}
[PROOFSTEP]
rw [← Iic_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 right_mem_Iic)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Ioi a ∪ {a} ↔ x ∈ Ici a
[PROOFSTEP]
simp [eq_comm, le_iff_eq_or_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
hab : a < b
⊢ Ioo a b ∪ {a} = Ico a b
[PROOFSTEP]
rw [← Ico_diff_left, diff_union_self, union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
hab : a < b
⊢ Ioo a b ∪ {b} = Ioc a b
[PROOFSTEP]
simpa only [dual_Ioo, dual_Ico] using Ioo_union_left hab.dual
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
⊢ Ioc a b ∪ {a} = Icc a b
[PROOFSTEP]
rw [← Icc_diff_left, diff_union_self, union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Icc.2 hab)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
⊢ Ico a b ∪ {b} = Icc a b
[PROOFSTEP]
simpa only [dual_Ioc, dual_Icc] using Ioc_union_left hab.dual
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b
[PROOFSTEP]
rw [insert_eq, union_comm, Ico_union_right h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ insert a (Ioc a b) = Icc a b
[PROOFSTEP]
rw [insert_eq, union_comm, Ioc_union_left h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a < b
⊢ insert a (Ioo a b) = Ico a b
[PROOFSTEP]
rw [insert_eq, union_comm, Ioo_union_left h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a < b
⊢ insert b (Ioo a b) = Ioc a b
[PROOFSTEP]
rw [insert_eq, union_comm, Ioo_union_right h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioi a ⊆ s
hc : s ⊆ Ici a
h : a ∈ s
⊢ Ici a ⊆ s
[PROOFSTEP]
rw [← Ioi_union_left, union_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioi a ⊆ s
hc : s ⊆ Ici a
h : a ∈ s
⊢ Ioi a ⊆ s ∧ {a} ⊆ s
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
classical
by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
· refine' Or.inl (Subset.antisymm hc _)
  rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right, diff_singleton_subset_iff,
    insert_eq_of_mem hb] at ho 
· refine' Or.inr <| Or.inl <| Subset.antisymm _ _
  · rw [← Icc_diff_right]
    exact subset_diff_singleton hc hb
  · rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho 
· refine' Or.inr <| Or.inr <| Or.inl <| Subset.antisymm _ _
  · rw [← Icc_diff_left]
    exact subset_diff_singleton hc ha
  · rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho 
· refine' Or.inr <| Or.inr <| Or.inr <| Subset.antisymm _ ho
  rw [← Ico_diff_left, ← Icc_diff_right]
  apply_rules [subset_diff_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
by_cases ha : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
by_cases hb : b ∈ s
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
by_cases hb : b ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
refine' Or.inl (Subset.antisymm hc _)
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s
[PROOFSTEP]
rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right, diff_singleton_subset_iff,
  insert_eq_of_mem hb] at ho 
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
refine' Or.inr <| Or.inl <| Subset.antisymm _ _
[GOAL]
case neg.refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ico a b
[PROOFSTEP]
rw [← Icc_diff_right]
[GOAL]
case neg.refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Icc a b \ {b}
[PROOFSTEP]
exact subset_diff_singleton hc hb
[GOAL]
case neg.refine'_2
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s
[PROOFSTEP]
rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho 
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
refine' Or.inr <| Or.inr <| Or.inl <| Subset.antisymm _ _
[GOAL]
case pos.refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Ioc a b
[PROOFSTEP]
rw [← Icc_diff_left]
[GOAL]
case pos.refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Icc a b \ {a}
[PROOFSTEP]
exact subset_diff_singleton hc ha
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s
[PROOFSTEP]
rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho 
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
refine' Or.inr <| Or.inr <| Or.inr <| Subset.antisymm _ ho
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ioo a b
[PROOFSTEP]
rw [← Ico_diff_left, ← Icc_diff_right]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ (Icc a b \ {b}) \ {a}
[PROOFSTEP]
apply_rules [subset_diff_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ Icc a ⊤ = Ici a
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ Ioc a ⊤ = Ioi a
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderBot α
a : α
⊢ Icc ⊥ a = Iic a
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderBot α
a : α
⊢ Ico ⊥ a = Iio a
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ Icc ⊥ ⊤ = univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ici a \ Ici b = Ico a b
[PROOFSTEP]
rw [diff_eq, compl_Ici, Ici_inter_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ici a \ Ioi b = Icc a b
[PROOFSTEP]
rw [diff_eq, compl_Ioi, Ici_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi a \ Ioi b = Ioc a b
[PROOFSTEP]
rw [diff_eq, compl_Ioi, Ioi_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi a \ Ici b = Ioo a b
[PROOFSTEP]
rw [diff_eq, compl_Ici, Ioi_inter_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Iic b \ Iic a = Ioc a b
[PROOFSTEP]
rw [diff_eq, compl_Iic, inter_comm, Ioi_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Iio b \ Iic a = Ioo a b
[PROOFSTEP]
rw [diff_eq, compl_Iic, inter_comm, Ioi_inter_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Iic b \ Iio a = Icc a b
[PROOFSTEP]
rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Iio b \ Iio a = Ico a b
[PROOFSTEP]
rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : a₁ < b₁
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁
[PROOFSTEP]
convert @Ico_subset_Ico_iff αᵒᵈ _ b₁ b₂ a₁ a₂ h₁ using 2
[GOAL]
case h.e'_1.h.e'_3.h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : a₁ < b₁
e_1✝ : Set α = Set αᵒᵈ
⊢ Ioc a₁ b₁ = Ico b₁ a₁
[PROOFSTEP]
exact (@dual_Ico α _ _ _).symm
[GOAL]
case h.e'_1.h.e'_4.h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : a₁ < b₁
e_1✝ : Set α = Set αᵒᵈ
⊢ Ioc a₂ b₂ = Ico b₂ a₂
[PROOFSTEP]
exact (@dual_Ico α _ _ _).symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂
[PROOFSTEP]
rcases exists_between h₁ with ⟨x, xa, xb⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁
[PROOFSTEP]
refine' le_of_not_lt fun h' => _
[GOAL]
case intro.intro.right
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ b₁ ≤ b₂
[PROOFSTEP]
refine' le_of_not_lt fun h' => _
[GOAL]
case intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ False
[PROOFSTEP]
have ab := (h ⟨xa, xb⟩).1.trans xb
[GOAL]
case intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
ab : a₂ < b₁
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (h ⟨h', ab⟩).1
[GOAL]
case intro.intro.right
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False
[PROOFSTEP]
have ab := xa.trans (h ⟨xa, xb⟩).2
[GOAL]
case intro.intro.right
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
ab : a₁ < b₂
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (h ⟨ab, h'⟩).2
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ = Ico a₂ b₂
⊢ a₁ = a₂ ∧ b₁ = b₂
[PROOFSTEP]
simp [Subset.antisymm_iff] at e 
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ a₁ = a₂ ∧ b₁ = b₂
[PROOFSTEP]
simp [le_antisymm_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
cases' h with h h <;> simp [Ico_subset_Ico_iff h] at e  <;> [rcases e with ⟨⟨h₁, h₂⟩, e'⟩;
      rcases e with ⟨e', ⟨h₁, h₂⟩⟩] <;>
    -- Porting note: restore `tauto`have hab := (Ico_subset_Ico_iff <| h₁.trans_lt <| h.trans_le h₂).1 e' <;>
  [exact ⟨⟨hab.left, h₁⟩, ⟨h₂, hab.right⟩⟩; exact ⟨⟨h₁, hab.left⟩, ⟨hab.right, h₂⟩⟩]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
cases' h with h h <;> simp [Ico_subset_Ico_iff h] at e  <;> [rcases e with ⟨⟨h₁, h₂⟩, e'⟩; rcases e with ⟨e', ⟨h₁, h₂⟩⟩]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
cases' h with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
h : a₁ < b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
simp [Ico_subset_Ico_iff h] at e 
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
h : a₂ < b₂
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
simp [Ico_subset_Ico_iff h] at e 
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁
e : (a₂ ≤ a₁ ∧ b₁ ≤ b₂) ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
rcases e with ⟨⟨h₁, h₂⟩, e'⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ a₁ ≤ a₂ ∧ b₂ ≤ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
rcases e with ⟨e', ⟨h₁, h₂⟩⟩
[GOAL]
case inl.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁
e' : Ico a₂ b₂ ⊆ Ico a₁ b₁
h₁ : a₂ ≤ a₁
h₂ : b₁ ≤ b₂
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
have hab := (Ico_subset_Ico_iff <| h₁.trans_lt <| h.trans_le h₂).1 e'
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₂ < b₂
e' : Ico a₁ b₁ ⊆ Ico a₂ b₂
h₁ : a₁ ≤ a₂
h₂ : b₂ ≤ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
have hab := (Ico_subset_Ico_iff <| h₁.trans_lt <| h.trans_le h₂).1 e'
[GOAL]
case inl.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁
e' : Ico a₂ b₂ ⊆ Ico a₁ b₁
h₁ : a₂ ≤ a₁
h₂ : b₁ ≤ b₂
hab : a₁ ≤ a₂ ∧ b₂ ≤ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
exact ⟨⟨hab.left, h₁⟩, ⟨h₂, hab.right⟩⟩
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₂ < b₂
e' : Ico a₁ b₁ ⊆ Ico a₂ b₂
h₁ : a₁ ≤ a₂
h₂ : b₂ ≤ b₁
hab : a₂ ≤ a₁ ∧ b₁ ≤ b₂
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
exact ⟨⟨h₁, hab.left⟩, ⟨hab.right, h₂⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
x✝ : a₁ = a₂ ∧ b₁ = b₂
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ Ico a₁ b₁ = Ico a₂ b₂
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi b ⊆ Ioi a ↔ a ≤ b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => Ioi_subset_Ioi h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Ioi b ⊆ Ioi a
⊢ a ≤ b
[PROOFSTEP]
by_contra ba
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Ioi b ⊆ Ioi a
ba : ¬a ≤ b
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (h (not_le.mp ba))
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
⊢ Ioi b ⊆ Ici a ↔ a ≤ b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => Ioi_subset_Ici h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
⊢ a ≤ b
[PROOFSTEP]
by_contra ba
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
⊢ False
[PROOFSTEP]
obtain ⟨c, bc, ca⟩ : ∃ c, b < c ∧ c < a := exists_between (not_le.mp ba)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c✝ d : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
c : α
bc : b < c
ca : c < a
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (ca.trans_le (h bc))
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Iio a ⊆ Iio b ↔ a ≤ b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => Iio_subset_Iio h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Iio a ⊆ Iio b
⊢ a ≤ b
[PROOFSTEP]
by_contra ab
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Iio a ⊆ Iio b
ab : ¬a ≤ b
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (h (not_le.mp ab))
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
⊢ Iio a ⊆ Iic b ↔ a ≤ b
[PROOFSTEP]
rw [← diff_eq_empty, Iio_diff_Iic, Ioo_eq_empty_iff, not_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp_rw [mem_union, mem_Ioo, mem_Ioi, min_lt_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x
[PROOFSTEP]
by_cases hc : c < x
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hc, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have hxb : x < b := (le_of_not_gt hc).trans_lt h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hxb, and_true]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c < max a b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c < max a b
hab : a ≤ b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
simp [hab] at h 
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c < max a b
hab : b ≤ a
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
simp [hab] at h 
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
h : c < b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
exact Ioo_union_Ioi' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
h : c < a
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
rw [min_comm]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
h : c < a
⊢ Ioo a b ∪ Ioi c = Ioi (min c a)
[PROOFSTEP]
simp [*, min_eq_left_of_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Ico a b ∪ Ici c ↔ x ∈ Ici (min a c)
[PROOFSTEP]
simp_rw [mem_union, mem_Ico, mem_Ici, min_le_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hc, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hxb, and_true]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : a ≤ b
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [hab] at h 
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : b ≤ a
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [hab] at h 
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
h : c ≤ b
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
exact Ico_union_Ici' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
h : c ≤ a
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Ioc a b ∪ Ioi c ↔ x ∈ Ioi (min a c)
[PROOFSTEP]
simp_rw [mem_union, mem_Ioc, mem_Ioi, min_lt_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x
[PROOFSTEP]
by_cases hc : c < x
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hc, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_gt hc).trans h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hxb, and_true]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : a ≤ b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
simp [hab] at h 
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : b ≤ a
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
simp [hab] at h 
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
h : c ≤ b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
exact Ioc_union_Ioi' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
h : c ≤ a
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Icc a b ∪ Ici c ↔ x ∈ Ici (min a c)
[PROOFSTEP]
simp_rw [mem_union, mem_Icc, mem_Ici, min_le_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hc, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hxb, and_true]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
cases' le_or_lt a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : a ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [hab] at h 
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : b < a
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [hab] at h 
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
h : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
exact Icc_union_Ici' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ a ∨ c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
cases' h with h h
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ a
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
have hca : c ≤ a := h.trans hab.le
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ b
hca : c ≤ a
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Iio b ∪ Ico c d ↔ x ∈ Iio (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Iio, mem_Ico, lt_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hc, true_and]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hxb, true_or]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
hcd : c ≤ d
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
simp [hcd] at h 
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
hcd : d ≤ c
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
simp [hcd] at h 
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : c ≤ d
h : c ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
exact Iio_union_Ico' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp_rw [mem_union, mem_Iic, mem_Ioc, le_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
[PROOFSTEP]
by_cases hc : c < x
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hc, true_and]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_gt hc).trans h₁.le
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hxb, true_or]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
hcd : c ≤ d
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
simp [hcd] at h 
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
hcd : d ≤ c
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
simp [hcd] at h 
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : c ≤ d
h : c < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
exact Iic_union_Ioc' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
rw [max_comm]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iic b ∪ Ioc c d = Iic (max d b)
[PROOFSTEP]
simp [*, max_eq_right_of_lt h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
[PROOFSTEP]
cases' lt_or_le x b with hba hba
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : x < b
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
[PROOFSTEP]
simp [hba, h₁]
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
[PROOFSTEP]
simp only [mem_Iio, mem_union, mem_Ioo, lt_max_iff]
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < b ∨ c < x ∧ x < d ↔ x < b ∨ x < d
[PROOFSTEP]
refine' or_congr Iff.rfl ⟨And.right, _⟩
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < d → c < x ∧ x < d
[PROOFSTEP]
exact fun h₂ => ⟨h₁.trans_le hba, h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
hcd : c ≤ d
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
simp [hcd] at h 
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
hcd : d ≤ c
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
simp [hcd] at h 
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : c ≤ d
h : c < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
exact Iio_union_Ioo' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
rw [max_comm]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (max d b)
[PROOFSTEP]
simp [*, max_eq_right_of_lt h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Iic b ∪ Icc c d ↔ x ∈ Iic (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Iic, mem_Icc, le_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hc, true_and]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [hxb, true_or]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
cases' le_or_lt c d with hcd hcd
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
hcd : c ≤ d
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
simp [hcd] at h 
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
hcd : d < c
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
simp [hcd] at h 
[GOAL]
case inl
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
exact Iic_union_Icc' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
cases' h with h h
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
have hdb : d ≤ b := hcd.le.trans h
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp_rw [mem_union, mem_Ico, min_le_iff, lt_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
by_cases hd : x < d
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
by_cases hd : x < d
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hc, hd, and_self, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
have hax : a ≤ x := h₂.trans (le_of_not_gt hd)
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hax, true_and, hc, or_self]
  -- Porting note: restore `tauto`
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hxb, and_true, hc, false_and, or_false, true_or]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hc, hd, and_self, or_false]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
hcd : c ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂ 
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
hcd : d ≤ c
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂ 
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
hcd : c ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂ 
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
hcd : d ≤ c
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂ 
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a ≤ d
h₂ : c ≤ b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
exact Ico_union_Ico' h₂ h₁
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
all_goals simp [*]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ x ∈ Ioc a b ∪ Ioc c d ↔ x ∈ Ioc (min a c) (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Ioc, min_lt_iff, le_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
by_cases hc : c < x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c < x
⊢ a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
by_cases hd : x ≤ d
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c < x
⊢ a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
by_cases hd : x ≤ d
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hc, hd, and_self, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
have hax : a < x := h₂.trans_lt (lt_of_not_ge hd)
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hax, true_and, hc, or_self]
  -- Porting note: restore `tauto`
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_gt hc).trans h₁
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hxb, and_true, hc, false_and, or_false, true_or]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hc, hd, and_self, or_false]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
hcd : c ≤ d
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂ 
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
hcd : d ≤ c
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂ 
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
hcd : c ≤ d
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂ 
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
hcd : d ≤ c
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂ 
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a ≤ d
h₂ : c ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
exact Ioc_union_Ioc' h₂ h₁
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
all_goals simp [*]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ x ∈ Icc a b ∪ Icc c d ↔ x ∈ Icc (min a c) (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Icc, min_le_iff, le_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ (a ≤ x ∨ c ≤ x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
by_cases hd : x ≤ d
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ (a ≤ x ∨ c ≤ x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
by_cases hd : x ≤ d
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hc, hd, and_self, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
have hax : a ≤ x := h₂.trans (le_of_not_ge hd)
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hax, true_and, hc, or_self]
  -- Porting note: restore `tauto`
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hxb, and_true, hc, false_and, or_false, true_or]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hc, hd, and_self, or_false]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
cases' le_or_lt a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
cases' le_or_lt c d with hcd hcd
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b < a
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
cases' le_or_lt c d with hcd hcd
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
hcd : c ≤ d
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt, min_eq_right_of_lt,
  max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂ 
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
hcd : d < c
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt, min_eq_right_of_lt,
  max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂ 
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b < a
hcd : c ≤ d
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt, min_eq_right_of_lt,
  max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂ 
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b < a
hcd : d < c
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt, min_eq_right_of_lt,
  max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂ 
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a < d
h₂ : c < b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
exact Icc_union_Icc' h₂.le h₁.le
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d < c
h₁ : a < c
h₂ : d < b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
hcd : d < c
h₁ : b < c
h₂ : d < a
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
all_goals simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d < c
h₁ : a < c
h₂ : d < b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
hcd : d < c
h₁ : b < c
h₂ : d < a
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
⊢ x ∈ Ioo a b ∪ Ioo c d ↔ x ∈ Ioo (min a c) (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Ioo, min_lt_iff, lt_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
by_cases hc : c < x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
hc : c < x
⊢ a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
by_cases hd : x < d
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
hc : ¬c < x
⊢ a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
by_cases hd : x < d
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hc, hd, and_self, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
have hax : a < x := h₂.trans_le (le_of_not_lt hd)
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hax, true_and, hc, or_self]
  -- Porting note: restore `tauto`
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
have hxb : x < b := (le_of_not_lt hc).trans_lt h₁
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hxb, and_true, hc, false_and, or_false, true_or]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp only [hc, hd, and_self, or_false]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b ≤ a
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
hcd : c ≤ d
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, hab, hcd] at h₁ h₂ 
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
hcd : d ≤ c
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, hab, hcd] at h₁ h₂ 
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b ≤ a
hcd : c ≤ d
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, hab, hcd] at h₁ h₂ 
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b ≤ a
hcd : d ≤ c
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, hab, hcd] at h₁ h₂ 
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a < d
h₂ : c < b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
exact Ioo_union_Ioo' h₂ h₁
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a < c
h₂ : d < b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b < c
h₂ : d < a
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
all_goals
  simp [*, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, le_of_lt h₂, le_of_lt h₁]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a < c
h₂ : d < b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, le_of_lt h₂, le_of_lt h₁]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, le_of_lt h₂, le_of_lt h₁]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b < c
h₂ : d < a
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, le_of_lt h₂, le_of_lt h₁]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a b : α
⊢ Iic a ∩ Iic b = Iic (a ⊓ b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a b x : α
⊢ x ∈ Iic a ∩ Iic b ↔ x ∈ Iic (a ⊓ b)
[PROOFSTEP]
simp [Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)
[PROOFSTEP]
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a b : α
⊢ Ici a ∩ Ici b = Ici (a ⊔ b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a b x : α
⊢ x ∈ Ici a ∩ Ici b ↔ x ∈ Ici (a ⊔ b)
[PROOFSTEP]
simp [Ici]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ Ico a b ∩ Ici c = Ico (a ⊔ c) b
[PROOFSTEP]
rw [← Ici_inter_Iio, ← Ici_inter_Iio, ← Ici_inter_Ici, inter_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Lattice α
a b c a₁ a₂ b₁ b₂ : α
⊢ Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
[PROOFSTEP]
simp only [Ici_inter_Iic.symm, Ici_inter_Ici.symm, Iic_inter_Iic.symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Lattice α
a b c a₁ a₂ b₁ b₂ : α
⊢ Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Lattice α
a b c a₁ a₂ b₁ b₂ : α
hab : a ≤ b
hbc : b ≤ c
⊢ Icc a b ∩ Icc b c = {b}
[PROOFSTEP]
rw [Icc_inter_Icc, sup_of_le_right hab, inf_of_le_left hbc, Icc_self]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂)
[PROOFSTEP]
simp only [Ici_inter_Iio.symm, Ici_inter_Ici.symm, Iio_inter_Iio.symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ici a₁ ∩ Iio b₁ ∩ (Ici a₂ ∩ Iio b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iio b₁ ∩ Iio b₂)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
[PROOFSTEP]
simp only [Ioi_inter_Iic.symm, Ioi_inter_Ioi.symm, Iic_inter_Iic.symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi a₁ ∩ Iic b₁ ∩ (Ioi a₂ ∩ Iic b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iic b₁ ∩ Iic b₂)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioo a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (a₁ ⊔ a₂) (b₁ ⊓ b₂)
[PROOFSTEP]
simp only [Ioi_inter_Iio.symm, Ioi_inter_Ioi.symm, Iio_inter_Iio.symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi a₁ ∩ Iio b₁ ∩ (Ioi a₂ ∩ Iio b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iio b₁ ∩ Iio b₂)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
h : b₁ < b₂
x : α
⊢ x ∈ Ioc a₁ b₁ ∩ Ioo a₂ b₂ ↔ x ∈ Ioc (max a₁ a₂) b₁
[PROOFSTEP]
simp [and_assoc, @and_left_comm (x ≤ _), and_iff_left_iff_imp.2 fun h' => lt_of_le_of_lt h' h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
h : b₂ ≤ b₁
x : α
⊢ x ∈ Ioc a₁ b₁ ∩ Ioo a₂ b₂ ↔ x ∈ Ioo (max a₁ a₂) b₂
[PROOFSTEP]
simp [and_assoc, @and_left_comm (x ≤ _), and_iff_right_iff_imp.2 fun h' => (le_of_lt h').trans h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
h : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁
[PROOFSTEP]
rw [inter_comm, Ioc_inter_Ioo_of_right_le h, max_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
h : b₂ < b₁
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂
[PROOFSTEP]
rw [inter_comm, Ioc_inter_Ioo_of_left_lt h, max_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ico a b \ Iio c = Ico (max a c) b
[PROOFSTEP]
rw [diff_eq, compl_Iio, Ico_inter_Ici, sup_eq_max]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ ∀ (x : α), x ∈ Ioc a b \ Ioi c ↔ x ∈ Ioc a (min b c)
[PROOFSTEP]
simp (config := { contextual := true }) [iff_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∩ Ioi c = Ioc (a ⊔ c) b
[PROOFSTEP]
rw [← Ioi_inter_Iic, inter_assoc, inter_comm, inter_assoc, Ioi_inter_Ioi, inter_comm, Ioi_inter_Iic, sup_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ ∀ (x : α), x ∈ Ico a b ∩ Iio c ↔ x ∈ Ico a (min b c)
[PROOFSTEP]
simp (config := { contextual := true }) [iff_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b \ Iic c = Ioc (max a c) b
[PROOFSTEP]
rw [diff_eq, compl_Iic, Ioc_inter_Ioi, sup_eq_max]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc a c = Ioc a (max b c)
[PROOFSTEP]
rw [Ioc_union_Ioc, min_self]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a b ≤ max a c
[PROOFSTEP]
exact (min_le_left _ _).trans (le_max_left _ _)
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a c ≤ max a b
[PROOFSTEP]
exact (min_le_left _ _).trans (le_max_left _ _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a c ∪ Ioc b c = Ioc (min a b) c
[PROOFSTEP]
rw [Ioc_union_Ioc, max_self]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a c ≤ max b c
[PROOFSTEP]
exact (min_le_right _ _).trans (le_max_right _ _)
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min b c ≤ max a c
[PROOFSTEP]
exact (min_le_right _ _).trans (le_max_right _ _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc b a = Ioc (min a b) (max a b)
[PROOFSTEP]
rw [max_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc b a = Ioc (min a b) (max b a)
[PROOFSTEP]
apply Ioc_union_Ioc
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a b ≤ max b a
[PROOFSTEP]
rw [max_comm]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min b a ≤ max a b
[PROOFSTEP]
rw [max_comm]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a b ≤ max a b
[PROOFSTEP]
exact min_le_max
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min b a ≤ max b a
[PROOFSTEP]
exact min_le_max
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc (min a (min b c)) (max a (max b c))
[PROOFSTEP]
rw [Ioc_union_Ioc, Ioc_union_Ioc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc (min (min a b) c) (max (max b c) a) = Ioc (min a (min b c)) (max a (max b c))
[PROOFSTEP]
simp [min_le_of_left_le, min_le_of_right_le, le_max_of_le_left, le_max_of_le_right, le_refl, min_assoc, max_comm]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min (min a b) (max b c) ≤ max c a
[PROOFSTEP]
simp [min_le_of_left_le, min_le_of_right_le, le_max_of_le_left, le_max_of_le_right, le_refl, min_assoc, max_comm]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min c a ≤ max (min a b) (max b c)
[PROOFSTEP]
simp [min_le_of_left_le, min_le_of_right_le, le_max_of_le_left, le_max_of_le_right, le_refl, min_assoc, max_comm]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a b ≤ max b c
[PROOFSTEP]
simp [min_le_of_left_le, min_le_of_right_le, le_max_of_le_left, le_max_of_le_right, le_refl, min_assoc, max_comm]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min b c ≤ max a b
[PROOFSTEP]
simp [min_le_of_left_le, min_le_of_right_le, le_max_of_le_left, le_max_of_le_right, le_refl, min_assoc, max_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
x : α
y : β
⊢ (x, y) ∈ Icc a₁ a₂ ×ˢ Icc b₁ b₂ ↔ (x, y) ∈ Icc (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
simp [and_assoc, and_comm, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α × β
⊢ Icc a b = Icc a.fst b.fst ×ˢ Icc a.snd b.snd
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioo x y)
a : α
ha₁ : x < a
ha₂ : a < y
⊢ ∃ b, b < { val := a, property := (_ : x < a ∧ a < y) }
[PROOFSTEP]
rcases exists_between ha₁ with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioo x y)
a : α
ha₁ : x < a
ha₂ : a < y
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ b, b < { val := a, property := (_ : x < a ∧ a < y) }
[PROOFSTEP]
exact ⟨⟨b, hb₁, hb₂.trans ha₂⟩, hb₂⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioc x y)
a : α
ha₁ : x < a
ha₂ : a ≤ y
⊢ ∃ b, b < { val := a, property := (_ : x < a ∧ a ≤ y) }
[PROOFSTEP]
rcases exists_between ha₁ with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioc x y)
a : α
ha₁ : x < a
ha₂ : a ≤ y
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ b, b < { val := a, property := (_ : x < a ∧ a ≤ y) }
[PROOFSTEP]
exact ⟨⟨b, hb₁, hb₂.le.trans ha₂⟩, hb₂⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioi x)
a : α
ha : a ∈ Set.Ioi x
⊢ ∃ b, b < { val := a, property := ha }
[PROOFSTEP]
rcases exists_between ha with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioi x)
a : α
ha : a ∈ Set.Ioi x
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ b, b < { val := a, property := ha }
[PROOFSTEP]
exact ⟨⟨b, hb₁⟩, hb₂⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioo x y)
a : α
ha₁ : x < a
ha₂ : a < y
⊢ ∃ b, { val := a, property := (_ : x < a ∧ a < y) } < b
[PROOFSTEP]
rcases exists_between ha₂ with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioo x y)
a : α
ha₁ : x < a
ha₂ : a < y
b : α
hb₁ : a < b
hb₂ : b < y
⊢ ∃ b, { val := a, property := (_ : x < a ∧ a < y) } < b
[PROOFSTEP]
exact ⟨⟨b, ha₁.trans hb₁, hb₂⟩, hb₁⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ico x y)
a : α
ha₁ : x ≤ a
ha₂ : a < y
⊢ ∃ b, { val := a, property := (_ : x ≤ a ∧ a < y) } < b
[PROOFSTEP]
rcases exists_between ha₂ with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ico x y)
a : α
ha₁ : x ≤ a
ha₂ : a < y
b : α
hb₁ : a < b
hb₂ : b < y
⊢ ∃ b, { val := a, property := (_ : x ≤ a ∧ a < y) } < b
[PROOFSTEP]
exact ⟨⟨b, ha₁.trans hb₁.le, hb₂⟩, hb₁⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Iio x)
a : α
ha : a ∈ Set.Iio x
⊢ ∃ b, { val := a, property := ha } < b
[PROOFSTEP]
rcases exists_between ha with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Iio x)
a : α
ha : a ∈ Set.Iio x
b : α
hb₁ : a < b
hb₂ : b < x
⊢ ∃ b, { val := a, property := ha } < b
[PROOFSTEP]
exact ⟨⟨b, hb₂⟩, hb₁⟩
