Commit 2024-03-25 01:19 31188bc4

chore: remove unnecessary @[eqns] attributes (#11460) These attributes are unused in Mathlib. Many of them were workarounds for the now-resolved leanprover/lean4#2243; this also allows the lemmas themselves (hasFiniteIntegral_def, integrable_def, memℒp_def, and integrableOn_def) to be deleted. We are currently experiencing problems with the @[eqns] attribute on the Lean nightlies. I'm uncertain yet what the outcome is going to be there, but it seems prudent to reduce our unnecessary exposure to a language feature added in Mathlib.