-- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
theorem associated_tmul [Invertible (2 : A)]
    (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) :
    (Q₁.tmul Q₂).associated = Q₁.associated.tmul Q₂.associated

Proof state:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing A
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : AddCommGroup M₂
inst✝¹³ : AddCommGroup N₁
inst✝¹² : AddCommGroup N₂
inst✝¹¹ : Algebra R A
inst✝¹⁰ : Module R M₁
inst✝⁹ : Module A M₁
inst✝⁸ : Module R N₁
inst✝⁷ : Module A N₁
inst✝⁶ : SMulCommClass R A M₁
inst✝⁵ : IsScalarTower R A M₁
inst✝⁴ : IsScalarTower R A N₁
inst✝³ : Module R M₂
inst✝² : Module R N₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
⊢ associated (Q₁.tmul Q₂) = (associated Q₁).tmul (associated Q₂)

Tactic:
rw [QuadraticMap.tmul, BilinMap.tmul]

Result:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing A
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : AddCommGroup M₂
inst✝¹³ : AddCommGroup N₁
inst✝¹² : AddCommGroup N₂
inst✝¹¹ : Algebra R A
inst✝¹⁰ : Module R M₁
inst✝⁹ : Module A M₁
inst✝⁸ : Module R N₁
inst✝⁷ : Module A N₁
inst✝⁶ : SMulCommClass R A M₁
inst✝⁵ : IsScalarTower R A M₁
inst✝⁴ : IsScalarTower R A N₁
inst✝³ : Module R M₂
inst✝² : Module R N₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
⊢ associated ((tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)) = (BilinMap.tensorDistrib R A) (associated Q₁ ⊗ₜ[R] associated Q₂)

Proof state:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing A
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : AddCommGroup M₂
inst✝¹³ : AddCommGroup N₁
inst✝¹² : AddCommGroup N₂
inst✝¹¹ : Algebra R A
inst✝¹⁰ : Module R M₁
inst✝⁹ : Module A M₁
inst✝⁸ : Module R N₁
inst✝⁷ : Module A N₁
inst✝⁶ : SMulCommClass R A M₁
inst✝⁵ : IsScalarTower R A M₁
inst✝⁴ : IsScalarTower R A N₁
inst✝³ : Module R M₂
inst✝² : Module R N₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
⊢ associated (Q₁.tmul Q₂) = (associated Q₁).tmul (associated Q₂)

Tactic:
letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm

Result:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing A
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : AddCommGroup M₂
inst✝¹³ : AddCommGroup N₁
inst✝¹² : AddCommGroup N₂
inst✝¹¹ : Algebra R A
inst✝¹⁰ : Module R M₁
inst✝⁹ : Module A M₁
inst✝⁸ : Module R N₁
inst✝⁷ : Module A N₁
inst✝⁶ : SMulCommClass R A M₁
inst✝⁵ : IsScalarTower R A M₁
inst✝⁴ : IsScalarTower R A N₁
inst✝³ : Module R M₂
inst✝² : Module R N₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
⊢ associated (Q₁.tmul Q₂) = (associated Q₁).tmul (associated Q₂)

Proof state:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing A
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : AddCommGroup M₂
inst✝¹³ : AddCommGroup N₁
inst✝¹² : AddCommGroup N₂
inst✝¹¹ : Algebra R A
inst✝¹⁰ : Module R M₁
inst✝⁹ : Module A M₁
inst✝⁸ : Module R N₁
inst✝⁷ : Module A N₁
inst✝⁶ : SMulCommClass R A M₁
inst✝⁵ : IsScalarTower R A M₁
inst✝⁴ : IsScalarTower R A N₁
inst✝³ : Module R M₂
inst✝² : Module R N₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
⊢ associated ((tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)) = (BilinMap.tensorDistrib R A) (associated Q₁ ⊗ₜ[R] associated Q₂)

Tactic:
have : Subsingleton (Invertible (2 : A)) := inferInstance

Result:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing A
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : AddCommGroup M₂
inst✝¹³ : AddCommGroup N₁
inst✝¹² : AddCommGroup N₂
inst✝¹¹ : Algebra R A
inst✝¹⁰ : Module R M₁
inst✝⁹ : Module A M₁
inst✝⁸ : Module R N₁
inst✝⁷ : Module A N₁
inst✝⁶ : SMulCommClass R A M₁
inst✝⁵ : IsScalarTower R A M₁
inst✝⁴ : IsScalarTower R A N₁
inst✝³ : Module R M₂
inst✝² : Module R N₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Subsingleton (Invertible 2)
⊢ associated ((tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)) = (BilinMap.tensorDistrib R A) (associated Q₁ ⊗ₜ[R] associated Q₂)

Proof state:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing A
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : AddCommGroup M₂
inst✝¹³ : AddCommGroup N₁
inst✝¹² : AddCommGroup N₂
inst✝¹¹ : Algebra R A
inst✝¹⁰ : Module R M₁
inst✝⁹ : Module A M₁
inst✝⁸ : Module R N₁
inst✝⁷ : Module A N₁
inst✝⁶ : SMulCommClass R A M₁
inst✝⁵ : IsScalarTower R A M₁
inst✝⁴ : IsScalarTower R A N₁
inst✝³ : Module R M₂
inst✝² : Module R N₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Subsingleton (Invertible 2)
⊢ associated ((tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)) = (BilinMap.tensorDistrib R A) (associated Q₁ ⊗ₜ[R] associated Q₂)

Tactic:
convert associated_left_inverse A (LinearMap.BilinMap.tmul_isSymm
  (QuadraticMap.associated_isSymm A Q₁) (QuadraticMap.associated_isSymm R Q₂))

Result:
no goals