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

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
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
s : Set α
a : α
f : ι → α
h : IsGLB s a
⊢ (⋃ (x : α) (_ : x ∈ s), Ioi x) = Ioi a
refine' (iUnion₂_subset fun x hx => _).antisymm fun x hx => _
no goals
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
exact Ioi_subset_Ioi (h.1 hx)
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
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
rcases h.exists_between hx with ⟨y, hys, _, hyx⟩
no goals
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
exact mem_biUnion hys hyx