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

State before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
⊢ f (x + 1) + 1 = f x
Tactic:
have h1 := h x 1
State after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
h1 : f (f x * f 1) + f (x + 1) = f (x * 1)
⊢ f (x + 1) + 1 = f x

State before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
h1 : f (f x * f 1) + f (x + 1) = f (x * 1)
⊢ f (x + 1) + 1 = f x
Tactic:
rwa [good_map_one h, mul_zero, h0, add_comm, mul_one] at h1
State after:
no goals