intros a b h4
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
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)
a b : F
h4 : f a = f b
⊢ a = b