Theorem: IMOSL.IMO2017A6.good_eq_of_inj (IMOSLLean4/IMO2017/A6/A6.lean)

State before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Function.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 : Function.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 : Function.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 : Function.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 : Function.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 : Function.Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ f x = f (f (f x))
Tactic:
rw [eq_sub_of_add_eq (h2 (f x)), ← h2 x, add_sub_cancel_left]
State after:
no goals