-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
a :
  ∀ (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂),
    Eq.{uR + 1} (α := R)
      (((((TensorProduct.AlgebraTensorModule.curry
                      (((((TensorProduct.AlgebraTensorModule.curry
                                    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₂) (N := R) :
                                          QuadraticMap R (M₁ ⊗[R] M₂) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₂) R) :
                                        (a : QuadraticMap R (M₁ ⊗[R] M₂) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₂) R)
                                      (comp (Q₂.tmul Q₁)
                                        (↑(TensorProduct.comm R M₁ M₂) : M₁ ⊗[R] M₂ →ₗ[R] M₂ ⊗[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
                                    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₂) (N := R) :
                                          QuadraticMap R (M₁ ⊗[R] M₂) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₂) R) :
                                        (a : QuadraticMap R (M₁ ⊗[R] M₂) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₂) R)
                                      (Q₁.tmul Q₂)) :
                                  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)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₂) (N := R) :
            QuadraticMap R (M₁ ⊗[R] M₂) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₂) R) :
          (a : QuadraticMap R (M₁ ⊗[R] M₂) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₂) R)
        (comp (Q₂.tmul Q₁) (↑(TensorProduct.comm R M₁ M₂) : M₁ ⊗[R] M₂ →ₗ[R] M₂ ⊗[R] M₁)) :
      LinearMap.BilinMap R (M₁ ⊗[R] M₂) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₂) (N := R) :
            QuadraticMap R (M₁ ⊗[R] M₂) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₂) R) :
          (a : QuadraticMap R (M₁ ⊗[R] M₂) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₂) R)
        (Q₁.tmul Q₂) :
      LinearMap.BilinMap R (M₁ ⊗[R] M₂) R)

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