Commit 2025-06-28 22:01 78a26d50

chore: split WithLp.equiv into a new pair WithLp.toLp/WithLp.ofLp (#26459) (WithLp.equiv p _).symm v is very inconvenient as a normal form when working with WithLp. This introduces WithLp.toLp p v as the simp-normal spelling of this operation, and v'.ofLp as the simp-normal spelling of WithLp.equiv p _ v'. It then deprecates almost all the lemmas about WithLp.equiv, as these are no longer stated in simp-normal form. The motivation for making toLp and ofLp as plain functions, as opposed to Equivs, is to permit them to be later adapted into a constructor and projection of a one-field structure. Almost nothing in mathlib needs them to be equivs anyway. Zulip thread: [#mathlib4 > defeq abuse in `WithLp` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/defeq.20abuse.20in.20.60WithLp.60/near/516241777)