rw [Pi.zero_apply, ← h3, ← mul_zero x, ← h,
  h3, mul_zero, h3, zero_add, add_zero]
case h
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
x : D
⊢ f x = 0 x
no goals