mathlib3

9e355305 - fix(order/lattice, tactic.simps): add missing `notation_class` attributes to `has_(bot,top,inf,sup,compl)` (#8381)

fix(order/lattice, tactic.simps): add missing `notation_class` attributes to `has_(bot,top,inf,sup,compl)` (#8381) From the docs for `simps`: > `@[notation_class]` should be added to all classes that define notation, like `has_mul` and > `has_zero`. This specifies that the projections that `@[simps]` used are the projections from > these notation classes instead of the projections of the superclasses. > Example: if `has_mul` is tagged with `@[notation_class]` then the projection used for `semigroup` > will be `λ α hα, @has_mul.mul α (@semigroup.to_has_mul α hα)` instead of `@semigroup.mul`.