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

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
⊢ f (b ^ 0 * x) = f (b ^ 0 * y)
Tactic:
rwa [pow_zero, one_mul, one_mul]
State after:
no goals

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
k : ℕ
⊢ f (b ^ (k + 1) * x) = f (b ^ (k + 1) * y)
Tactic:
rw [pow_succ', mul_assoc, mul_assoc]
State after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
k : ℕ
⊢ f (b * (b ^ k * x)) = f (b * (b ^ k * y))

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
k : ℕ
⊢ f (b * (b ^ k * x)) = f (b * (b ^ k * y))
Tactic:
have h1 := h (b ^ k * y) 0
State after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
k : ℕ
h1 : f (0 + f (b ^ k * y)) - f 0 = f (b * (b ^ k * y)) - f (b ^ k * y) + c
⊢ f (b * (b ^ k * x)) = f (b * (b ^ k * y))

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
k : ℕ
h1 : f (0 + f (b ^ k * y)) - f 0 = f (b * (b ^ k * y)) - f (b ^ k * y) + c
⊢ f (b * (b ^ k * x)) = f (b * (b ^ k * y))
Tactic:
rwa [← map_b_pow_mul_eq_of_map_eq h0 k,
  h, add_left_inj, sub_left_inj] at h1
State after:
no goals