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 `Equiv`s, 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)

Co-authored-by: Yael Dillies <yael.dillies@gmail.com>
Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Author: eric-wieser

Mathlib/Analysis/CStarAlgebra/Matrix.lean

@@ -36,8 +36,9 @@ coincide with the existing topology and uniformity on matrices.
 
 -/
 
-
+open WithLp
 open scoped Matrix
+
 variable {𝕜 m n l E : Type*}
 
 section EntrywiseSupNorm
@@ -113,15 +114,21 @@ lemma coe_toEuclideanCLM_eq_toEuclideanLin (A : Matrix n n 𝕜) :
   rfl
 
 @[simp]
+lemma toEuclideanCLM_toLp (A : Matrix n n 𝕜) (x : n → 𝕜) :
+    toEuclideanCLM (n := n) (𝕜 := 𝕜) A (toLp _ x) = toLp _ (A *ᵥ x) := rfl
+
+@[deprecated toEuclideanCLM_toLp (since := "2025-05-07")]
 lemma toEuclideanCLM_piLp_equiv_symm (A : Matrix n n 𝕜) (x : n → 𝕜) :
     toEuclideanCLM (n := n) (𝕜 := 𝕜) A ((WithLp.equiv _ _).symm x) =
-      (WithLp.equiv _ _).symm (A *ᵥ x) :=
-  rfl
+      (WithLp.equiv _ _).symm (A *ᵥ x) := rfl
 
 @[simp]
+lemma ofLp_toEuclideanCLM (A : Matrix n n 𝕜) (x : EuclideanSpace 𝕜 n) :
+    ofLp (toEuclideanCLM (n := n) (𝕜 := 𝕜) A x) = A *ᵥ ofLp x := rfl
+
+@[deprecated ofLp_toEuclideanCLM (since := "2025-05-07")]
 lemma piLp_equiv_toEuclideanCLM (A : Matrix n n 𝕜) (x : EuclideanSpace 𝕜 n) :
-    WithLp.equiv _ _ (toEuclideanCLM (n := n) (𝕜 := 𝕜) A x) =
-      A *ᵥ (WithLp.equiv _ _ x) :=
+    WithLp.equiv _ _ (toEuclideanCLM (n := n) (𝕜 := 𝕜) A x) = A *ᵥ (WithLp.equiv _ _ x) :=
   rfl
 
 /-- An auxiliary definition used only to construct the true `NormedAddCommGroup` (and `Metric`)

Mathlib/Analysis/Calculus/FDeriv/WithLp.lean

@@ -7,14 +7,13 @@ import Mathlib.Analysis.Calculus.FDeriv.Prod
 import Mathlib.Analysis.Calculus.FDeriv.Equiv
 import Mathlib.Analysis.Normed.Lp.PiLp
 
-
 /-!
 # Derivatives on `WithLp`
 -/
 
-section PiLp
+open ContinuousLinearMap PiLp WithLp
 
-open ContinuousLinearMap
+section PiLp
 
 variable {𝕜 ι : Type*} {E : ι → Type*} {H : Type*}
 variable [NontriviallyNormedField 𝕜] [NormedAddCommGroup H] [∀ i, NormedAddCommGroup (E i)]
@@ -55,29 +54,48 @@ theorem hasFDerivWithinAt_piLp :
 
 namespace PiLp
 
-theorem hasStrictFDerivAt_equiv (f : PiLp p E) :
-    HasStrictFDerivAt (WithLp.equiv p (∀ i, E i))
-      (PiLp.continuousLinearEquiv p 𝕜 _).toContinuousLinearMap f :=
+theorem hasStrictFDerivAt_ofLp (f : PiLp p E) :
+    HasStrictFDerivAt ofLp (continuousLinearEquiv p 𝕜 _).toContinuousLinearMap f :=
   .of_isLittleO <| (Asymptotics.isLittleO_zero _ _).congr_left fun _ => (sub_self _).symm
 
