case left
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
⊢ sSup s ∈ upperBounds s

case right
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
⊢ sSup s ∈ lowerBounds (upperBounds s)
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
⊢ IsLUB s (sSup s)
constructor
case left
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
⊢ (if ⊤ ∈ s then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' s) then ↑(sSup ((fun a => ↑a) ⁻¹' s)) else ⊤) ∈ upperBounds s
case left
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
⊢ sSup s ∈ upperBounds s
show ite _ _ _ ∈ _
case left.inl
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ upperBounds s

case left.inr.inl
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ∈ upperBounds s

case left.inr.inr
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s
case left
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
⊢ (if ⊤ ∈ s then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' s) then ↑(sSup ((fun a => ↑a) ⁻¹' s)) else ⊤) ∈ upperBounds s
split_ifs with h₁ h₂
case left.inl
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ⊤ ∈ s
a✝¹ : WithTop β
a✝ : a✝¹ ∈ s
⊢ a✝¹ ≤ ⊤
case left.inl
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ upperBounds s
intro _ _
no goals
case left.inl
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ⊤ ∈ s
a✝¹ : WithTop β
a✝ : a✝¹ ∈ s
⊢ a✝¹ ≤ ⊤
exact le_top
case left.inr.inl.none
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
ha : none ∈ s
⊢ none ≤ ↑(sSup ((fun a => ↑a) ⁻¹' s))

case left.inr.inl.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
a : β
ha : Option.some a ∈ s
⊢ Option.some a ≤ ↑(sSup ((fun a => ↑a) ⁻¹' s))
case left.inr.inl
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ∈ upperBounds s
rintro (⟨⟩ | a) ha
case left.inr.inl.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
a : β
ha : Option.some a ∈ s
⊢ a ≤ sSup ((fun a => ↑a) ⁻¹' s)
case left.inr.inl.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
a : β
ha : Option.some a ∈ s
⊢ Option.some a ≤ ↑(sSup ((fun a => ↑a) ⁻¹' s))
apply some_le_some.2
no goals
case left.inr.inl.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
a : β
ha : Option.some a ∈ s
⊢ a ≤ sSup ((fun a => ↑a) ⁻¹' s)
exact le_csSup h₂ ha
no goals
case left.inr.inl.none
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
ha : none ∈ s
⊢ none ≤ ↑(sSup ((fun a => ↑a) ⁻¹' s))
contradiction
case left.inr.inr
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
a✝¹ : WithTop β
a✝ : a✝¹ ∈ s
⊢ a✝¹ ≤ ⊤
case left.inr.inr
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s
intro _ _
no goals
case left.inr.inr
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
a✝¹ : WithTop β
a✝ : a✝¹ ∈ s
⊢ a✝¹ ≤ ⊤
exact le_top
case right
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
⊢ (if ⊤ ∈ s then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' s) then ↑(sSup ((fun a => ↑a) ⁻¹' s)) else ⊤) ∈
    lowerBounds (upperBounds s)
case right
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
⊢ sSup s ∈ lowerBounds (upperBounds s)
show ite _ _ _ ∈ _
case right.inl
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ lowerBounds (upperBounds s)

case right.inr.inl
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ∈ lowerBounds (upperBounds s)

case right.inr.inr
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ⊤ ∈ lowerBounds (upperBounds s)
case right
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
⊢ (if ⊤ ∈ s then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' s) then ↑(sSup ((fun a => ↑a) ⁻¹' s)) else ⊤) ∈
    lowerBounds (upperBounds s)
split_ifs with h₁ h₂
case right.inl.none
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ⊤ ∈ s
ha : none ∈ upperBounds s
⊢ ⊤ ≤ none

case right.inl.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a
case right.inl
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ lowerBounds (upperBounds s)
rintro (⟨⟩ | a) ha
no goals
case right.inl.none
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ⊤ ∈ s
ha : none ∈ upperBounds s
⊢ ⊤ ≤ none
exact le_rfl
no goals
case right.inl.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a
exact False.elim (not_top_le_coe a (ha h₁))
case right.inr.inl.none
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ≤ none

case right.inr.inl.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ≤ Option.some b
case right.inr.inl
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ∈ lowerBounds (upperBounds s)
rintro (⟨⟩ | b) hb
case right.inr.inl.some.refine'_1
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ Set.Nonempty ((fun a => ↑a) ⁻¹' s)

case right.inr.inl.some.refine'_2
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ (b_1 : β), b_1 ∈ (fun a => ↑a) ⁻¹' s → b_1 ≤ b
case right.inr.inl.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ≤ Option.some b
refine' some_le_some.2 (csSup_le _ _)
no goals
case right.inr.inl.none
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ≤ none
exact le_top
case right.inr.inl.some.refine'_1.intro.none
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb✝ : Option.some b ∈ upperBounds s
hb : none ∈ s
⊢ Set.Nonempty ((fun a => ↑a) ⁻¹' s)

case right.inr.inl.some.refine'_1.intro.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b✝ : β
hb✝ : Option.some b✝ ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ Set.Nonempty ((fun a => ↑a) ⁻¹' s)
case right.inr.inl.some.refine'_1
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ Set.Nonempty ((fun a => ↑a) ⁻¹' s)
rcases hs with ⟨⟨⟩ | b, hb⟩
no goals
case right.inr.inl.some.refine'_1.intro.none
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb✝ : Option.some b ∈ upperBounds s
hb : none ∈ s
⊢ Set.Nonempty ((fun a => ↑a) ⁻¹' s)
exact absurd hb h₁
no goals
case right.inr.inl.some.refine'_1.intro.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b✝ : β
hb✝ : Option.some b✝ ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ Set.Nonempty ((fun a => ↑a) ⁻¹' s)
exact ⟨b, hb⟩
case right.inr.inl.some.refine'_2
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : a ∈ (fun a => ↑a) ⁻¹' s
⊢ a ≤ b
case right.inr.inl.some.refine'_2
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ (b_1 : β), b_1 ∈ (fun a => ↑a) ⁻¹' s → b_1 ≤ b
intro a ha
no goals
case right.inr.inl.some.refine'_2
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : a ∈ (fun a => ↑a) ⁻¹' s
⊢ a ≤ b
exact some_le_some.1 (hb ha)
case right.inr.inr.none
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ⊤ ≤ none

case right.inr.inr.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ⊤ ≤ Option.some b
case right.inr.inr
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ⊤ ∈ lowerBounds (upperBounds s)
rintro (⟨⟩ | b) hb
no goals
case right.inr.inr.none
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ⊤ ≤ none
exact le_rfl
case right.inr.inr.some.h
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ False
case right.inr.inr.some
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ⊤ ≤ Option.some b
exfalso
case right.inr.inr.some.h
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ BddAbove ((fun a => ↑a) ⁻¹' s)
case right.inr.inr.some.h
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ False
apply h₂
case right.inr.inr.some.h
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ b ∈ upperBounds ((fun a => ↑a) ⁻¹' s)
case right.inr.inr.some.h
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ BddAbove ((fun a => ↑a) ⁻¹' s)
use b
case right.inr.inr.some.h
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : a ∈ (fun a => ↑a) ⁻¹' s
⊢ a ≤ b
case right.inr.inr.some.h
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ b ∈ upperBounds ((fun a => ↑a) ⁻¹' s)
intro a ha
no goals
case right.inr.inr.some.h
α : Type ?u.85179
β✝ : Type ?u.85182
γ : Type ?u.85185
ι : Sort ?u.85188
inst✝¹ : ConditionallyCompleteLinearOrderBot α
β : Type u_1
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : Set.Nonempty s
h₁ : ¬⊤ ∈ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : a ∈ (fun a => ↑a) ⁻¹' s
⊢ a ≤ b
exact some_le_some.1 (hb ha)