-- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean
theorem tmul_comp_tensorMap
    {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂}
    {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄}
    (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) :
    (Q₂.tmul Q₄).comp (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃

Proof state:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R 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₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
⊢ (associatedHom R) (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap)) = (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₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R 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₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
m₁ : M₁
m₃ : M₃
m₁' : M₁
m₃' : M₃
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry
                ((associatedHom R) (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap))))
              m₁)
            m₃))
        m₁')
      m₃' =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul Q₃))) m₁) m₃))
        m₁')
      m₃'

Proof state:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R 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₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
⊢ comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃

Tactic:
have h₁ : Q₁ = Q₂.comp f.toLinearMap := QuadraticMap.ext fun x => (f.map_app x).symm

Result:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R 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₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
⊢ comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃

Proof state:
case a.h.h.a.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R 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₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
m₁ : M₁
m₃ : M₃
m₁' : M₁
m₃' : M₃
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry
                ((associatedHom R) (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap))))
              m₁)
            m₃))
        m₁')
      m₃' =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul Q₃))) m₁) m₃))
        m₁')
      m₃'

Tactic:
simp [-associated_apply, h₁, h₃, associated_tmul]

Result:
no goals

Proof state:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R 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₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
⊢ comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃

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

Result:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R 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₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
⊢ (associatedHom R) (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap)) = (associatedHom R) (Q₁.tmul Q₃)

Proof state:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R 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₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
⊢ comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃

Tactic:
have h₃ : Q₃ = Q₄.comp g.toLinearMap := QuadraticMap.ext fun x => (g.map_app x).symm

Result:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R 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₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
⊢ comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