Theorem: IMOSL.Extra.SquareLike.two_nsmul_BilinMap_eq (IMOSLLean4/Extra/SquareLike.lean)

State before:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : ∀ (x y : G), f (x + y) + f (x - y) = 2 • (f x + f y)
x y : G
⊢ 2 • ((BilinMap hH h) x) y = f (x + y) - f (x - y)
Tactic:
rw [BilinMap_def, nsmul_sub, ← h, two_nsmul, add_sub_add_left_eq_sub]
State after:
no goals