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

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k : ℤ
⊢ f (y + f 0 * k) = c * k + f y
Tactic:
have h0 n : f (y + f 0 * (n + 1)) = c + f (y + f 0 * n) := by
  rw [mul_add_one (α := ℤ), ← add_assoc, map_map_zero_add h]
State after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k : ℤ
h0 : ∀ (n : ℤ), f (y + f 0 * (n + 1)) = c + f (y + f 0 * n)
⊢ f (y + f 0 * k) = c * k + f y

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k : ℤ
h0 : ∀ (n : ℤ), f (y + f 0 * (n + 1)) = c + f (y + f 0 * n)
⊢ f (y + f 0 * k) = c * k + f y
Tactic:
replace h0 := Extra.IntIntLinearSolverAlt (f := λ n ↦ f (y + f 0 * n)) h0 k
State after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k : ℤ
h0 : f (y + f 0 * k) = c * k + f (y + f 0 * 0)
⊢ f (y + f 0 * k) = c * k + f y

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k : ℤ
h0 : f (y + f 0 * k) = c * k + f (y + f 0 * 0)
⊢ f (y + f 0 * k) = c * k + f y
Tactic:
rwa [mul_zero, add_zero] at h0
State after:
no goals

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k n : ℤ
⊢ f (y + f 0 * (n + 1)) = c + f (y + f 0 * n)
Tactic:
rw [mul_add_one (α := ℤ), ← add_assoc, map_map_zero_add h]
State after:
no goals