rw [← zero_sub, h2, h1, one_add_one_eq_two]
case refine_1
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
y : D
⊢ f (2 * f y) = f (f (-1) * f y)
no goals