Commit 2022-11-20 06:21 13b5722b

fix(Tactic/Simps): use capital letter for namespace (#647)

• Custom simps projections now are declared as def MyStructure.Simps.myProjection instead of def MyStructure.simps.myProjection. This declaration was already used in the library multiple times, even though it did nothing before.
• Use symm_apply instead of symmApply for lemmas generated by simps.
• Remove custom simps projection for Subtype. It did nothing, since coercions expand to Subtype.val. (Do we also want to rename the generated lemmas to foo_val instead of foo_coe?)
• Simplify some proofs using definitional eta for structures