mathlib3

84582d28 - feat(data/quot,data/set/basic): add lemmas about `lift` (#17699)

feat(data/quot,data/set/basic): add lemmas about `lift` (#17699) * Add `quot.surjective_lift`, `quotient.surjective_lift_on'`. * Mark `quot.lift_mk` as `simp`. * Add `set.range_quot_lift`, `set.range_quotient_lift`, `set.range_quotient_mk'`, and `set.range_quotient_lift_on'`. * The `mathlib4` version: leanprover-community/mathlib4#701. * Prove `matrix.to_linear_map₂_apply` by `rfl`.