refine ⟨RepFun.mk f (fun a ha ↦ by simp [hf, ha]) (fun a ha ↦ ?_) (fun a b hab ↦ ?_), fun a ↦ ?_⟩
α : 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
⊢ ∃ f, ∀ (x : ↑t), f ↑x = f₀ x
case refine_1
α : 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 : α
ha : a ∈ s
⊢ P.Rel a (f a)

case refine_2
α : 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 b : α
hab : P.Rel a b
⊢ f a = f b

case refine_3
α : 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
⊢ { toFun := f, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯, apply_eq_of_rel := ⋯ } ↑a = f₀ a