feat: QuotLike

[FR-vdash-bot]

This typeclass is primarily for use by type synonyms of Quot and Quotient. Using QuotLike API for type synonyms of Quot and Quotient will avoid defeq abuse caused by directly using Quot and Quotient APIs.

---

Some of the naming may need to be discussed. For example, ⟦·⟧ is currently called mkQ in names. This distinguishes it from other .mks and makes it possible to write the quotient map as mkQ mkQ' mkQ_ h. But this will also require changing the old lemma names.

[github-actions]

PR summary f4ddcad285

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.QuotLike	100

---

Declarations diff

+ HasQuot
+ HasQuotHint
+ Hint
+ HintClass
+ Q
+ QuotLike
+ QuotLikeStruct
+ delabMkQ
+ eq
+ eq_iff_quotMk
+ eq_mkQ_iff_out
+ exact
+ exists_rep
+ hrecOn
+ hrecOn_mkQ
+ hrecOn₂
+ hrecOn₂_mkQ
+ ind
+ indep
+ indepCoherent
+ inductionOn
+ inductionOnPi
+ inductionOn₂
+ inductionOn₃
+ ind₂
+ ind₃
+ instance (p : Submodule R M) : QuotLike.Hint p (M ⧸ p) M p.quotientRel
+ instance (priority := 800)
+ instance (priority := 800) (f : α → Prop) [hf : DecidablePred f] (h : ∀ a b, r a b → f a = f b) :
+ instance (priority := 800) [Inhabited α] : Inhabited Q
+ instance (priority := 800) [IsEquiv α r] [dec : DecidableRel r] : DecidableEq Q
+ instance (priority := 800) [Nonempty α] : Nonempty Q
+ instance (priority := 800) [Subsingleton α] : Subsingleton Q
+ instance (priority := 800) [Unique α] : Unique Q := Unique.mk' _
+ instance : QuotLike (Q A B) B (HintClass.r A)
+ instance : QuotLike.HasQuot ZFSet PSet PSet.Equiv
+ instance : QuotLike.HasQuotHint A (Q A B) B (HintClass.r A)
+ lift
+ liftIndepPr1
+ liftOn
+ liftOn_mkQ
+ liftOn₂
+ liftOn₂'
+ liftOn₂'_mkQ
+ liftOn₂_mkQ
+ lift_comp_mkQ
+ lift_mkQ
+ lift₂
+ lift₂'
+ lift₂'_mkQ
+ lift₂_mkQ
+ map
+ map_mkQ
+ map₂
+ map₂_mkQ
+ mkQ'Impl
+ mkQ_Impl
+ mkQ_eq_iff_out
+ mkQ_eq_mkQ
+ mkQ_out
+ nonempty_quotient_iff
+ ofQuot
+ ofQuot_toQuot
+ out
+ out_inj
+ out_injective
+ out_mkQ_rel
+ out_rel_out
+ rec
+ recOn
+ recOnSubsingleton
+ recOnSubsingleton₂
+ rec_mkQ
+ rel_out_mkQ
+ sound
+ surjective_lift
+ surjective_liftOn
+ surjective_mkQ
+ toQuot_injective
+ toQuot_mkQ
+ toQuot_ofQuot
+ «exists»
+ «forall»
++ instQuotLike

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[urkud]

Why not just require an Equiv to Quot with default value of Equiv.refl _?

[FR-vdash-bot]

Mathlib.Logic.Equiv.Defs imports Mathlib.Data.Quot. I want QuotLike to import less.

[urkud]

It isn't clear what's the meaning of Hint.

[FR-vdash-bot]

Its full name is QuotLike.Hint. Is the explanation in the documentation string clear enough? If there is a better name, I can use it.