refactor(LinearAlgebra/BilinearForm/Basic): Delete infered instances (#…

…12122)

Following #11278 the instances in `LinearAlgebra/BilinearForm/Basic` can be infered without further proof, and therefore the instance statements are no longer required.

Mathlib/LinearAlgebra/BilinearForm/Basic.lean

@@ -136,8 +136,6 @@ 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
 
-instance : Zero (BilinForm R M) := inferInstance
-
 theorem coe_zero : ⇑(0 : BilinForm R M) = 0 :=
   rfl
 #align bilin_form.coe_zero LinearMap.BilinForm.coe_zero
@@ -149,8 +147,6 @@ theorem zero_apply (x y : M) : (0 : BilinForm R M) x y = 0 :=
 
 variable (B D B₁ D₁)
 
-instance : Add (BilinForm R M) := inferInstance
-
 theorem coe_add : ⇑(B + D) = B + D :=
   rfl
 #align bilin_form.coe_add LinearMap.BilinForm.coe_add
@@ -160,32 +156,9 @@ theorem add_apply (x y : M) : (B + D) x y = B x y + D x y :=
   rfl
 #align bilin_form.add_apply LinearMap.BilinForm.add_apply
 
-/-- `BilinForm R M` inherits the scalar action by `α` on `R` if this is compatible with
-multiplication.
-
-When `R` itself is commutative, this provides an `R`-action via `Algebra.id`. -/
-instance {α} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] : SMul α (BilinForm R M) :=
-  inferInstance
-
 #noalign bilin_form.coe_smul
 #noalign bilin_form.smul_apply
 
-instance {α β} [Monoid α] [Monoid β] [DistribMulAction α R] [DistribMulAction β R]
-    [SMulCommClass R α R] [SMulCommClass R β R] [SMulCommClass α β R] :
-    SMulCommClass α β (BilinForm R M) := inferInstance
-
-instance {α β} [Monoid α] [Monoid β] [SMul α β] [DistribMulAction α R] [DistribMulAction β R]
-    [SMulCommClass R α R] [SMulCommClass R β R] [IsScalarTower α β R] :
-    IsScalarTower α β (BilinForm R M) := inferInstance
-
-instance {α} [Monoid α] [DistribMulAction α R] [DistribMulAction αᵐᵒᵖ R]
-    [SMulCommClass R α R] [IsCentralScalar α R] :
-    IsCentralScalar α (BilinForm R M) := inferInstance
-
-instance : AddCommMonoid (BilinForm R M) := inferInstance
-
-instance : Neg (BilinForm R₁ M₁) := inferInstance
-
 theorem coe_neg : ⇑(-B₁) = -B₁ :=
   rfl
 #align bilin_form.coe_neg LinearMap.BilinForm.coe_neg
@@ -195,8 +168,6 @@ theorem neg_apply (x y : M₁) : (-B₁) x y = -B₁ x y :=
   rfl
 #align bilin_form.neg_apply LinearMap.BilinForm.neg_apply
 
-instance : Sub (BilinForm R₁ M₁) := inferInstance
-
 theorem coe_sub : ⇑(B₁ - D₁) = B₁ - D₁ :=
   rfl
 #align bilin_form.coe_sub LinearMap.BilinForm.coe_sub
@@ -206,23 +177,13 @@ theorem sub_apply (x y : M₁) : (B₁ - D₁) x y = B₁ x y - D₁ x y :=
   rfl
 #align bilin_form.sub_apply LinearMap.BilinForm.sub_apply
 
-instance : AddCommGroup (BilinForm R₁ M₁) := inferInstance
-
-instance : Inhabited (BilinForm R M) := inferInstance
-
 /-- `coeFn` as an `AddMonoidHom` -/
 def coeFnAddMonoidHom : BilinForm R M →+ M → M → R where
   toFun := (fun B x y => B x y)
   map_zero' := rfl
   map_add' _ _ := rfl
 #align bilin_form.coe_fn_add_monoid_hom LinearMap.BilinForm.coeFnAddMonoidHom
 
-instance {α} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] :
-    DistribMulAction α (BilinForm R M) := inferInstance
-
-instance {α} [CommSemiring α] [Module α R] [SMulCommClass R α R] : Module α (BilinForm R M) :=
-  inferInstance
-
 section flip
 
 /-- Auxiliary construction for the flip of a bilinear form, obtained by exchanging the left and