case left
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ lowerBounds s

case right
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ upperBounds (lowerBounds s)
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ IsGLB s (sInf s)
constructor
case left
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} then ⊤ else ↑(sInf ((fun a => ↑a) ⁻¹' s))) ∈ lowerBounds s
case left
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ lowerBounds s
show ite _ _ _ ∈ _
case left.inl
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ lowerBounds s

case left.inr
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a => ↑a) ⁻¹' s)) ∈ lowerBounds s
case left
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} then ⊤ else ↑(sInf ((fun a => ↑a) ⁻¹' s))) ∈ lowerBounds s
split_ifs with h
case left.inl
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a : WithTop β
ha : a ∈ s
⊢ ⊤ ≤ a
case left.inl
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ lowerBounds s
intro a ha
no goals
case left.inl
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a : WithTop β
ha : a ∈ s
⊢ ⊤ ≤ a
exact top_le_iff.2 (Set.mem_singleton_iff.1 (h ha))
case left.inr.none
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ s
⊢ ↑(sInf ((fun a => ↑a) ⁻¹' s)) ≤ none

case left.inr.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
⊢ ↑(sInf ((fun a => ↑a) ⁻¹' s)) ≤ Option.some a
case left.inr
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a => ↑a) ⁻¹' s)) ∈ lowerBounds s
rintro (⟨⟩ | a) ha
case left.inr.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
⊢ BddBelow ((fun a => ↑a) ⁻¹' s)
case left.inr.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
⊢ ↑(sInf ((fun a => ↑a) ⁻¹' s)) ≤ Option.some a
refine' some_le_some.2 (csInf_le _ ha)
case left.inr.some.intro.none
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ BddBelow ((fun a => ↑a) ⁻¹' s)

case left.inr.some.intro.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
⊢ BddBelow ((fun a => ↑a) ⁻¹' s)
case left.inr.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
⊢ BddBelow ((fun a => ↑a) ⁻¹' s)
rcases hs with ⟨⟨⟩ | b, hb⟩
case left.inr.some.intro.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
⊢ b ∈ lowerBounds ((fun a => ↑a) ⁻¹' s)
case left.inr.some.intro.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
⊢ BddBelow ((fun a => ↑a) ⁻¹' s)
use b
case left.inr.some.intro.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
c : β
hc : c ∈ (fun a => ↑a) ⁻¹' s
⊢ b ≤ c
case left.inr.some.intro.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
⊢ b ∈ lowerBounds ((fun a => ↑a) ⁻¹' s)
intro c hc
no goals
case left.inr.some.intro.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
c : β
hc : c ∈ (fun a => ↑a) ⁻¹' s
⊢ b ≤ c
exact some_le_some.1 (hb hc)
no goals
case left.inr.none
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ s
⊢ ↑(sInf ((fun a => ↑a) ⁻¹' s)) ≤ none
exact le_top
case left.inr.some.intro.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ False
case left.inr.some.intro.none
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ BddBelow ((fun a => ↑a) ⁻¹' s)
exfalso
case left.inr.some.intro.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ s ⊆ {⊤}
case left.inr.some.intro.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ False
apply h
case left.inr.some.intro.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ c ∈ {⊤}
case left.inr.some.intro.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ s ⊆ {⊤}
intro c hc
case left.inr.some.intro.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ ⊤ ≤ c
case left.inr.some.intro.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ c ∈ {⊤}
rw [mem_singleton_iff, ← top_le_iff]
no goals
case left.inr.some.intro.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ ⊤ ≤ c
exact hb hc
case right
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} then ⊤ else ↑(sInf ((fun a => ↑a) ⁻¹' s))) ∈ upperBounds (lowerBounds s)
case right
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ upperBounds (lowerBounds s)
show ite _ _ _ ∈ _
case right.inl
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ upperBounds (lowerBounds s)

case right.inr
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a => ↑a) ⁻¹' s)) ∈ upperBounds (lowerBounds s)
case right
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} then ⊤ else ↑(sInf ((fun a => ↑a) ⁻¹' s))) ∈ upperBounds (lowerBounds s)
split_ifs with h
case right.inl
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a✝¹ : WithTop β
a✝ : a✝¹ ∈ lowerBounds s
⊢ a✝¹ ≤ ⊤
case right.inl
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ upperBounds (lowerBounds s)
intro _ _
no goals
case right.inl
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a✝¹ : WithTop β
a✝ : a✝¹ ∈ lowerBounds s
⊢ a✝¹ ≤ ⊤
exact le_top
case right.inr.none
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ none ≤ ↑(sInf ((fun a => ↑a) ⁻¹' s))

case right.inr.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Option.some a ≤ ↑(sInf ((fun a => ↑a) ⁻¹' s))
case right.inr
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a => ↑a) ⁻¹' s)) ∈ upperBounds (lowerBounds s)
rintro (⟨⟩ | a) ha
case right.inr.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ False
case right.inr.none
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ none ≤ ↑(sInf ((fun a => ↑a) ⁻¹' s))
exfalso
case right.inr.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ s ⊆ {⊤}
case right.inr.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ False
apply h
case right.inr.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
b : WithTop β
hb : b ∈ s
⊢ b ∈ {⊤}
case right.inr.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ s ⊆ {⊤}
intro b hb
no goals
case right.inr.none.h
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
b : WithTop β
hb : b ∈ s
⊢ b ∈ {⊤}
exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))
case right.inr.some.refine'_1
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Set.Nonempty ((fun a => ↑a) ⁻¹' s)

case right.inr.some.refine'_2
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ∀ (b : β), b ∈ (fun a => ↑a) ⁻¹' s → a ≤ b
case right.inr.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Option.some a ≤ ↑(sInf ((fun a => ↑a) ⁻¹' s))
refine' some_le_some.2 (le_csInf _ _)
case right.inr.some.refine'_1
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha : Option.some a ∈ lowerBounds s
h : ¬Set.Nonempty ((fun a => ↑a) ⁻¹' s)
⊢ s ⊆ {⊤}
case right.inr.some.refine'_1
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Set.Nonempty ((fun a => ↑a) ⁻¹' s)
contrapose! h
case right.inr.some.refine'_1.none
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha✝ : Option.some a ∈ lowerBounds s
h : ¬Set.Nonempty ((fun a => ↑a) ⁻¹' s)
ha : none ∈ s
⊢ none ∈ {⊤}

case right.inr.some.refine'_1.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a✝ : β
ha✝ : Option.some a✝ ∈ lowerBounds s
h : ¬Set.Nonempty ((fun a => ↑a) ⁻¹' s)
a : β
ha : Option.some a ∈ s
⊢ Option.some a ∈ {⊤}
case right.inr.some.refine'_1
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha : Option.some a ∈ lowerBounds s
h : ¬Set.Nonempty ((fun a => ↑a) ⁻¹' s)
⊢ s ⊆ {⊤}
rintro (⟨⟩ | a) ha
no goals
case right.inr.some.refine'_1.none
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha✝ : Option.some a ∈ lowerBounds s
h : ¬Set.Nonempty ((fun a => ↑a) ⁻¹' s)
ha : none ∈ s
⊢ none ∈ {⊤}
exact mem_singleton ⊤
no goals
case right.inr.some.refine'_1.some
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a✝ : β
ha✝ : Option.some a✝ ∈ lowerBounds s
h : ¬Set.Nonempty ((fun a => ↑a) ⁻¹' s)
a : β
ha : Option.some a ∈ s
⊢ Option.some a ∈ {⊤}
exact (h ⟨a, ha⟩).elim
case right.inr.some.refine'_2
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : b ∈ (fun a => ↑a) ⁻¹' s
⊢ a ≤ b
case right.inr.some.refine'_2
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ∀ (b : β), b ∈ (fun a => ↑a) ⁻¹' s → a ≤ b
intro b hb
case right.inr.some.refine'_2
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : b ∈ (fun a => ↑a) ⁻¹' s
⊢ Option.some a ≤ Option.some b
case right.inr.some.refine'_2
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : b ∈ (fun a => ↑a) ⁻¹' s
⊢ a ≤ b
rw [← some_le_some]
no goals
case right.inr.some.refine'_2
α : Type ?u.90006
β✝ : Type ?u.90009
γ : Type ?u.90012
ι : Sort ?u.90015
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : b ∈ (fun a => ↑a) ⁻¹' s
⊢ Option.some a ≤ Option.some b
exact ha hb