have h1 : (-1 : R) * (-1) = 1 := by rw [neg_mul_neg, mul_one]
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
⊢ f (f 0 ^ 2) = 0
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h1 : -1 * -1 = 1
⊢ f (f 0 ^ 2) = 0