From 400d126a38159c4ff810f1d8e584f6f500ad28df Mon Sep 17 00:00:00 2001
From: Christopher Hoskin <christopher.hoskin@gmail.com>
Date: Sun, 14 Apr 2024 14:15:01 +0000
Subject: [PATCH] refactor(LinearAlgebra/BilinearForm/Basic): Deprecate
 coercions (#12132)

Following #11278 the coercions in `LinearAlgebra/BilinearForm/Basic` are no longer useful. This PR deprecates them.
---
 Mathlib/LinearAlgebra/BilinearForm/Basic.lean | 10 ++++++----
 Mathlib/LinearAlgebra/BilinearForm/Hom.lean   |  4 +---
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/LinearAlgebra/BilinearForm/Basic.lean b/Mathlib/LinearAlgebra/BilinearForm/Basic.lean
index 765e2456b1cd97..33eb58648dfaea 100644
--- a/Mathlib/LinearAlgebra/BilinearForm/Basic.lean
+++ b/Mathlib/LinearAlgebra/BilinearForm/Basic.lean
@@ -64,6 +64,7 @@ namespace BilinForm
 
 #noalign bilin_form.coe_fn_mk
 
+@[deprecated]
 theorem coeFn_congr : ∀ {x x' y y' : M}, x = x' → y = y' → B x y = B x' y'
   | _, _, _, _, rfl, rfl => rfl
 #align bilin_form.coe_fn_congr LinearMap.BilinForm.coeFn_congr
@@ -122,10 +123,7 @@ theorem coe_injective : Function.Injective ((fun B x y => B x y) : BilinForm R M
 #align bilin_form.coe_injective LinearMap.BilinForm.coe_injective
 
 @[ext]
-theorem ext (H : ∀ x y : M, B x y = D x y) : B = D :=
-  coe_injective <| by
-    funext
-    exact H _ _
+theorem ext (H : ∀ x y : M, B x y = D x y) : B = D := ext₂ H
 #align bilin_form.ext LinearMap.BilinForm.ext
 
 theorem congr_fun (h : B = D) (x y : M) : B x y = D x y :=
@@ -136,6 +134,7 @@ theorem ext_iff : B = D ↔ ∀ x y, B x y = D x y :=
   ⟨congr_fun, ext₂⟩
 #align bilin_form.ext_iff LinearMap.BilinForm.ext_iff
 
+@[deprecated]
 theorem coe_zero : ⇑(0 : BilinForm R M) = 0 :=
   rfl
 #align bilin_form.coe_zero LinearMap.BilinForm.coe_zero
@@ -147,6 +146,7 @@ theorem zero_apply (x y : M) : (0 : BilinForm R M) x y = 0 :=
 
 variable (B D B₁ D₁)
 
+@[deprecated]
 theorem coe_add : ⇑(B + D) = B + D :=
   rfl
 #align bilin_form.coe_add LinearMap.BilinForm.coe_add
@@ -159,6 +159,7 @@ theorem add_apply (x y : M) : (B + D) x y = B x y + D x y :=
 #noalign bilin_form.coe_smul
 #noalign bilin_form.smul_apply
 
+@[deprecated]
 theorem coe_neg : ⇑(-B₁) = -B₁ :=
   rfl
 #align bilin_form.coe_neg LinearMap.BilinForm.coe_neg
@@ -168,6 +169,7 @@ theorem neg_apply (x y : M₁) : (-B₁) x y = -B₁ x y :=
   rfl
 #align bilin_form.neg_apply LinearMap.BilinForm.neg_apply
 
+@[deprecated]
 theorem coe_sub : ⇑(B₁ - D₁) = B₁ - D₁ :=
   rfl
 #align bilin_form.coe_sub LinearMap.BilinForm.coe_sub
diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean
index fc7f9ea65c6e6e..2914e658279621 100644
--- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean
+++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean
@@ -87,9 +87,7 @@ theorem sum_right {α} (t : Finset α) (w : M) (g : α → M) :
 
 theorem sum_apply {α} (t : Finset α) (B : α → BilinForm R M) (v w : M) :
     (∑ i in t, B i) v w = ∑ i in t, B i v w := by
-  show coeFnAddMonoidHom (∑ i in t, B i) v w = _
-  rw [map_sum, Finset.sum_apply, Finset.sum_apply]
-  rfl
+  simp only [coeFn_sum, Finset.sum_apply]
 
 variable {B}