Theorem: Imo2017P2.good_eq_of_inj (Compfiles/Imo2017P2.lean)

State before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Injective f
x : R
⊢ f (f x) + f x = 1
Tactic:
rw [← h0, ← mul_zero x, ← h, add_zero, h0, mul_one]
State after:
no goals

State before:
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 = 1 - x
Tactic:
rw [eq_sub_iff_add_eq', ← h2 x, add_left_inj]
State after:
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
⊢ x = f (f x)

State before:
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
⊢ x = f (f x)
Tactic:
apply h1
State after:
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))

State before:
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))
Tactic:
rw [← add_left_inj (f (f x)), h2, add_comm, h2]
State after:
no goals