Commit 2023-03-24 02:31 b531e74a

feat: elementwise linting checks, and putting into simp normal form (#2956) Some elementwise lemmas are completely trivial even without any simp lemmas, likely because coercions are being unfolded. We add some linting checks to let the user know they can omit the elementwise attribute. Also, elementwise doesn't necessarily put lemmas into simp normal form, which means @[elementwise (attr := simp)] can lead to failing the simpNF linter. Now by default elementwise will apply simp to the left-hand and right-hand sides of the lemma. Use @[elementwise nosimp] to override this.