rcases eq_or_ne a 0 with rfl | ha
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 + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
⊢ a = b
case inl
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)
b : F
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
h4 : f (0 + 1) = f (b + 1)
⊢ 0 = b

case inr
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 + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
⊢ a = b