exact Eq.symm <| h_eq _ _ h.choose_spec
case pos
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P✝ P : Partition s
t : Set α
f₀ : ↑t → α
h_not_mem : ∀ (x : ↑t), ↑x ∉ s → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ s → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a => if ha : a ∈ s then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hf : f = fun a => if ha : a ∈ s then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : ↑t
ha : ↑a ∈ s
h : ∃ b, P.Rel ↑a ↑b
⊢ f₀ h.choose = f₀ a
no goals