feat(data/quot): Add quotient pi induction (#11137)
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 <9aae9d5de72d411a786fadd8f8c49164a0ec757a@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib