Commit 2021-01-04 23:56 12921e9e

feat(tactic/simps): some improvements (#5541)

• @[simps] would previously fail if the definition is not a constructor application (with the suggestion to add option {rhs_md := semireducible} and maybe simp_rhs := tt). Now it automatically adds {rhs_md := semireducible, simp_rhs := tt} whenever it reaches this situation.
• Remove all (now) unnecessary occurrences of {rhs_md := semireducible} from the library. There are still a couple left where the simp_rhs := tt is undesirable.
• @[simps {simp_rhs := tt}] now also applies dsimp, simp to the right-hand side of the lemmas it generates.
• Add some @[simps] in category_theory/limits/cones.lean
• @[simps] would not recursively apply projections of prod or pprod. This is now customizable with the not_recursive option.
• Add an option trace.simps.debug with some debugging information.