Interplay of quotient types and subtypes

Stream: lean4

[Bernhard Reinke]

I am trying to understand the interplay of quotient types and subtypes. I am trying to define the following function

def Quotient.lift_subtype {α β} {s : Setoid α} (p : Quotient s -> Prop) (f : ∀ a, p ⟦a⟧→ β)
(eq : ∀ a a' h h', a ≈ a' → f a h = f a' h') : Subtype p -> β :=
fun ⟨t, h⟩  =>  Quotient.recOn t f (by
  sorry
) h

The idea is that I have a type α, some quotient defined by a setoid relation s, a predicate p on the quotient by s and a function f : ∀ a, p ⟦a⟧→ β that I want to push onto the subtype defined by p. It is a bit annoying that f is a dependent function, otherwise Quotient.lift or something like this would easily work. I think I have to use Quotient.recOn, but I don't fully understand it. Could someone please enlighten me?