Function on an family of quotients

Stream: lean4

[Parth Shastri]

Is there a nice way to lift functions that operate on indexed families of quotients? My current code uses both classical and unsafe, and is very cumbersome to use once unfolded.

namespace Quot

variable {α : Sort u} {r : α → α → Prop} {β : Sort v} {γ : Sort w} (f : (β → α) → γ)

private unsafe def liftF.impl (_ : ∀ a b, (∀ x, mk r (a x) = mk r (b x)) → f a = f b) (q : β → Quot r) : γ :=
  f λ x => unsafeCast <| q x

@[implemented_by liftF.impl]
def liftF (c : ∀ a b, (∀ x, mk r (a x) = mk r (b x)) → f a = f b) (q : β → Quot r) : γ :=
  f λ x => Classical.choose (q x).exists_rep

theorem liftF_mk (c : ∀ a b, (∀ x, mk r (a x) = mk r (b x)) → f a = f b) (a : β → α) : liftF f c (λ x => mk r (a x)) = f a :=
  c _ a λ _ => Classical.choose_spec <| exists_rep _

Also, there there a way to write c as a variable? It seems that include from Lean 3 no longer works.

[Eric Wieser]

Yes, we have something like this in Lean 3, it's docs#quotient.fin_choice

[Eric Wieser]

port-status#data/fintype/quotient links to a relevant discussion

[Eric Wieser]

https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/quotient.2Elift_on_family/near/286096782