congr
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : CommSemiring A✝
inst✝¹³ : Algebra R✝ A✝
inst✝¹² : Invertible 2
R A M N T : Type
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup T
inst✝³ : Module A T
inst✝² : Module R T
inst✝¹ : IsScalarTower R A T
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ a * a * ↑(algebraMap R A) (⅟2 * (2 * 2 * ↑F m - ↑F m - ↑F m)) = a * a * ↑(algebraMap R A) (↑F m)
case e_a.h.e_6.h
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : CommSemiring A✝
inst✝¹³ : Algebra R✝ A✝
inst✝¹² : Invertible 2
R A M N T : Type
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup T
inst✝³ : Module A T
inst✝² : Module R T
inst✝¹ : IsScalarTower R A T
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ ⅟2 * (2 * 2 * ↑F m - ↑F m - ↑F m) = ↑F m