Commit 2023-03-08 15:13 b5daaa7b

feat: initialize_simps_projections automatically finds coercions (#2045)

• initialize_simps_projections automatically find coercions if there is a Funlike or SetLike instance defined by one of the projections.
• Some improvements compared to Lean 3:
  • Find coercions even if it is defined by a field of a parent structure
  • Find SetLike coercions Not yet implemented (and rarely - if ever - used in mathlib3):
• Automatic custom projections for algebraic notation (like +,*,...)