rw [sub_add_cancel, h1, zero_mul] at h3
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f (f (c - 1 + 1) * f ((c - 1)⁻¹ + 1)) = 0
⊢ f = 0
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
⊢ f = 0