have h3 : ∀ c d : F, d ≠ 0 → f (c + 1) = f (d + 1) →
    f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1) := λ c d h3 h4 ↦ by
  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
⊢ Injective f
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
⊢ Injective f