case H
S : Type u_3
R : Type u_1
R₁ : Type ?u.408596
M : Type u_2
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₁
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module R₁ M
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Invertible 2
B₁ : BilinForm R M
Q : QuadraticForm R M
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
x✝ y✝ : N
⊢ bilin (↑(associatedHom S) (comp Q f)) x✝ y✝ = bilin (BilinForm.comp (↑(associatedHom S) Q) f f) x✝ y✝
S : Type u_3
R : Type u_1
R₁ : Type ?u.408596
M : Type u_2
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₁
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module R₁ M
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Invertible 2
B₁ : BilinForm R M
Q : QuadraticForm R M
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
⊢ ↑(associatedHom S) (comp Q f) = BilinForm.comp (↑(associatedHom S) Q) f f
ext
no goals
case H
S : Type u_3
R : Type u_1
R₁ : Type ?u.408596
M : Type u_2
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₁
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module R₁ M
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Invertible 2
B₁ : BilinForm R M
Q : QuadraticForm R M
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
x✝ y✝ : N
⊢ bilin (↑(associatedHom S) (comp Q f)) x✝ y✝ = bilin (BilinForm.comp (↑(associatedHom S) Q) f f) x✝ y✝
simp only [QuadraticForm.comp_apply, BilinForm.comp_apply, associated_apply, LinearMap.map_add]