-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
m₁ m₁' : M₁
a :
  Eq.{uR + 1} (α := R)
    (((((((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
                        QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                      (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
                    (comp Q₁ (↑(TensorProduct.rid R M₁) : M₁ ⊗[R] R →ₗ[R] M₁)) :
                  LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                (a : M₁ ⊗[R] R) → M₁ ⊗[R] R →ₗ[R] R)
              (m₁ ⊗ₜ[R] 1) :
            M₁ ⊗[R] R →ₗ[R] R) :
          (a : M₁ ⊗[R] R) → R)
        (m₁' ⊗ₜ[R] 1) :
      R)
    (((((((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
                        QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                      (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
                    (Q₁.tmul (R := R) (M₂ := R) QuadraticMap.sq) :
                  LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                (a : M₁ ⊗[R] R) → M₁ ⊗[R] R →ₗ[R] R)
              (m₁ ⊗ₜ[R] 1) :
            M₁ ⊗[R] R →ₗ[R] R) :
          (a : M₁ ⊗[R] R) → R)
        (m₁' ⊗ₜ[R] 1) :
      R)
⊢ Eq.{uR + 1} (α := R)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (((((TensorProduct.AlgebraTensorModule.curry
                                  (((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
                                        QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                                      (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
                                    (comp Q₁ (↑(TensorProduct.rid R M₁) : M₁ ⊗[R] R →ₗ[R] M₁))) :
                                M₁ →ₗ[R] R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R) :
                              (a : M₁) → R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R)
                            m₁ :
                          R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R) :
                        (a : R) → M₁ ⊗[R] R →ₗ[R] R)
                      1) :
                  M₁ →ₗ[R] R →ₗ[R] R) :
                (a : M₁) → R →ₗ[R] R)
              m₁' :
            R →ₗ[R] R) :
          (a : R) → R)
        1 :
      R)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (((((TensorProduct.AlgebraTensorModule.curry
                                  (((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
                                        QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                                      (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
                                    (Q₁.tmul (R := R) (M₂ := R) QuadraticMap.sq)) :
                                M₁ →ₗ[R] R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R) :
                              (a : M₁) → R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R)
                            m₁ :
                          R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R) :
                        (a : R) → M₁ ⊗[R] R →ₗ[R] R)
                      1) :
                  M₁ →ₗ[R] R →ₗ[R] R) :
                (a : M₁) → R →ₗ[R] R)
              m₁' :
            R →ₗ[R] R) :
          (a : R) → R)
        1 :
      R)

Tactic:
dsimp [-associated_apply]

Premises used: QuadraticMap.associated_apply