-- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean
theorem comp_tensorRId_eq (Q₁ : QuadraticForm R M₁) :
    Q₁.comp (TensorProduct.rid R M₁) = Q₁.tmul (sq (R := R))

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.rid R M₁) = Q₁.tmul QuadraticMap.sq

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.rid R M₁)) = (associatedHom R) (Q₁.tmul QuadraticMap.sq)

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.rid R M₁) ↑(TensorProduct.rid R M₁)) (m₁ ⊗ₜ[R] 1))
      (m₁' ⊗ₜ[R] 1) =
    ((LinearMap.BilinForm.tmul (associated Q₁) (associated QuadraticMap.sq)) (m₁ ⊗ₜ[R] 1)) (m₁' ⊗ₜ[R] 1)

Tactic:
simp [-associated_apply, one_mul]

Result:
no goals

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.rid R M₁)))) m₁) 1))
        m₁')
      1 =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul QuadraticMap.sq))) m₁) 1))
        m₁')
      1

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.rid R M₁))) (m₁ ⊗ₜ[R] 1)) (m₁' ⊗ₜ[R] 1) =
    (((associatedHom R) (Q₁.tmul QuadraticMap.sq)) (m₁ ⊗ₜ[R] 1)) (m₁' ⊗ₜ[R] 1)

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.rid R M₁))) (m₁ ⊗ₜ[R] 1)) (m₁' ⊗ₜ[R] 1) =
    (((associatedHom R) (Q₁.tmul QuadraticMap.sq)) (m₁ ⊗ₜ[R] 1)) (m₁' ⊗ₜ[R] 1)

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.rid R M₁) ↑(TensorProduct.rid R M₁)) (m₁ ⊗ₜ[R] 1))
      (m₁' ⊗ₜ[R] 1) =
    ((LinearMap.BilinForm.tmul (associated Q₁) (associated QuadraticMap.sq)) (m₁ ⊗ₜ[R] 1)) (m₁' ⊗ₜ[R] 1)

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.rid R M₁)) = (associatedHom R) (Q₁.tmul QuadraticMap.sq)

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.rid R M₁)))) m₁) 1))
        m₁')
      1 =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul QuadraticMap.sq))) m₁) 1))
        m₁')
      1