Theorem: IMOSL.Extra.SquareLike.map_zero (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)
⊢ f 0 = 0
Tactic:
specialize h 0 0
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 : f (0 + 0) + f (0 - 0) = 2 • (f 0 + f 0)
⊢ f 0 = 0

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 : f (0 + 0) + f (0 - 0) = 2 • (f 0 + f 0)
⊢ f 0 = 0
Tactic:
rw [add_zero, sub_zero, two_nsmul, self_eq_add_right, ← two_nsmul] at h
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 : 2 • f 0 = 0
⊢ f 0 = 0

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 : 2 • f 0 = 0
⊢ f 0 = 0
Tactic:
exact hH _ _ (h.trans (nsmul_zero 2).symm)
State after:
no goals