feat(data/quot): Add quotient pi induction (#11137)

I am planning to use this later to show that the (pi) product of homotopy classes of paths is well-defined, and prove
properties about that product. 



Co-authored-by: prakol16 <prakol16@users.noreply.github.com>

src/data/quot.lean

@@ -249,6 +249,8 @@ by rw [← quotient.eq_mk_iff_out, quotient.out_eq]
   x.out = y.out ↔ x = y :=
 ⟨λ h, quotient.out_equiv_out.1 $ h ▸ setoid.refl _, λ h, h ▸ rfl⟩
 
+section pi
+
 instance pi_setoid {ι : Sort*} {α : ι → Sort*} [∀ i, setoid (α i)] : setoid (Π i, α i) :=
 { r := λ a b, ∀ i, a i ≈ b i,
   iseqv := ⟨
@@ -262,10 +264,21 @@ noncomputable def quotient.choice {ι : Type*} {α : ι → Type*} [S : Π i, se
   (f : Π i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=
 ⟦λ i, (f i).out⟧
 
-theorem quotient.choice_eq {ι : Type*} {α : ι → Type*} [Π i, setoid (α i)]
+@[simp] theorem quotient.choice_eq {ι : Type*} {α : ι → Type*} [Π i, setoid (α i)]
   (f : Π i, α i) : quotient.choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
 quotient.sound $ λ i, quotient.mk_out _
 
+@[elab_as_eliminator] lemma quotient.induction_on_pi
+   {ι : Type*} {α : ι → Sort*} [s : ∀ i, setoid (α i)]
+   {p : (Π i, quotient (s i)) → Prop} (f : Π i, quotient (s i))
+   (h : ∀ a : Π i, α i, p (λ i, ⟦a i⟧)) : p f :=
+begin
+  rw ← (funext (λ i, quotient.out_eq (f i)) : (λ i,  ⟦(f i).out⟧) = f),
+  apply h,
+end
+
+end pi
+
 lemma nonempty_quotient_iff (s : setoid α) : nonempty (quotient s) ↔ nonempty α :=
 ⟨assume ⟨a⟩, quotient.induction_on a nonempty.intro, assume ⟨a⟩, ⟨⟦a⟧⟩⟩