rintro rfl
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
a : α✝
⊢ a = s → a ≠ ⊥
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α✝
hs : a ≠ ⊥
⊢ a ≠ ⊥