[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : Preorder α
a b c : α
⊢ Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b
[PROOFSTEP]
rw [Set.disjoint_iff_inter_eq_empty, Ici_inter_Iic, Icc_eq_empty_iff]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : Preorder α
a✝ b c a : α
⊢ ⋃ (b : α), Icc a b = Ici a
[PROOFSTEP]
simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : Preorder α
a✝ b c a : α
⊢ ⋃ (b : α), Ioc a b = Ioi a
[PROOFSTEP]
simp only [← Ioi_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : Preorder α
a b✝ c b : α
⊢ ⋃ (a : α), Icc a b = Iic b
[PROOFSTEP]
simp only [← Ici_inter_Iic, ← iUnion_inter, iUnion_Ici, univ_inter]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : Preorder α
a b✝ c b : α
⊢ ⋃ (a : α), Ico a b = Iio b
[PROOFSTEP]
simp only [← Ici_inter_Iio, ← iUnion_inter, iUnion_Ici, univ_inter]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : Preorder α
a✝ b c : α
inst✝ : NoMaxOrder α
a : α
⊢ ⋃ (b : α), Ico a b = Ici a
[PROOFSTEP]
simp only [← Ici_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : Preorder α
a✝ b c : α
inst✝ : NoMaxOrder α
a : α
⊢ ⋃ (b : α), Ioo a b = Ioi a
[PROOFSTEP]
simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : Preorder α
a b✝ c : α
inst✝ : NoMinOrder α
b : α
⊢ ⋃ (a : α), Ioc a b = Iic b
[PROOFSTEP]
simp only [← Ioi_inter_Iic, ← iUnion_inter, iUnion_Ioi, univ_inter]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : Preorder α
a b✝ c : α
inst✝ : NoMinOrder α
b : α
⊢ ⋃ (a : α), Ioo a b = Iio b
[PROOFSTEP]
simp only [← Ioi_inter_Iio, ← iUnion_inter, iUnion_Ioi, univ_inter]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
[PROOFSTEP]
simp_rw [Set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff, inf_eq_min, sup_eq_max, not_lt]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
[PROOFSTEP]
have h : _ ↔ min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂) := Ico_disjoint_Ico
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h :
  Disjoint (Ico (↑toDual a₂) (↑toDual a₁)) (Ico (↑toDual b₂) (↑toDual b₁)) ↔
    min (↑toDual a₁) (↑toDual b₁) ≤ max (↑toDual a₂) (↑toDual b₂)
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
[PROOFSTEP]
simpa only [dual_Ico] using h
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α
h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
[PROOFSTEP]
rw [Ico_disjoint_Ico, min_eq_left (le_of_lt h2.2), le_max_iff] at h 
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
[PROOFSTEP]
apply le_antisymm h2.1
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ x₂ ≤ y₁
[PROOFSTEP]
exact h.elim (fun h => absurd hx (not_lt_of_le h)) id
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
f : ι → α
a : α
⊢ ⋃ (i : ι), Ico (f i) a = Iio a ↔ ∀ (x : α), x < a → ∃ i, f i ≤ x
[PROOFSTEP]
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
f : ι → α
a : α
⊢ ⋃ (i : ι), Ioc a (f i) = Ioi a ↔ ∀ (x : α), a < x → ∃ i, x ≤ f i
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
⊢ ⋃ (i : ι) (hi : p i), Ico (f i hi) a = Iio a ↔ ∀ (x : α), x < a → ∃ i hi, f i hi ≤ x
[PROOFSTEP]
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
⊢ ⋃ (i : ι) (hi : p i), Ioc a (f i hi) = Ioi a ↔ ∀ (x : α), a < x → ∃ i hi, x ≤ f i hi
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
h : IsGLB s a
⊢ ⋃ (x : α) (_ : x ∈ s), Ioi x = Ioi a
[PROOFSTEP]
refine' (iUnion₂_subset fun x hx => _).antisymm fun x hx => _
[GOAL]
case refine'_1
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
h : IsGLB s a
x : α
hx : x ∈ s
⊢ Ioi x ⊆ Ioi a
[PROOFSTEP]
exact Ioi_subset_Ioi (h.1 hx)
[GOAL]
case refine'_2
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ (i : α) (_ : i ∈ s), Ioi i
[PROOFSTEP]
rcases h.exists_between hx with ⟨y, hys, _, hyx⟩
[GOAL]
case refine'_2.intro.intro.intro
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ x ∈ ⋃ (i : α) (_ : i ∈ s), Ioi i
[PROOFSTEP]
exact mem_biUnion hys hyx
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_not_mem : ¬a ∈ s
⊢ ⋃ (x : α) (_ : x ∈ s), Ici x = Ioi a
[PROOFSTEP]
refine' (iUnion₂_subset fun x hx => _).antisymm fun x hx => _
[GOAL]
case refine'_1
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_not_mem : ¬a ∈ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ioi a
[PROOFSTEP]
exact Ici_subset_Ioi.mpr (lt_of_le_of_ne (a_glb.1 hx) fun h => (h ▸ a_not_mem) hx)
[GOAL]
case refine'_2
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_not_mem : ¬a ∈ s
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ (i : α) (_ : i ∈ s), Ici i
[PROOFSTEP]
rcases a_glb.exists_between hx with ⟨y, hys, _, hyx⟩
[GOAL]
case refine'_2.intro.intro.intro
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_not_mem : ¬a ∈ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ x ∈ ⋃ (i : α) (_ : i ∈ s), Ici i
[PROOFSTEP]
apply mem_iUnion₂.mpr
[GOAL]
case refine'_2.intro.intro.intro
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_not_mem : ¬a ∈ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ ∃ i j, x ∈ Ici i
[PROOFSTEP]
refine' ⟨y, hys, hyx.le⟩
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_mem : a ∈ s
⊢ ⋃ (x : α) (_ : x ∈ s), Ici x = Ici a
[PROOFSTEP]
refine' (iUnion₂_subset fun x hx => _).antisymm fun x hx => _
[GOAL]
case refine'_1
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ici a
[PROOFSTEP]
exact Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx)
[GOAL]
case refine'_2
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ Ici a
⊢ x ∈ ⋃ (i : α) (_ : i ∈ s), Ici i
[PROOFSTEP]
apply mem_iUnion₂.mpr
[GOAL]
case refine'_2
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ Ici a
⊢ ∃ i j, x ∈ Ici i
[PROOFSTEP]
refine' ⟨a, a_mem, hx⟩
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : LinearOrder α
s : Set α
a : α
f✝ : ι → α
R : Type u_1
inst✝ : CompleteLinearOrder R
f : ι → R
no_least_elem : ¬⨅ (i : ι), f i ∈ range f
⊢ ⋃ (i : ι), Ici (f i) = Ioi (⨅ (i : ι), f i)
[PROOFSTEP]
simp only [← IsGLB.biUnion_Ici_eq_Ioi (@isGLB_iInf _ _ _ f) no_least_elem, mem_range, iUnion_exists, iUnion_iUnion_eq']
[GOAL]
ι : Sort u
α : Type v
β : Type w
inst✝¹ : LinearOrder α
s : Set α
a : α
f✝ : ι → α
R : Type u_1
inst✝ : CompleteLinearOrder R
f : ι → R
has_least_elem : ⨅ (i : ι), f i ∈ range f
⊢ ⋃ (i : ι), Ici (f i) = Ici (⨅ (i : ι), f i)
[PROOFSTEP]
simp only [← IsGLB.biUnion_Ici_eq_Ici (@isGLB_iInf _ _ _ f) has_least_elem, mem_range, iUnion_exists, iUnion_iUnion_eq']
