-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
m₁ : M₁
m₂ : M₂
m₁' : M₃
m₂' : M₁
m₁'' : M₂
m₂'' : M₃
a :
  Eq.{uR + 1} (α := R)
    ((((LinearMap.compl₁₂
                  (LinearMap.BilinForm.tmul
                    (((associated.{uR, uM₁, uR} (R := R) (M := M₁) (N := R) :
                          QuadraticMap R M₁ R →ₗ[R] LinearMap.BilinMap R M₁ R) :
                        (a : QuadraticMap R M₁ R) → LinearMap.BilinMap R M₁ R)
                      Q₁)
                    (LinearMap.BilinForm.tmul
                      (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) :
                            QuadraticMap R M₂ R →ₗ[R] LinearMap.BilinMap R M₂ R) :
                          (a : QuadraticMap R M₂ R) → LinearMap.BilinMap R M₂ R)
                        Q₂)
                      (((associated.{uR, uM₃, uR} (R := R) (M := M₃) (N := R) :
                            QuadraticMap R M₃ R →ₗ[R] LinearMap.BilinMap R M₃ R) :
                          (a : QuadraticMap R M₃ R) → LinearMap.BilinMap R M₃ R)
                        Q₃)))
                  (↑(TensorProduct.assoc R M₁ M₂ M₃) : M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃))
                  (↑(TensorProduct.assoc R M₁ M₂ M₃) : M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃)) :
                (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₁') :
            M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → R)
        (m₂' ⊗ₜ[R] m₁'' ⊗ₜ[R] m₂'') :
      R)
    ((((LinearMap.BilinForm.tmul
                  (LinearMap.BilinForm.tmul
                    (((associated.{uR, uM₁, uR} (R := R) (M := M₁) (N := R) :
                          QuadraticMap R M₁ R →ₗ[R] LinearMap.BilinMap R M₁ R) :
                        (a : QuadraticMap R M₁ R) → LinearMap.BilinMap R M₁ R)
                      Q₁)
                    (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) :
                          QuadraticMap R M₂ R →ₗ[R] LinearMap.BilinMap R M₂ R) :
                        (a : QuadraticMap R M₂ R) → LinearMap.BilinMap R M₂ R)
                      Q₂))
                  (((associated.{uR, uM₃, uR} (R := R) (M := M₃) (N := R) :
                        QuadraticMap R M₃ R →ₗ[R] LinearMap.BilinMap R M₃ R) :
                      (a : QuadraticMap R M₃ R) → LinearMap.BilinMap R M₃ R)
                    Q₃) :
                (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₁') :
            M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → R)
        (m₂' ⊗ₜ[R] m₁'' ⊗ₜ[R] m₂'') :
      R)
⊢ Eq.{uR + 1} (α := R)
    (((((((associatedHom R (R := R) (M := M₁ ⊗[R] M₂ ⊗[R] M₃) (N := R) :
                        QuadraticMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R) :
                      (a : QuadraticMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R)
                    (comp (Q₁.tmul (Q₂.tmul Q₃))
                      (↑(TensorProduct.assoc R M₁ M₂ M₃) : M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃))) :
                  LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R) :
                (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₁') :
            M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → R)
        (m₂' ⊗ₜ[R] m₁'' ⊗ₜ[R] m₂'') :
      R)
    (((((((associatedHom R (R := R) (M := M₁ ⊗[R] M₂ ⊗[R] M₃) (N := R) :
                        QuadraticMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R) :
                      (a : QuadraticMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R)
                    (QuadraticForm.tmul (Q₁.tmul Q₂) Q₃) :
                  LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R) :
                (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₁') :
            M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → R)
        (m₂' ⊗ₜ[R] m₁'' ⊗ₜ[R] m₂'') :
      R)

Tactic:
simp only [associated_tmul, QuadraticMap.associated_comp]

Premises used: QuadraticMap.associated_comp, QuadraticForm.associated_tmul