perf: make QuadraticForm.tensorDistrib noncomputable (#7265)

It's actually (trivially) computable, but Lean takes such an extraordinarily long time to compile it that its better to pretend that it isn't.

Another instance of #7103.

Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean

@@ -43,7 +43,8 @@ namespace CliffordAlgebra
 variable (A)
 
 /-- Auxiliary construction: note this is really just a heterobasic `CliffordAlgebra.map`. -/
-def ofBaseChangeAux (Q : QuadraticForm R V) :
+-- `noncomputable` is a performance workaround for mathlib4#7103
+noncomputable def ofBaseChangeAux (Q : QuadraticForm R V) :
     CliffordAlgebra Q →ₐ[R] CliffordAlgebra (Q.baseChange A) :=
   CliffordAlgebra.lift Q <| by
     refine ⟨(ι (Q.baseChange A)).restrictScalars R ∘ₗ TensorProduct.mk R A V 1, fun v => ?_⟩
@@ -57,7 +58,8 @@ def ofBaseChangeAux (Q : QuadraticForm R V) :
 
 /-- Convert from the base-changed clifford algebra to the clifford algebra over a base-changed
 module. -/
-def ofBaseChange (Q : QuadraticForm R V) :
+-- `noncomputable` is a performance workaround for mathlib4#7103
+noncomputable def ofBaseChange (Q : QuadraticForm R V) :
     A ⊗[R] CliffordAlgebra Q →ₐ[A] CliffordAlgebra (Q.baseChange A) :=
   Algebra.TensorProduct.algHomOfLinearMapTensorProduct
     (TensorProduct.AlgebraTensorModule.lift <|
@@ -88,7 +90,8 @@ def ofBaseChange (Q : QuadraticForm R V) :
 
 /-- Convert from the clifford algebra over a base-changed module to the base-changed clifford
 algebra. -/
-def toBaseChange (Q : QuadraticForm R V) :
+-- `noncomputable` is a performance workaround for mathlib4#7103
+noncomputable def toBaseChange (Q : QuadraticForm R V) :
     CliffordAlgebra (Q.baseChange A) →ₐ[A] A ⊗[R] CliffordAlgebra Q :=
   CliffordAlgebra.lift _ <| by
     refine ⟨TensorProduct.AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) (ι Q), ?_⟩
@@ -192,7 +195,8 @@ base-changing the clifford algebra itself; <|Cℓ(A ⊗_R V, Q_A) ≅ A ⊗_R C
 
 This is `CliffordAlgebra.toBaseChange` and `CliffordAlgebra.ofBaseChange` as an equivalence. -/
 @[simps!]
-def equivBaseChange (Q : QuadraticForm R V) :
+-- `noncomputable` is a performance workaround for mathlib4#7103
+noncomputable def equivBaseChange (Q : QuadraticForm R V) :
     CliffordAlgebra (Q.baseChange A) ≃ₐ[A] A ⊗[R] CliffordAlgebra Q :=
   AlgEquiv.ofAlgHom (toBaseChange A Q) (ofBaseChange A Q)
     (toBaseChange_comp_ofBaseChange A Q)

Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

@@ -37,7 +37,9 @@ variable (R A) in
 
 Note this is heterobasic; the quadratic form on the left can take values in a larger ring than
 the one on the right. -/
-def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) :=
+-- `noncomputable` is a performance workaround for mathlib4#7103
+noncomputable def tensorDistrib :
+    QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) :=
   letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
   -- while `letI`s would produce a better term than `let`, they would make this already-slow
   -- definition even slower.
@@ -58,7 +60,8 @@ theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R
     (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _)
 
 /-- The tensor product of two quadratic forms, a shorthand for dot notation. -/
-protected abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
+-- `noncomputable` is a performance workaround for mathlib4#7103
+protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
     QuadraticForm A (M₁ ⊗[R] M₂) :=
   tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂)
 
@@ -78,7 +81,8 @@ theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂
 
 variable (A) in
 /-- The base change of a quadratic form. -/
-protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) :=
+-- `noncomputable` is a performance workaround for mathlib4#7103
+protected noncomputable def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) :=
   QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq (R := A)) Q
 
 @[simp]