Theorem: IMOSL.IMO2009N3.const_of_infinite_map_eq_map_zero (IMOSLLean4/IMO2009/N3/N3.lean)

State before:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0 : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b : ℕ
⊢ f b = f 0
Tactic:
obtain ⟨n, h0, h1⟩ := h0 (b + (f 0 - f b).natAbs + 1)
State after:
case intro.intro
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : b + (f 0 - f b).natAbs + 1 ≤ n
h1 : f n = f 0
⊢ f b = f 0

State before:
case intro.intro
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : b + (f 0 - f b).natAbs + 1 ≤ n
h1 : f n = f 0
⊢ f b = f 0
Tactic:
specialize h n b
State after:
case intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : b + (f 0 - f b).natAbs + 1 ≤ n
h1 : f n = f 0
h : ↑n - ↑b ∣ f n - f b
⊢ f b = f 0

State before:
case intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : b + (f 0 - f b).natAbs + 1 ≤ n
h1 : f n = f 0
h : ↑n - ↑b ∣ f n - f b
⊢ f b = f 0
Tactic:
rw [Nat.succ_le_iff, lt_iff_exists_add] at h0
State after:
case intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : ∃ c > 0, n = b + (f 0 - f b).natAbs + c
h1 : f n = f 0
h : ↑n - ↑b ∣ f n - f b
⊢ f b = f 0

State before:
case intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : ∃ c > 0, n = b + (f 0 - f b).natAbs + c
h1 : f n = f 0
h : ↑n - ↑b ∣ f n - f b
⊢ f b = f 0
Tactic:
rcases h0 with ⟨C, h0, rfl⟩
State after:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : ↑(b + (f 0 - f b).natAbs + C) - ↑b ∣ f (b + (f 0 - f b).natAbs + C) - f b
⊢ f b = f 0

State before:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : ↑(b + (f 0 - f b).natAbs + C) - ↑b ∣ f (b + (f 0 - f b).natAbs + C) - f b
⊢ f b = f 0
Tactic:
rw [h1, add_assoc, Nat.cast_add, add_sub_cancel_left, Int.natCast_dvd] at h
State after:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : (f 0 - f b).natAbs + C ∣ (f 0 - f b).natAbs
⊢ f b = f 0

State before:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : (f 0 - f b).natAbs + C ∣ (f 0 - f b).natAbs
⊢ f b = f 0
Tactic:
have h2 := Nat.eq_zero_of_dvd_of_lt h (Nat.lt_add_of_pos_right h0)
State after:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : (f 0 - f b).natAbs + C ∣ (f 0 - f b).natAbs
h2 : (f 0 - f b).natAbs = 0
⊢ f b = f 0

State before:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : (f 0 - f b).natAbs + C ∣ (f 0 - f b).natAbs
h2 : (f 0 - f b).natAbs = 0
⊢ f b = f 0
Tactic:
rwa [Int.natAbs_eq_zero, sub_eq_zero, eq_comm] at h2
State after:
no goals