-theorem hasStrictFDerivAt_equiv_symm (f : PiLp p E) :
-    HasStrictFDerivAt (WithLp.equiv p (∀ i, E i)).symm
-      (PiLp.continuousLinearEquiv p 𝕜 _).symm.toContinuousLinearMap f :=
+@[deprecated hasStrictFDerivAt_ofLp (since := "2025-05-07")]
+theorem hasStrictFDerivAt_equiv (f : ∀ i, E i) :
+    HasStrictFDerivAt (WithLp.equiv p _)
+      (continuousLinearEquiv p 𝕜 _).toContinuousLinearMap f :=
+  hasStrictFDerivAt_ofLp _ f
+
+theorem hasStrictFDerivAt_toLp (f : ∀ i, E i) :
+    HasStrictFDerivAt (toLp p) (continuousLinearEquiv p 𝕜 _).symm.toContinuousLinearMap f :=
   .of_isLittleO <| (Asymptotics.isLittleO_zero _ _).congr_left fun _ => (sub_self _).symm
 
+@[deprecated hasStrictFDerivAt_toLp (since := "2025-05-07")]
+theorem hasStrictFDerivAt_equiv_symm (f : ∀ i, E i) :
+    HasStrictFDerivAt (WithLp.equiv p _).symm
+      (continuousLinearEquiv p 𝕜 _).symm.toContinuousLinearMap f :=
+  hasStrictFDerivAt_toLp _ f
+
 nonrec theorem hasStrictFDerivAt_apply (f : PiLp p E) (i : ι) :
     HasStrictFDerivAt (𝕜 := 𝕜) (fun f : PiLp p E => f i) (proj p E i) f :=
-  (hasStrictFDerivAt_apply i f).comp f (hasStrictFDerivAt_equiv (𝕜 := 𝕜) p f)
+  (hasStrictFDerivAt_apply i f).comp f (hasStrictFDerivAt_ofLp (𝕜 := 𝕜) p f)
+
+theorem hasFDerivAt_ofLp (f : PiLp p E) :
+    HasFDerivAt ofLp (continuousLinearEquiv p 𝕜 _).toContinuousLinearMap f :=
+  (hasStrictFDerivAt_ofLp p f).hasFDerivAt
 
+@[deprecated hasFDerivAt_ofLp (since := "2025-05-07")]
 theorem hasFDerivAt_equiv (f : PiLp p E) :
-    HasFDerivAt (WithLp.equiv p (∀ i, E i))
-      (PiLp.continuousLinearEquiv p 𝕜 _).toContinuousLinearMap f :=
-  (hasStrictFDerivAt_equiv p f).hasFDerivAt
-
-theorem hasFDerivAt_equiv_symm (f : PiLp p E) :
-    HasFDerivAt (WithLp.equiv p (∀ i, E i)).symm
-      (PiLp.continuousLinearEquiv p 𝕜 _).symm.toContinuousLinearMap f :=
-  (hasStrictFDerivAt_equiv_symm p f).hasFDerivAt
+    HasFDerivAt (WithLp.equiv _ _) (continuousLinearEquiv p 𝕜 _).toContinuousLinearMap f :=
+  hasFDerivAt_ofLp _ f
+
+theorem hasFDerivAt_toLp (f : ∀ i, E i) :
+    HasFDerivAt (toLp p) (continuousLinearEquiv p 𝕜 _).symm.toContinuousLinearMap f :=
+  (hasStrictFDerivAt_toLp p f).hasFDerivAt
+
+@[deprecated hasFDerivAt_toLp (since := "2025-05-07")]
+theorem hasFDerivAt_equiv_symm (f : ∀ i, E i) :
+    HasFDerivAt (WithLp.equiv _ _).symm
+      (continuousLinearEquiv p 𝕜 _).symm.toContinuousLinearMap f :=
+  hasFDerivAt_toLp _ f
 
 nonrec theorem hasFDerivAt_apply (f : PiLp p E) (i : ι) :
     HasFDerivAt (𝕜 := 𝕜) (fun f : PiLp p E => f i) (proj p E i) f :=

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -55,7 +55,7 @@ For consequences in infinite dimension (Hilbert bases, etc.), see the file
 
 
 open Real Set Filter RCLike Submodule Function Uniformity Topology NNReal ENNReal
