Theorem: IMOSL.IMO2014A4.c_eq_b_sub_one_mul_map_zero (IMOSLLean4/IMO2014/A4/A4.lean)

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
⊢ c = (b - 1) * f 0
Tactic:
have h3 := h 0 0
State after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h3 : f (0 + f 0) - f 0 = f (b * 0) - f 0 + c
⊢ c = (b - 1) * f 0

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h3 : f (0 + f 0) - f 0 = f (b * 0) - f 0 + c
⊢ c = (b - 1) * f 0
Tactic:
rwa [zero_add, mul_zero, sub_self, zero_add,
  map_is_linear h h0 h1, add_sub_cancel_right, eq_comm] at h3
State after:
no goals