-- 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₃
a :
  ∀ (m₁ : M₁) (m₂ : M₂) (m₁' : M₃) (m₂' : M₁) (m₁'' : M₂) (m₂'' : M₃),
    Eq.{uR + 1} (α := R)
      (((((((TensorProduct.AlgebraTensorModule.curry
                            (TensorProduct.AlgebraTensorModule.curry
                              (((((((TensorProduct.AlgebraTensorModule.curry
                                                  (TensorProduct.AlgebraTensorModule.curry
                                                    (((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₃))))) :
                                                M₁ →ₗ[R] M₂ →ₗ[R] M₃ →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
                                              (a : M₁) → M₂ →ₗ[R] M₃ →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
                                            m₁ :
                                          M₂ →ₗ[R] M₃ →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
                                        (a : M₂) → M₃ →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
                                      m₂ :
                                    M₃ →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
                                  (a : M₃) → M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
                                m₁')) :
                          M₁ →ₗ[R] M₂ →ₗ[R] M₃ →ₗ[R] R) :
                        (a : M₁) → M₂ →ₗ[R] M₃ →ₗ[R] R)
                      m₂' :
                    M₂ →ₗ[R] M₃ →ₗ[R] R) :
                  (a : M₂) → M₃ →ₗ[R] R)
                m₁'' :
              M₃ →ₗ[R] R) :
            (a : M₃) → R)
          m₂'' :
        R)
      (((((((TensorProduct.AlgebraTensorModule.curry
                            (TensorProduct.AlgebraTensorModule.curry
                              (((((((TensorProduct.AlgebraTensorModule.curry
                                                  (TensorProduct.AlgebraTensorModule.curry
                                                    (((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₃))) :
                                                M₁ →ₗ[R] M₂ →ₗ[R] M₃ →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
                                              (a : M₁) → M₂ →ₗ[R] M₃ →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
                                            m₁ :
                                          M₂ →ₗ[R] M₃ →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
                                        (a : M₂) → M₃ →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
                                      m₂ :
                                    M₃ →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
                                  (a : M₃) → M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
                                m₁')) :
                          M₁ →ₗ[R] M₂ →ₗ[R] M₃ →ₗ[R] R) :
                        (a : M₁) → M₂ →ₗ[R] M₃ →ₗ[R] R)
                      m₂' :
                    M₂ →ₗ[R] M₃ →ₗ[R] R) :
                  (a : M₂) → M₃ →ₗ[R] R)
                m₁'' :
              M₃ →ₗ[R] R) :
            (a : M₃) → R)
          m₂'' :
        R)
⊢ Eq (α := LinearMap.BilinMap 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)
        (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)
    (((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)

Tactic:
ext m₁ m₂ m₁' m₂' m₁'' m₂''