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

State before:
D : Type u_1
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:
D : Type u_1
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:
D : Type u_1
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