rw [← add_left_inj (f (f x)), h2, add_comm, h2]
case a
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ f x = f (f (f x))
no goals