Theorem: IMOSL.IMO2019A1.final_solution (IMOSLLean4/IMO2019/A1/A1.lean)

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Tactic:
have h1 n : N * (f (n + 1) - f n) = f N - f 0 := by
  rw [mul_sub, sub_eq_iff_eq_add, ← add_sub_right_comm, eq_sub_iff_add_eq',
    ← N.mul_zero, h0, zero_add, n.add_comm, ← h0, mul_one]
State after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
h1 : ∀ (n : ℤ), N * (f (n + 1) - f n) = f N - f 0
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
h1 : ∀ (n : ℤ), N * (f (n + 1) - f n) = f N - f 0
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Tactic:
replace h1 n : f (n + 1) = (f 1 - f 0) + f n :=
  eq_add_of_sub_eq <| mul_left_cancel₀ h <| by rw [h1, ← h1 0, zero_add]
State after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
h1 : ∀ (n : ℤ), f (n + 1) = f 1 - f 0 + f n
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
h1 : ∀ (n : ℤ), f (n + 1) = f 1 - f 0 + f n
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Tactic:
generalize f 1 - f 0 = q at h1
State after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f (n + 1) = q + f n
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f (n + 1) = q + f n
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Tactic:
apply Extra.IntIntLinearSolverAlt at h1
State after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Tactic:
refine (em' (N = q)).imp (λ h2 ↦ ?_) (λ h2 ↦ ⟨f 0, funext <| by rwa [h2]⟩)
State after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
⊢ f = 0

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
⊢ f = 0
Tactic:
have h3 := h0 0 0
State after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f (N * 0) + N * f 0 = f (f (0 + 0))
⊢ f = 0

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f (N * 0) + N * f 0 = f (f (0 + 0))
⊢ f = 0
Tactic:
rw [add_zero, N.mul_zero, h1 (f 0), add_comm, add_left_inj,
  mul_eq_mul_right_iff, or_iff_right h2] at h3
State after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
⊢ f = 0

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
⊢ f = 0
Tactic:
specialize h0 0 1
State after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : f (N * 0) + N * f 1 = f (f (0 + 1))
⊢ f = 0

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : f (N * 0) + N * f 1 = f (f (0 + 1))
⊢ f = 0
Tactic:
rw [N.mul_zero, zero_add, h1 (f 1), add_comm, add_left_inj,
  mul_eq_mul_right_iff, or_iff_right h2, h1, mul_one, h3, add_zero] at h0
State after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : q = 0
⊢ f = 0

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : q = 0
⊢ f = 0
Tactic:
funext n
State after:
case h
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : q = 0
n : ℤ
⊢ f n = 0 n

State before:
case h
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : q = 0
n : ℤ
⊢ f n = 0 n
Tactic:
rw [h1, h0, h3, n.zero_mul, add_zero, Pi.zero_apply]
State after:
no goals

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
n : ℤ
⊢ N * (f (n + 1) - f n) = f N - f 0
Tactic:
rw [mul_sub, sub_eq_iff_eq_add, ← add_sub_right_comm, eq_sub_iff_add_eq',
  ← N.mul_zero, h0, zero_add, n.add_comm, ← h0, mul_one]
State after:
no goals

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
h1 : ∀ (n : ℤ), N * (f (n + 1) - f n) = f N - f 0
n : ℤ
⊢ N * (f (n + 1) - f n) = N * (f 1 - f 0)
Tactic:
rw [h1, ← h1 0, zero_add]
State after:
no goals

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : N = q
⊢ ∀ (x : ℤ), f x = N * x + f 0
Tactic:
rwa [h2]
State after:
no goals

State before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : f = 0 ∨ ∃ c, f = fun x => N * x + c
a b : ℤ
⊢ f (N * a) + N * f b = f (f (a + b))
Tactic:
rcases h0 with rfl | ⟨c, rfl⟩
State after:
case inl
N : ℤ
h : N ≠ 0
a b : ℤ
⊢ 0 (N * a) + N * 0 b = 0 (0 (a + b))

case inr.intro
N : ℤ
h : N ≠ 0
a b c : ℤ
⊢ (fun x => N * x + c) (N * a) + N * (fun x => N * x + c) b = (fun x => N * x + c) ((fun x => N * x + c) (a + b))

State before:
case inl
N : ℤ
h : N ≠ 0
a b : ℤ
⊢ 0 (N * a) + N * 0 b = 0 (0 (a + b))
Tactic:
exact (N * 0).zero_add.trans N.mul_zero
State after:
no goals

State before:
case inr.intro
N : ℤ
h : N ≠ 0
a b c : ℤ
⊢ (fun x => N * x + c) (N * a) + N * (fun x => N * x + c) b = (fun x => N * x + c) ((fun x => N * x + c) (a + b))
Tactic:
rw [add_right_comm, ← mul_add, ← add_assoc, ← mul_add]
State after:
no goals