Theorem: IMOSL.IMO2015N1.final_solution (IMOSLLean4/IMO2015/N1/N1.lean)

State before:
M : ℤ
⊢ (∃ k, 2 ∣ f^[k] M) ↔ M ≠ 3
Tactic:
rw [iff_not_comm, not_exists]
State after:
M : ℤ
⊢ M = 3 ↔ ∀ (x : ℕ), ¬2 ∣ f^[x] M

State before:
M : ℤ
⊢ M = 3 ↔ ∀ (x : ℕ), ¬2 ∣ f^[x] M
Tactic:
refine ⟨λ h n ↦ ?_, λ h ↦ ?_⟩
State after:
case refine_1
M : ℤ
h : M = 3
n : ℕ
⊢ ¬2 ∣ f^[n] M

case refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
⊢ M = 3

State before:
case refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
⊢ M = 3
Tactic:
suffices h0 : ∀ n k, 2 ^ (n + 1) ∣ f^[k] M - 3 by
  let K := (M - 3).natAbs
  refine eq_of_sub_eq_zero <| Int.eq_zero_of_abs_lt_dvd (h0 K 0) <| ?_
  rw [← Int.natCast_natAbs, ← Nat.cast_ofNat (n := 2), ← Int.natCast_pow]
  exact Int.ofNat_lt.mpr (K.lt_succ_self.trans K.succ.lt_two_pow)
State after:
case refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
⊢ ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3

State before:
case refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
⊢ ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
Tactic:
refine Nat.rec (λ k ↦ ?_) (λ n h0 k ↦ ?_)
State after:
case refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
k : ℕ
⊢ 2 ^ (Nat.zero + 1) ∣ f^[k] M - 3

case refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n.succ + 1) ∣ f^[k] M - 3

State before:
case refine_1
M : ℤ
h : M = 3
n : ℕ
⊢ ¬2 ∣ f^[n] M
Tactic:
have h0 : f 3 = 3 := rfl
State after:
case refine_1
M : ℤ
h : M = 3
n : ℕ
h0 : f 3 = 3
⊢ ¬2 ∣ f^[n] M

State before:
case refine_1
M : ℤ
h : M = 3
n : ℕ
h0 : f 3 = 3
⊢ ¬2 ∣ f^[n] M
Tactic:
rw [h, Function.iterate_fixed h0, ← two_add_one_eq_three]
State after:
case refine_1
M : ℤ
h : M = 3
n : ℕ
h0 : f 3 = 3
⊢ ¬2 ∣ 2 + 1

State before:
case refine_1
M : ℤ
h : M = 3
n : ℕ
h0 : f 3 = 3
⊢ ¬2 ∣ 2 + 1
Tactic:
exact Int.two_not_dvd_two_mul_add_one 1
State after:
no goals

State before:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
⊢ M = 3
Tactic:
let K := (M - 3).natAbs
State after:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ M = 3

State before:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ M = 3
Tactic:
refine eq_of_sub_eq_zero <| Int.eq_zero_of_abs_lt_dvd (h0 K 0) <| ?_
State after:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ |M - 3| < 2 ^ (K + 1)

State before:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ |M - 3| < 2 ^ (K + 1)
Tactic:
rw [← Int.natCast_natAbs, ← Nat.cast_ofNat (n := 2), ← Int.natCast_pow]
State after:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ ↑(M - 3).natAbs < ↑(OfNat.ofNat 2 ^ (K + 1))

State before:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ ↑(M - 3).natAbs < ↑(OfNat.ofNat 2 ^ (K + 1))
Tactic:
exact Int.ofNat_lt.mpr (K.lt_succ_self.trans K.succ.lt_two_pow)
State after:
no goals

State before:
case refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
k : ℕ
⊢ 2 ^ (Nat.zero + 1) ∣ f^[k] M - 3
Tactic:
rw [Int.dvd_iff_emod_eq_zero, Nat.zero_add, pow_one,
  ← Int.even_iff, Int.even_sub', Int.odd_iff_not_even,
  Int.even_iff, ← Int.dvd_iff_emod_eq_zero]
State after:
case refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
k : ℕ
⊢ ¬2 ∣ f^[k] M ↔ Odd 3

State before:
case refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
k : ℕ
⊢ ¬2 ∣ f^[k] M ↔ Odd 3
Tactic:
exact iff_of_true (h k) (Int.odd_iff.mpr rfl)
State after:
no goals

State before:
case refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n.succ + 1) ∣ f^[k] M - 3
Tactic:
rw [pow_succ', pow_succ']
State after:
case refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * (2 * 2 ^ n) ∣ f^[k] M - 3

State before:
case refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * (2 * 2 ^ n) ∣ f^[k] M - 3
Tactic:
refine main_claim ?_ ?_
State after:
case refine_2.refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * 2 ^ n ∣ f^[k] M - 3

case refine_2.refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * 2 ^ n ∣ f (f^[k] M) - 3

State before:
case refine_2.refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * 2 ^ n ∣ f^[k] M - 3
Tactic:
rw [← pow_succ']
State after:
case refine_2.refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n + 1) ∣ f^[k] M - 3

State before:
case refine_2.refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n + 1) ∣ f^[k] M - 3
Tactic:
exact h0 k
State after:
no goals

State before:
case refine_2.refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * 2 ^ n ∣ f (f^[k] M) - 3
Tactic:
rw [← pow_succ', ← f.iterate_succ_apply']
State after:
case refine_2.refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n + 1) ∣ f^[k.succ] M - 3

State before:
case refine_2.refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n + 1) ∣ f^[k.succ] M - 3
Tactic:
exact h0 (k + 1)
State after:
no goals