-- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean
theorem tmul_comp_tensorAssoc
    (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃) :
    (Q₁.tmul (Q₂.tmul Q₃)).comp (TensorProduct.assoc R M₁ M₂ M₃) = (Q₁.tmul Q₂).tmul Q₃

Proof state:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
⊢ comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃) = (Q₁.tmul Q₂).tmul Q₃

Tactic:
refine (QuadraticMap.associated_rightInverse R).injective ?_

Result:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
⊢ (associatedHom R) (comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃)) =
    (associatedHom R) ((Q₁.tmul Q₂).tmul Q₃)

Proof state:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
⊢ (associatedHom R) (comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃)) =
    (associatedHom R) ((Q₁.tmul Q₂).tmul Q₃)

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

Result:
case a.a.h.h.h.a.a.h.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Invertible 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₃
⊢ (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              ((((TensorProduct.AlgebraTensorModule.curry
                      (TensorProduct.AlgebraTensorModule.curry
                        ((associatedHom R) (comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃)))))
                    m₁)
                  m₂)
                m₁')))
          m₂')
        m₁'')
      m₂'' =
    (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              ((((TensorProduct.AlgebraTensorModule.curry
                      (TensorProduct.AlgebraTensorModule.curry ((associatedHom R) ((Q₁.tmul Q₂).tmul Q₃))))
                    m₁)
                  m₂)
                m₁')))
          m₂')
        m₁'')
      m₂''

Proof state:
case a.a.h.h.h.a.a.h.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Invertible 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₃
⊢ (((associatedHom R) (comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃))) ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁'))
      ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'') =
    (((associatedHom R) ((Q₁.tmul Q₂).tmul Q₃)) ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁')) ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'')

Tactic:
simp only [associated_tmul, QuadraticMap.associated_comp]

Result:
case a.a.h.h.h.a.a.h.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Invertible 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₃
⊢ ((LinearMap.compl₁₂
          (LinearMap.BilinForm.tmul (associated Q₁) (LinearMap.BilinForm.tmul (associated Q₂) (associated Q₃)))
          ↑(TensorProduct.assoc R M₁ M₂ M₃) ↑(TensorProduct.assoc R M₁ M₂ M₃))
        ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁'))
      ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'') =
    ((LinearMap.BilinForm.tmul (LinearMap.BilinForm.tmul (associated Q₁) (associated Q₂)) (associated Q₃))
        ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁'))
      ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'')

Proof state:
case a.a.h.h.h.a.a.h.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Invertible 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₃
⊢ ((LinearMap.compl₁₂
          (LinearMap.BilinForm.tmul (associated Q₁) (LinearMap.BilinForm.tmul (associated Q₂) (associated Q₃)))
          ↑(TensorProduct.assoc R M₁ M₂ M₃) ↑(TensorProduct.assoc R M₁ M₂ M₃))
        ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁'))
      ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'') =
    ((LinearMap.BilinForm.tmul (LinearMap.BilinForm.tmul (associated Q₁) (associated Q₂)) (associated Q₃))
        ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁'))
      ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'')

Tactic:
exact mul_assoc _ _ _

Result:
no goals

Proof state:
case a.a.h.h.h.a.a.h.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Invertible 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₃
⊢ (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              ((((TensorProduct.AlgebraTensorModule.curry
                      (TensorProduct.AlgebraTensorModule.curry
                        ((associatedHom R) (comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃)))))
                    m₁)
                  m₂)
                m₁')))
          m₂')
        m₁'')
      m₂'' =
    (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              ((((TensorProduct.AlgebraTensorModule.curry
                      (TensorProduct.AlgebraTensorModule.curry ((associatedHom R) ((Q₁.tmul Q₂).tmul Q₃))))
                    m₁)
                  m₂)
                m₁')))
          m₂')
        m₁'')
      m₂''

Tactic:
dsimp [-associated_apply]

Result:
case a.a.h.h.h.a.a.h.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Invertible 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₃
⊢ (((associatedHom R) (comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃))) ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁'))
      ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'') =
    (((associatedHom R) ((Q₁.tmul Q₂).tmul Q₃)) ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁')) ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'')