-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (goal)
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₂
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)
have a : Eq.{uR + 1} (α := 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) :
              (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
            (m₁ ⊗ₜ[R] m₂) :
          M₁ ⊗[R] M₂ →ₗ[R] R) :
        (a : M₁ ⊗[R] M₂) → 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) :
              (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
            (m₁ ⊗ₜ[R] m₂) :
          M₁ ⊗[R] M₂ →ₗ[R] R) :
        (a : M₁ ⊗[R] M₂) → R)
      (m₁' ⊗ₜ[R] m₂') :
    R)
Tactic: dsimp [-associated_apply]