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

Proof state:
case a.h.h.a.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry
                ((associatedHom R) (comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂))))
              m₁)
            m₂))
        m₁')
      m₂' =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul Q₂))) m₁) m₂))
        m₁')
      m₂'

Tactic:
dsimp [-associated_apply]

Result:
case a.h.h.a.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ (((associatedHom R) (comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂))) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') =
    (((associatedHom R) (Q₁.tmul Q₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂')

Proof state:
case a.h.h.a.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ (((associatedHom R) (comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂))) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') =
    (((associatedHom R) (Q₁.tmul Q₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂')

Tactic:
simp only [associated_tmul, QuadraticMap.associated_comp]

Result:
case a.h.h.a.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ ((LinearMap.compl₁₂ (LinearMap.BilinForm.tmul (associated Q₂) (associated Q₁)) ↑(TensorProduct.comm R M₁ M₂)
          ↑(TensorProduct.comm R M₁ M₂))
        (m₁ ⊗ₜ[R] m₂))
      (m₁' ⊗ₜ[R] m₂') =
    ((LinearMap.BilinForm.tmul (associated Q₁) (associated Q₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂')

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

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

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

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

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

Result:
case a.h.h.a.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry
                ((associatedHom R) (comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂))))
              m₁)
            m₂))
        m₁')
      m₂' =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul Q₂))) m₁) m₂))
        m₁')
      m₂'

Proof state:
case a.h.h.a.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ ((LinearMap.compl₁₂ (LinearMap.BilinForm.tmul (associated Q₂) (associated Q₁)) ↑(TensorProduct.comm R M₁ M₂)
          ↑(TensorProduct.comm R M₁ M₂))
        (m₁ ⊗ₜ[R] m₂))
      (m₁' ⊗ₜ[R] m₂') =
    ((LinearMap.BilinForm.tmul (associated Q₁) (associated Q₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂')

Tactic:
exact mul_comm _ _

Result:
no goals