case inl
ι : Type ?u.326160
ι' : Type ?u.326163
α : Type u_1
β : Type ?u.326169
γ : Type ?u.326172
inst✝ : SemilatticeSup α
a : α
h : IsEmpty ↑(Ioi a)
⊢ atTop = comap Subtype.val atTop

case inr.intro.mk
ι : Type ?u.326160
ι' : Type ?u.326163
α : Type u_1
β : Type ?u.326169
γ : Type ?u.326172
inst✝ : SemilatticeSup α
a b : α
hb : b ∈ Ioi a
⊢ atTop = comap Subtype.val atTop
ι : Type ?u.326160
ι' : Type ?u.326163
α : Type u_1
β : Type ?u.326169
γ : Type ?u.326172
inst✝ : SemilatticeSup α
a : α
⊢ atTop = comap Subtype.val atTop
rcases isEmpty_or_nonempty (Ioi a) with h|⟨⟨b, hb⟩⟩
no goals
case inl
ι : Type ?u.326160
ι' : Type ?u.326163
α : Type u_1
β : Type ?u.326169
γ : Type ?u.326172
inst✝ : SemilatticeSup α
a : α
h : IsEmpty ↑(Ioi a)
⊢ atTop = comap Subtype.val atTop
exact Subsingleton.elim _ _
no goals
case inr.intro.mk
ι : Type ?u.326160
ι' : Type ?u.326163
α : Type u_1
β : Type ?u.326169
γ : Type ?u.326172
inst✝ : SemilatticeSup α
a b : α
hb : b ∈ Ioi a
⊢ atTop = comap Subtype.val atTop
rw [← map_val_atTop_of_Ici_subset (Ici_subset_Ioi.2 hb), comap_map Subtype.coe_injective]