replace h6 := congr_arg f h6
case inr.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
hb : b ≠ 0
h6 : ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) = (a + b⁻¹ + 1) * (b + a⁻¹ + 1)
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
⊢ a = b
case inr.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
hb : b ≠ 0
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
h6 : f (((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1)) = f ((a + b⁻¹ + 1) * (b + a⁻¹ + 1))
⊢ a = b