simpa using P.exists_extend_partial_repFun (fun x : t ↦ x) (by simp)
  (by simp [P.rel_self_iff_mem]) (fun x y ↦ h x.2 y.2)
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
t : Set α
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y
⊢ ∃ f, EqOn (⇑f) id t
no goals