ext x
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
⊢ ⇑f = id
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
⊢ f x = id x