Theorem: IMOSL.Extra.SquareLike.BilinMap_eq_two_nsmul (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 : G
⊢ ((BilinMap hH h) x) x = 2 • f x
Tactic:
rw [two_nsmul, ← neg_inj, ← map_neg, BilinMap_def,
  add_neg_self, map_zero hH h, map_even hH h, zero_sub]
State after:
no goals