Quotient of Pi type equivalent to Pi of quotient type

Stream: Is there code for X?

[Praneeth Kolichala]

I see there is a pi_setoid (https://github.com/leanprover-community/mathlib/blob/93047c523782a1cf6d1e96dc55beeab88c63d0ab/src/data/quot.lean#L252) in mathlib, but the natural followup would be something like:

lemma pi_quotient_equiv_quotient_pi
  {I : Type} {α : I → Type} [∀ i, setoid (α i)] :
  (Π i, @quotient (α i) infer_instance) ≃ @quotient (Π i, (α i)) infer_instance
  := sorry

Does such a thing exist? If not, I'm having trouble writing it; I want a function which descends to the quotient within a pi type, but I don't know how to do that without already having something like this function.

In other words, if you have a function $f : \left(\Pi_i \beta_i\right) \ \rightarrow \gamma$ such that $f$ depends on each coordinate of the input only up to some equivalence relation $\sim_i$, how do you descend to $f: \left(\Pi_i (\beta_i/\sim_i)\right)\rightarrow \gamma$?