diff --git a/Mathlib/LinearAlgebra/BilinearForm/Properties.lean b/Mathlib/LinearAlgebra/BilinearForm/Properties.lean
index bd6b0a757a293..1608da83a02f1 100644
--- a/Mathlib/LinearAlgebra/BilinearForm/Properties.lean
+++ b/Mathlib/LinearAlgebra/BilinearForm/Properties.lean
@@ -539,9 +539,8 @@ theorem comp_symmCompOfNondegenerate_apply (B₁ : BilinForm K V) {B₂ : BilinF
 @[simp]
 theorem symmCompOfNondegenerate_left_apply (B₁ : BilinForm K V) {B₂ : BilinForm K V}
     (b₂ : B₂.Nondegenerate) (v w : V) : B₂ (symmCompOfNondegenerate B₁ B₂ b₂ w) v = B₁ w v := by
-  conv_lhs => rw [← BilinForm.toLin_apply, comp_symmCompOfNondegenerate_apply]
-  rfl
-#align bilin_form.symm_comp_of_nondegenerate_left_apply BilinForm.symmCompOfNondegenerate_left_apply
+  conv_lhs => rw [comp_symmCompOfNondegenerate_apply]
+#align bilin_form.symm_comp_of_nondegenerate_left_apply LinearMap.BilinForm.symmCompOfNondegenerate_left_apply
 
 /-- Given the nondegenerate bilinear form `B` and the linear map `φ`,
 `leftAdjointOfNondegenerate` provides the left adjoint of `φ` with respect to `B`.