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

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
⊢ ∀ (n : ℤ), f n = (b - 1) * n + f 0
Tactic:
suffices f.Injective by
intro n
  have h2 := eq_add_of_sub_eq' (h 0 (b * n))
  rw [mul_zero, sub_self, zero_add, ← sub_left_inj (a := f n),
    add_sub_right_comm, ← h n n, sub_left_inj] at h2
  rw [sub_one_mul, ← add_sub_right_comm, this h2, add_sub_cancel_left]
State after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
⊢ Function.Injective f

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
⊢ Function.Injective f
Tactic:
have h2 : f 0 ≠ 0 := λ h2 ↦ by
  have h3 := map_map_zero_add h 0
  rw [zero_add, h2, h2, add_zero] at h3
  exact h1 h3.symm
State after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
⊢ Function.Injective f

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
⊢ Function.Injective f
Tactic:
obtain ⟨m, n, h3, h4⟩ := exists_ne_pow_eq h2 b
State after:
case intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
h4 : b ^ m % f 0 = b ^ n % f 0
⊢ Function.Injective f

State before:
case intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
h4 : b ^ m % f 0 = b ^ n % f 0
⊢ Function.Injective f
Tactic:
rw [Int.emod_eq_emod_iff_emod_sub_eq_zero, ← Int.dvd_iff_emod_eq_zero] at h4
State after:
case intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
h4 : f 0 ∣ b ^ m - b ^ n
⊢ Function.Injective f

State before:
case intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
h4 : f 0 ∣ b ^ m - b ^ n
⊢ Function.Injective f
Tactic:
rcases h4 with ⟨N, h4⟩
State after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
⊢ Function.Injective f

State before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
⊢ Function.Injective f
Tactic:
intro x y h5
State after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : f x = f y
⊢ x = y

State before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : f x = f y
⊢ x = y
Tactic:
apply map_b_pow_mul_eq_of_map_eq h at h5
State after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
⊢ x = y

State before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
⊢ x = y
Tactic:
have h6 := h5 m
State after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : f (b ^ m * x) = f (b ^ m * y)
⊢ x = y

State before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : f (b ^ m * x) = f (b ^ m * y)
⊢ x = y
Tactic:
have h7 := map_mul_map_zero_add h
State after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : f (b ^ m * x) = f (b ^ m * y)
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
⊢ x = y

State before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : f (b ^ m * x) = f (b ^ m * y)
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
⊢ x = y
Tactic:
rw [eq_add_of_sub_eq' h4, add_mul, mul_assoc, h7, add_mul,
  mul_assoc, h7, h5, add_left_inj, Int.mul_eq_mul_left_iff h1] at h6
State after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
⊢ x = y

State before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
⊢ x = y
Tactic:
refine (Int.mul_eq_mul_left_iff λ h8 ↦ ?_).mp h6
State after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
h8 : N = 0
⊢ False

State before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
h8 : N = 0
⊢ False
Tactic:
rw [h8, mul_zero, sub_eq_zero] at h4
State after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m = b ^ n
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
h8 : N = 0
⊢ False

State before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m = b ^ n
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
h8 : N = 0
⊢ False
Tactic:
exact h3 (Int.pow_right_injective h0 h4)
State after:
no goals

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
⊢ ∀ (n : ℤ), f n = (b - 1) * n + f 0
Tactic:
intro n
State after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
⊢ f n = (b - 1) * n + f 0

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
⊢ f n = (b - 1) * n + f 0
Tactic:
have h2 := eq_add_of_sub_eq' (h 0 (b * n))
State after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
h2 : f (b * n + f 0) = f (b * n) + (f (b * 0) - f 0 + c)
⊢ f n = (b - 1) * n + f 0

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
h2 : f (b * n + f 0) = f (b * n) + (f (b * 0) - f 0 + c)
⊢ f n = (b - 1) * n + f 0
Tactic:
rw [mul_zero, sub_self, zero_add, ← sub_left_inj (a := f n),
  add_sub_right_comm, ← h n n, sub_left_inj] at h2
State after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
h2 : f (b * n + f 0) = f (n + f n)
⊢ f n = (b - 1) * n + f 0

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
h2 : f (b * n + f 0) = f (n + f n)
⊢ f n = (b - 1) * n + f 0
Tactic:
rw [sub_one_mul, ← add_sub_right_comm, this h2, add_sub_cancel_left]
State after:
no goals

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

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 = 0
h3 : f (0 + f 0) = c + f 0
⊢ False
Tactic:
rw [zero_add, h2, h2, add_zero] at h3
State after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 = 0
h3 : 0 = c
⊢ False

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 = 0
h3 : 0 = c
⊢ False
Tactic:
exact h1 h3.symm
State after:
no goals