chore(data/quot): Add missing simp lemmas (#5372)
chore(data/quot): Add missing simp lemmas (#5372)

These are called `lift_on'_beta` for consistency with `lift_on_beta`; even though we also have `map_mk'` etc in the same file.





leanprover-community/mathlib,leanprover-community/mathlib