rwa [← h3, self_eq_add_left, ← h2, good_map_eq_zero_iff h0 h1,
  sub_eq_iff_eq_add, one_add_one_eq_two, mul_right_eq_self₀,
  or_iff_left h, ← add_sub_cancel_right y 1, h2, add_left_eq_self,
  good_map_add_one_eq_zero_iff h0 h1] at h4
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : D), f (x - 1) = f x + 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
y : D
h4 : f y = f (-y)
⊢ y = 0
no goals