Simps attribute

This file initializes notation classes and simps-projections for structures defined in the core library.

For documentation about simps, see Mathlib.Tactic.Simps.Basic.