-- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean
theorem comp_tensorLId_eq (Q₂ : QuadraticForm R M₂) :
    Q₂.comp (TensorProduct.lid R M₂) = QuadraticForm.tmul (sq (R := R)) Q₂

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

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

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

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

Tactic:
simp [-associated_apply, mul_one]

Result:
no goals

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

Tactic:
ext m₂ m₂'

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

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

Tactic:
simp only [associated_tmul, QuadraticMap.associated_comp]

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

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

Tactic:
dsimp [-associated_apply]

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