-  ComplexConjugate DirectSum
+  ComplexConjugate DirectSum WithLp
 
 noncomputable section
 
@@ -109,27 +109,24 @@ open Lean Meta Elab Term Macro TSyntax PrettyPrinter.Delaborator SubExpr
 open Mathlib.Tactic (subscriptTerm)
 
 /-- Notation for vectors in Lp space. `!₂[x, y, ...]` is a shorthand for
-`(WithLp.equiv 2 _).symm ![x, y, ...]`, of type `EuclideanSpace _ (Fin _)`.
+`WithLp.toLp 2 ![x, y, ...]`, of type `EuclideanSpace _ (Fin _)`.
 
 This also works for other subscripts. -/
 syntax (name := PiLp.vecNotation) "!" noWs subscriptTerm noWs "[" term,* "]" : term
 macro_rules | `(!$p:subscript[$e:term,*]) => do
   -- override the `Fin n.succ` to a literal
   let n := e.getElems.size
-  `((WithLp.equiv $p <| ∀ _ : Fin $(quote n), _).symm ![$e,*])
+  `(WithLp.toLp $p (V := ∀ _ : Fin $(quote n), _) ![$e,*])
 
 /-- Unexpander for the `!₂[x, y, ...]` notation. -/
-@[app_delab DFunLike.coe]
+@[app_delab WithLp.toLp]
 def EuclideanSpace.delabVecNotation : Delab :=
-  whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 6 do
-    -- check that the `(WithLp.equiv _ _).symm` is present
-    let p : Term ← withAppFn <| withAppArg do
-      let_expr Equiv.symm _ _ e := ← getExpr | failure
-      let_expr WithLp.equiv _ _ := e | failure
-      withNaryArg 2 <| withNaryArg 0 <| delab
+  whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 3 do
+    -- check that the `WithLp.toLp _` is present
+    let p : Term ← withNaryArg 0 <| delab
     -- to be conservative, only allow subscripts which are numerals
     guard <| p matches `($_:num)
