refactor(LinearAlgebra/BilinearForm/Basic): Derive the *_left and `…

…*_right` results from the `map_*₂` and `map_*` results (#12124)

Following #11278 a number of the results in `LinearAlgebra/BilinearForm/Basic` are just special cases of results in `LinearAlgebra/BilinearMap`.

Mathlib/LinearAlgebra/BilinearForm/Basic.lean

@@ -69,12 +69,10 @@ 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
 
-theorem add_left (x y z : M) : B (x + y) z = B x z + B y z := by
-  simp only [map_add, LinearMap.add_apply]
+theorem add_left (x y z : M) : B (x + y) z = B x z + B y z := map_add₂ _ _ _ _
 #align bilin_form.add_left LinearMap.BilinForm.add_left
 
-theorem smul_left (a : R) (x y : M) : B (a • x) y = a * B x y := by
-  simp only [map_smul, LinearMap.smul_apply, smul_eq_mul]
+theorem smul_left (a : R) (x y : M) : B (a • x) y = a * B x y := map_smul₂ _ _ _ _
 #align bilin_form.smul_left LinearMap.BilinForm.smul_left
 
 theorem add_right (x y z : M) : B x (y + z) = B x y + B x z := map_add _ _ _
@@ -83,28 +81,22 @@ theorem add_right (x y z : M) : B x (y + z) = B x y + B x z := map_add _ _ _
 theorem smul_right (a : R) (x y : M) : B x (a • y) = a * B x y := map_smul _ _ _
 #align bilin_form.smul_right LinearMap.BilinForm.smul_right
 
-theorem zero_left (x : M) : B 0 x = 0 := by
-  rw [← @zero_smul R _ _ _ _ (0 : M), smul_left, zero_mul]
+theorem zero_left (x : M) : B 0 x = 0 := map_zero₂ _ _
 #align bilin_form.zero_left LinearMap.BilinForm.zero_left
 
-theorem zero_right (x : M) : B x 0 = 0 := by
-  rw [← @zero_smul R _ _ _ _ (0 : M), smul_right, zero_mul]
+theorem zero_right (x : M) : B x 0 = 0 := map_zero _
 #align bilin_form.zero_right LinearMap.BilinForm.zero_right
 
-theorem neg_left (x y : M₁) : B₁ (-x) y = -B₁ x y := by
-  rw [← @neg_one_smul R₁ _ _, smul_left, neg_one_mul]
+theorem neg_left (x y : M₁) : B₁ (-x) y = -B₁ x y := map_neg₂ _ _ _
 #align bilin_form.neg_left LinearMap.BilinForm.neg_left
 
-theorem neg_right (x y : M₁) : B₁ x (-y) = -B₁ x y := by
-  rw [← @neg_one_smul R₁ _ _, smul_right, neg_one_mul]
+theorem neg_right (x y : M₁) : B₁ x (-y) = -B₁ x y := map_neg _ _
 #align bilin_form.neg_right LinearMap.BilinForm.neg_right
 
-theorem sub_left (x y z : M₁) : B₁ (x - y) z = B₁ x z - B₁ y z := by
-  rw [sub_eq_add_neg, sub_eq_add_neg, add_left, neg_left]
+theorem sub_left (x y z : M₁) : B₁ (x - y) z = B₁ x z - B₁ y z := map_sub₂ _ _ _ _
 #align bilin_form.sub_left LinearMap.BilinForm.sub_left
 
-theorem sub_right (x y z : M₁) : B₁ x (y - z) = B₁ x y - B₁ x z := by
-  rw [sub_eq_add_neg, sub_eq_add_neg, add_right, neg_right]
+theorem sub_right (x y z : M₁) : B₁ x (y - z) = B₁ x y - B₁ x z := map_sub _ _ _
 #align bilin_form.sub_right LinearMap.BilinForm.sub_right
 
 lemma smul_left_of_tower (r : S) (x y : M) : B (r • x) y = r • B x y := by
@@ -126,12 +118,10 @@ theorem coe_injective : Function.Injective ((fun B x y => B x y) : BilinForm R M
 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 :=
-  h ▸ rfl
+theorem congr_fun (h : B = D) (x y : M) : B x y = D x y := congr_fun₂ h _ _
 #align bilin_form.congr_fun LinearMap.BilinForm.congr_fun
 
-theorem ext_iff : B = D ↔ ∀ x y, B x y = D x y :=
-  ⟨congr_fun, ext₂⟩
+theorem ext_iff : B = D ↔ ∀ x y, B x y = D x y := ext_iff₂
 #align bilin_form.ext_iff LinearMap.BilinForm.ext_iff
 
 @[deprecated]