Theorem: IMOSL.Extra.SquareLike.map_even (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 : G
⊢ f (-x) = f x
Tactic:
have h0 := h 0 x
State after:
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 : G
h0 : f (0 + x) + f (0 - x) = 2 • (f 0 + f x)
⊢ f (-x) = f x

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 : G
h0 : f (0 + x) + f (0 - x) = 2 • (f 0 + f x)
⊢ f (-x) = f x
Tactic:
rwa [zero_add, zero_sub, map_zero hH h, zero_add, two_nsmul, add_right_inj] at h0
State after:
no goals