rw [good_shift2 h0 h1, ← h0, h4, add_assoc, ← add_assoc (c + 1), h2,
  good_special_equality h0 (mul_inv_cancel h3), zero_add, add_right_comm]
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
c d : F
h3 : d ≠ 0
h4 : f (c + 1) = f (d + 1)
⊢ f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
no goals