case H
S : Type ?u.466182
R : Type ?u.466185
R₁ : Type u_1
M : Type u_2
inst✝³ : CommRing R₁
inst✝² : AddCommGroup M
inst✝¹ : Module R₁ M
inst✝ : Invertible 2
f g : M →ₗ[R₁] R₁
x✝ y✝ : M
⊢ bilin (↑associated (linMulLin f g)) x✝ y✝ = bilin (⅟2 • (BilinForm.linMulLin f g + BilinForm.linMulLin g f)) x✝ y✝
S : Type ?u.466182
R : Type ?u.466185
R₁ : Type u_1
M : Type u_2
inst✝³ : CommRing R₁
inst✝² : AddCommGroup M
inst✝¹ : Module R₁ M
inst✝ : Invertible 2
f g : M →ₗ[R₁] R₁
⊢ ↑associated (linMulLin f g) = ⅟2 • (BilinForm.linMulLin f g + BilinForm.linMulLin g f)
ext
case H
S : Type ?u.466182
R : Type ?u.466185
R₁ : Type u_1
M : Type u_2
inst✝³ : CommRing R₁
inst✝² : AddCommGroup M
inst✝¹ : Module R₁ M
inst✝ : Invertible 2
f g : M →ₗ[R₁] R₁
x✝ y✝ : M
⊢ ⅟2 * ((↑f x✝ + ↑f y✝) * (↑g x✝ + ↑g y✝) - ↑f x✝ * ↑g x✝ - ↑f y✝ * ↑g y✝) = ⅟2 * (↑f x✝ * ↑g y✝) + ⅟2 * (↑g x✝ * ↑f y✝)
case H
S : Type ?u.466182
R : Type ?u.466185
R₁ : Type u_1
M : Type u_2
inst✝³ : CommRing R₁
inst✝² : AddCommGroup M
inst✝¹ : Module R₁ M
inst✝ : Invertible 2
f g : M →ₗ[R₁] R₁
x✝ y✝ : M
⊢ bilin (↑associated (linMulLin f g)) x✝ y✝ = bilin (⅟2 • (BilinForm.linMulLin f g + BilinForm.linMulLin g f)) x✝ y✝
simp only [smul_add, Algebra.id.smul_eq_mul, BilinForm.linMulLin_apply,
  QuadraticForm.linMulLin_apply, BilinForm.smul_apply, associated_apply, BilinForm.add_apply,
  LinearMap.map_add]
no goals
case H
S : Type ?u.466182
R : Type ?u.466185
R₁ : Type u_1
M : Type u_2
inst✝³ : CommRing R₁
inst✝² : AddCommGroup M
inst✝¹ : Module R₁ M
inst✝ : Invertible 2
f g : M →ₗ[R₁] R₁
x✝ y✝ : M
⊢ ⅟2 * ((↑f x✝ + ↑f y✝) * (↑g x✝ + ↑g y✝) - ↑f x✝ * ↑g x✝ - ↑f y✝ * ↑g y✝) = ⅟2 * (↑f x✝ * ↑g y✝) + ⅟2 * (↑g x✝ * ↑f y✝)
ring