obtain ⟨f, -⟩ := P.exists_extend_partial_repFun' (t := ∅) (by simp)
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
⊢ Nonempty P.RepFun
case intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
f : P.RepFun
⊢ Nonempty P.RepFun