-    let `(![$elems,*]) := ← withAppArg delab | failure
+    let `(![$elems,*]) := ← withNaryArg 2 delab | failure
     `(!$p[$elems,*])
 
 end Notation
@@ -185,9 +182,12 @@ theorem finrank_euclideanSpace_fin {n : ℕ} :
     Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n := by simp
 
 theorem EuclideanSpace.inner_eq_star_dotProduct (x y : EuclideanSpace 𝕜 ι) :
-    ⟪x, y⟫ = WithLp.equiv _ _ y ⬝ᵥ star (WithLp.equiv _ _ x) :=
-  rfl
+    ⟪x, y⟫ = ofLp y ⬝ᵥ star (ofLp x) := rfl
+
+lemma EuclideanSpace.inner_toLp_toLp (x y : ι → 𝕜) :
+    ⟪toLp 2 x, toLp 2 y⟫ = dotProduct y (star x) := rfl
 
+@[deprecated EuclideanSpace.inner_toLp_toLp (since := "2024-04-27")]
 theorem EuclideanSpace.inner_piLp_equiv_symm (x y : ι → 𝕜) :
     ⟪(WithLp.equiv 2 _).symm x, (WithLp.equiv 2 _).symm y⟫ = y ⬝ᵥ star x :=
   rfl
@@ -247,22 +247,27 @@ variable [DecidableEq ι]
 /-- The vector given in euclidean space by being `a : 𝕜` at coordinate `i : ι` and `0 : 𝕜` at
 all other coordinates. -/
 def EuclideanSpace.single (i : ι) (a : 𝕜) : EuclideanSpace 𝕜 ι :=
-  (WithLp.equiv _ _).symm (Pi.single i a)
+  toLp _ (Pi.single i a)
 
-@[simp]
+@[simp] lemma EuclideanSpace.ofLp_single (i : ι) (a : 𝕜) : ofLp (single i a) = Pi.single i a := rfl
+
+@[deprecated EuclideanSpace.ofLp_single (since := "2024-04-27")]
 theorem WithLp.equiv_single (i : ι) (a : 𝕜) :
     WithLp.equiv _ _ (EuclideanSpace.single i a) = Pi.single i a :=
   rfl
 
 @[simp]
+lemma EuclideanSpace.toLp_single (i : ι) (a : 𝕜) : toLp _ (Pi.single i a) = single i a := rfl
+
+@[deprecated EuclideanSpace.toLp_single (since := "2024-04-27")]
 theorem WithLp.equiv_symm_single (i : ι) (a : 𝕜) :
     (WithLp.equiv _ _).symm (Pi.single i a) = EuclideanSpace.single i a :=
   rfl
 
 @[simp]
 theorem EuclideanSpace.single_apply (i : ι) (a : 𝕜) (j : ι) :
     (EuclideanSpace.single i a) j = ite (j = i) a 0 := by
-  rw [EuclideanSpace.single, WithLp.equiv_symm_pi_apply, ← Pi.single_apply i a j]
+  rw [EuclideanSpace.single, PiLp.toLp_apply, ← Pi.single_apply i a j]
 
 @[simp]
 theorem EuclideanSpace.single_eq_zero_iff {i : ι} {a : 𝕜} :
@@ -279,27 +284,27 @@ theorem EuclideanSpace.inner_single_right (i : ι) (a : 𝕜) (v : EuclideanSpac
 @[simp]
 theorem EuclideanSpace.norm_single (i : ι) (a : 𝕜) :
     ‖EuclideanSpace.single i (a : 𝕜)‖ = ‖a‖ :=
-  PiLp.norm_equiv_symm_single 2 (fun _ => 𝕜) i a
+  PiLp.norm_toLp_single 2 (fun _ => 𝕜) i a
 
 @[simp]
 theorem EuclideanSpace.nnnorm_single (i : ι) (a : 𝕜) :
     ‖EuclideanSpace.single i (a : 𝕜)‖₊ = ‖a‖₊ :=
-  PiLp.nnnorm_equiv_symm_single 2 (fun _ => 𝕜) i a
+  PiLp.nnnorm_toLp_single 2 (fun _ => 𝕜) i a
 
 @[simp]
 theorem EuclideanSpace.dist_single_same (i : ι) (a b : 𝕜) :
     dist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = dist a b :=
-  PiLp.dist_equiv_symm_single_same 2 (fun _ => 𝕜) i a b
+  PiLp.dist_toLp_single_same 2 (fun _ => 𝕜) i a b
 
 @[simp]
 theorem EuclideanSpace.nndist_single_same (i : ι) (a b : 𝕜) :
     nndist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = nndist a b :=
-  PiLp.nndist_equiv_symm_single_same 2 (fun _ => 𝕜) i a b
+  PiLp.nndist_toLp_single_same 2 (fun _ => 𝕜) i a b
 
 @[simp]
 theorem EuclideanSpace.edist_single_same (i : ι) (a b : 𝕜) :
     edist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = edist a b :=
-  PiLp.edist_equiv_symm_single_same 2 (fun _ => 𝕜) i a b
+  PiLp.edist_toLp_single_same 2 (fun _ => 𝕜) i a b
 
 /-- `EuclideanSpace.single` forms an orthonormal family. -/
 theorem EuclideanSpace.orthonormal_single :
@@ -370,7 +375,7 @@ instance instFunLike : FunLike (OrthonormalBasis ι 𝕜 E) ι E where
         rw [this, Pi.single_smul]
         replace h := congr_fun h i
         simp only [LinearEquiv.comp_coe, map_smul, LinearEquiv.coe_coe,
-          LinearEquiv.trans_apply, WithLp.linearEquiv_symm_apply, WithLp.equiv_symm_single,
+          LinearEquiv.trans_apply, WithLp.linearEquiv_symm_apply, EuclideanSpace.toLp_single,
           LinearIsometryEquiv.coe_symm_toLinearEquiv] at h ⊢
         rw [h]
 
@@ -593,18 +598,18 @@ theorem _root_.Pi.orthonormalBasis_apply {η : Type*} [Fintype η] [DecidableEq
     [∀ i, Fintype (ι i)] {𝕜 : Type*} [RCLike 𝕜] {E : η → Type*} [∀ i, NormedAddCommGroup (E i)]
     [∀ i, InnerProductSpace 𝕜 (E i)] (B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i))
     (j : (i : η) × (ι i)) :
-    Pi.orthonormalBasis B j = (WithLp.equiv _ _).symm (Pi.single _ (B j.fst j.snd)) := by
+    Pi.orthonormalBasis B j = toLp _ (Pi.single _ (B j.fst j.snd)) := by
   classical
   ext k
   obtain ⟨i, j⟩ := j
   simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
     LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
     LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
-    LinearIsometryEquiv.piLpCurry_apply, WithLp.equiv_single, WithLp.equiv_symm_pi_apply,
+    LinearIsometryEquiv.piLpCurry_apply, EuclideanSpace.ofLp_single, PiLp.toLp_apply,
     Sigma.curry_single (γ := fun _ _ => 𝕜)]
   obtain rfl | hi := Decidable.eq_or_ne i k
-  · simp only [Pi.single_eq_same, WithLp.equiv_symm_single, OrthonormalBasis.repr_symm_single]
-  · simp only [Pi.single_eq_of_ne' hi, WithLp.equiv_symm_zero, map_zero]
+  · simp only [Pi.single_eq_same, EuclideanSpace.toLp_single, OrthonormalBasis.repr_symm_single]
+  · simp only [Pi.single_eq_of_ne' hi, toLp_zero, map_zero]
 
 @[simp]
 theorem _root_.Pi.orthonormalBasis_repr {η : Type*} [Fintype η] {ι : η → Type*}
@@ -1079,26 +1084,44 @@ def toEuclideanLin : Matrix m n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[
       (WithLp.linearEquiv _ 𝕜 (m → 𝕜)).symm
 
 @[simp]
+lemma toEuclideanLin_toLp (A : Matrix m n 𝕜) (x : n → 𝕜) :
+    Matrix.toEuclideanLin A (toLp _ x) = toLp _ (Matrix.toLin' A x) := rfl
+
+@[deprecated toEuclideanLin_toLp (since := "2024-04-27")]
 theorem toEuclideanLin_piLp_equiv_symm (A : Matrix m n 𝕜) (x : n → 𝕜) :
     Matrix.toEuclideanLin A ((WithLp.equiv _ _).symm x) =
       (WithLp.equiv _ _).symm (A *ᵥ x) :=
   rfl
 
 @[simp]
+theorem piLp_ofLp_toEuclideanLin (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) :
+    ofLp (Matrix.toEuclideanLin A x) = Matrix.toLin' A (ofLp x) :=
+  rfl
+
+@[deprecated piLp_ofLp_toEuclideanLin (since := "2024-04-27")]
 theorem piLp_equiv_toEuclideanLin (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) :
     WithLp.equiv _ _ (Matrix.toEuclideanLin A x) = A *ᵥ (WithLp.equiv _ _ x) :=
   rfl
 
 theorem toEuclideanLin_apply (M : Matrix m n 𝕜) (v : EuclideanSpace 𝕜 n) :
-    toEuclideanLin M v = (WithLp.equiv 2 (m → 𝕜)).symm (M *ᵥ (WithLp.equiv 2 (n → 𝕜)) v) :=
-  rfl
+    toEuclideanLin M v = toLp _ (M *ᵥ ofLp v) := rfl
 
 @[simp]
+theorem ofLp_toEuclideanLin_apply (M : Matrix m n 𝕜) (v : EuclideanSpace 𝕜 n) :
+    ofLp (toEuclideanLin M v) = M *ᵥ ofLp v :=
+  rfl
+
+@[deprecated ofLp_toEuclideanLin_apply (since := "2024-04-27")]
 theorem piLp_equiv_toEuclideanLin_apply (M : Matrix m n 𝕜) (v : EuclideanSpace 𝕜 n) :
     WithLp.equiv 2 (m → 𝕜) (toEuclideanLin M v) = M *ᵥ WithLp.equiv 2 (n → 𝕜) v :=
   rfl
 
 @[simp]
+theorem toEuclideanLin_apply_piLp_toLp (M : Matrix m n 𝕜) (v : n → 𝕜) :
+    toEuclideanLin M (toLp _ v) = toLp _ (M *ᵥ v) :=
+  rfl
+
+@[deprecated toEuclideanLin_apply_piLp_toLp (since := "2024-04-27")]
 theorem toEuclideanLin_apply_piLp_equiv_symm (M : Matrix m n 𝕜) (v : n → 𝕜) :
     toEuclideanLin M ((WithLp.equiv 2 (n→ 𝕜)).symm v) = (WithLp.equiv 2 (m → 𝕜)).symm (M *ᵥ v) :=
   rfl
@@ -1116,8 +1139,7 @@ lemma toEuclideanLin_eq_toLin_orthonormal [Fintype m] :
 
 end Matrix
 
-local notation "⟪" x ", " y "⟫ₑ" =>
-  inner 𝕜 (Equiv.symm (WithLp.equiv 2 _) x) (Equiv.symm (WithLp.equiv 2 _) y)
+local notation "⟪" x ", " y "⟫ₑ" => inner 𝕜 (toLp 2 x) (toLp 2 y)
 
 /-- The inner product of a row of `A` and a row of `B` is an entry of `B * Aᴴ`. -/
 theorem inner_matrix_row_row [Fintype n] (A B : Matrix m n 𝕜) (i j : m) :
@@ -1127,7 +1149,7 @@ theorem inner_matrix_row_row [Fintype n] (A B : Matrix m n 𝕜) (i j : m) :
 /-- The inner product of a column of `A` and a column of `B` is an entry of `Aᴴ * B`. -/
 theorem inner_matrix_col_col [Fintype m] (A B : Matrix m n 𝕜) (i j : n) :
     ⟪Aᵀ i, Bᵀ j⟫ₑ = (Aᴴ * B) i j := by
-  simp_rw [EuclideanSpace.inner_piLp_equiv_symm, Matrix.mul_apply',
+  simp_rw [EuclideanSpace.inner_toLp_toLp, Matrix.mul_apply',
     Matrix.conjTranspose_apply, dotProduct_comm, Pi.star_def]
   rfl
 

Mathlib/Analysis/InnerProductSpace/ProdL2.lean

@@ -43,9 +43,7 @@ variable {E F}
 
 @[simp]
 theorem prod_inner_apply (x y : WithLp 2 (E × F)) :
-    ⟪x, y⟫_𝕜 =
-      ⟪(WithLp.equiv 2 (E × F) x).fst, (WithLp.equiv 2 (E × F) y).fst⟫_𝕜 +
-      ⟪(WithLp.equiv 2 (E × F) x).snd, (WithLp.equiv 2 (E × F) y).snd⟫_𝕜 := rfl
+    ⟪x, y⟫_𝕜 = ⟪(ofLp x).fst, (ofLp y).fst⟫_𝕜 + ⟪(ofLp x).snd, (ofLp y).snd⟫_𝕜 := rfl
 
 end WithLp
 
@@ -65,7 +63,7 @@ def prod (v : OrthonormalBasis ι₁ 𝕜 E) (w : OrthonormalBasis ι₂ 𝕜 F)
     · unfold Pairwise
       simp only [ne_eq, Basis.map_apply, Basis.prod_apply, LinearMap.coe_inl,
         OrthonormalBasis.coe_toBasis, LinearMap.coe_inr, WithLp.linearEquiv_symm_apply,
-        WithLp.prod_inner_apply, Equiv.apply_symm_apply, Sum.forall, Sum.elim_inl,
+        WithLp.prod_inner_apply, WithLp.ofLp_toLp, Sum.forall, Sum.elim_inl,
         Function.comp_apply, inner_zero_right, add_zero, Sum.elim_inr, zero_add, Sum.inl.injEq,
         reduceCtorEq, not_false_eq_true, inner_zero_left, imp_self, implies_true, and_true,
         Sum.inr.injEq, true_and]