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

State before:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCancelCommMonoid 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 z : G
⊢ 2 • (f (x + y + z) + f x + (f y + f z)) = 2 • (f (x + y) + f (x + z) + f (y + z))
Tactic:
rw [nsmul_add, ← h, ← h, add_add_add_comm, add_assoc x, add_sub_cancel_left,
add_comm (f (y + z)), add_add_add_comm, ← two_nsmul, nsmul_add, add_left_inj, ← h,
add_sub_add_left_eq_sub, add_left_inj, add_right_comm, add_add_add_comm]
State after:
no goals