-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (goal)
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₃
⊢ 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)
have a : 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: dsimp [-associated_apply]