no goals
ι : Type ?u.328153
ι' : Type ?u.328156
α : Type u_1
β : Type ?u.328162
γ : Type ?u.328165
inst✝ : SemilatticeSup α
a : α
⊢ atTop = comap Subtype.val atTop
rw [← map_val_Ici_atTop a, comap_map Subtype.coe_injective]