Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective (IMOSLLean4/IMO2020/A6/A6.lean)

State before:
f : ℤ → ℤ
h : good f
h0 : ∃ M, ∀ (n : ℕ), |f^[n] 0| < M
⊢ f = 0
Tactic:
rcases h0 with ⟨M, h0⟩
State after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
⊢ f = 0

State before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
⊢ f = 0
Tactic:
have h1 (a : ℤ) : f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a)) := by
  have h := h a (-a); rwa [a.natAbs_neg, add_neg_self,
    ← two_mul, neg_mul, ← sub_eq_add_neg, ← mul_sub] at h
State after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
⊢ f = 0

State before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
⊢ f = 0
Tactic:
replace h0 (a : ℤ) (h2 : M ≤ a) : f.IsPeriodicPt (2 * a.natAbs ^ 2) 0 :=
  Int.eq_zero_of_abs_lt_dvd ⟨_, h1 a⟩ ((h0 _).trans_le h2)
State after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
⊢ f = 0

State before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
⊢ f = 0
Tactic:
replace h0 : f.IsPeriodicPt 2 0 := by
  have h2 := (h0 _ M.le_refl).gcd (h0 _ M.lt_succ.le)
  have h3 : IsCoprime M (M + 1) :=
    ⟨-1, 1, by rw [one_mul, neg_one_mul, neg_add_cancel_left]⟩
  rwa [Nat.gcd_mul_left, ← Int.natAbs_pow, ← Int.natAbs_pow,
    ← Int.gcd_eq_natAbs, Int.gcd_eq_one_iff_coprime.mpr h3.pow, mul_one] at h2
State after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : IsPeriodicPt f 2 0
⊢ f = 0

State before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : IsPeriodicPt f 2 0
⊢ f = 0
Tactic:
replace h1 (a : ℤ) (h3 : a ≠ 0) : f a = f (-a) := by
  specialize h1 a
  rw [h0.mul_const, zero_eq_mul] at h1
  exact eq_of_sub_eq_zero (h1.resolve_left h3)
State after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
⊢ f = 0

State before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
⊢ f = 0
Tactic:
suffices h2 : ∀ a : ℤ, a ≠ 0 → f a = 0 by
  have h3 : f (f 2) = 1 * f 1 + 1 * f 1 := h 1 1
  rw [h2 1 one_ne_zero, h2 _ two_ne_zero] at h3
  exact funext λ a ↦ (ne_or_eq a 0).elim (h2 a) (λ h4 ↦ h4.symm ▸ h3)
State after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
⊢ ∀ (a : ℤ), a ≠ 0 → f a = 0

State before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
⊢ ∀ (a : ℤ), a ≠ 0 → f a = 0
Tactic:
intro a h2
State after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
⊢ f a = 0

State before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
⊢ f a = 0
Tactic:
obtain ⟨n, h3⟩ : ∃ n : ℕ, a.natAbs ^ 2 = n.succ :=
  Nat.exists_eq_succ_of_ne_zero (pow_ne_zero 2 <| Int.natAbs_ne_zero.mpr h2)
State after:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
⊢ f a = 0

State before:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
⊢ f a = 0
Tactic:
have h4 := map_iterate_sq h (-a)
State after:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
h4 : f^[(-a).natAbs ^ 2] (-a) = -a * f (-a)
⊢ f a = 0

State before:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
h4 : f^[(-a).natAbs ^ 2] (-a) = -a * f (-a)
⊢ f a = 0
Tactic:
rw [Int.natAbs_neg, h3, iterate_succ_apply, ← h1 a h2, ← iterate_succ_apply,
  ← h3, map_iterate_sq h, neg_mul, eq_neg_self_iff, mul_eq_zero] at h4
State after:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
h4 : a = 0 ∨ f a = 0
⊢ f a = 0

State before:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
h4 : a = 0 ∨ f a = 0
⊢ f a = 0
Tactic:
exact h4.resolve_left h2
State after:
no goals

State before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
a : ℤ
⊢ f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
Tactic:
have h := h a (-a)
State after:
f : ℤ → ℤ
h✝ : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
a : ℤ
h : f^[a.natAbs ^ 2 + (-a).natAbs ^ 2] (a + -a) = a * f a + -a * f (-a)
⊢ f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))

State before:
f : ℤ → ℤ
h✝ : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
a : ℤ
h : f^[a.natAbs ^ 2 + (-a).natAbs ^ 2] (a + -a) = a * f a + -a * f (-a)
⊢ f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
Tactic:
rwa [a.natAbs_neg, add_neg_self,
← two_mul, neg_mul, ← sub_eq_add_neg, ← mul_sub] at h
State after:
no goals

State before:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
⊢ IsPeriodicPt f 2 0
Tactic:
have h2 := (h0 _ M.le_refl).gcd (h0 _ M.lt_succ.le)
State after:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
h2 : IsPeriodicPt f ((2 * M.natAbs ^ 2).gcd (2 * (M + 1).natAbs ^ 2)) 0
⊢ IsPeriodicPt f 2 0

State before:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
h2 : IsPeriodicPt f ((2 * M.natAbs ^ 2).gcd (2 * (M + 1).natAbs ^ 2)) 0
⊢ IsPeriodicPt f 2 0
Tactic:
have h3 : IsCoprime M (M + 1) :=
  ⟨-1, 1, by rw [one_mul, neg_one_mul, neg_add_cancel_left]⟩
State after:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
h2 : IsPeriodicPt f ((2 * M.natAbs ^ 2).gcd (2 * (M + 1).natAbs ^ 2)) 0
h3 : IsCoprime M (M + 1)
⊢ IsPeriodicPt f 2 0

State before:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
h2 : IsPeriodicPt f ((2 * M.natAbs ^ 2).gcd (2 * (M + 1).natAbs ^ 2)) 0
h3 : IsCoprime M (M + 1)
⊢ IsPeriodicPt f 2 0
Tactic:
rwa [Nat.gcd_mul_left, ← Int.natAbs_pow, ← Int.natAbs_pow,
  ← Int.gcd_eq_natAbs, Int.gcd_eq_one_iff_coprime.mpr h3.pow, mul_one] at h2
State after:
no goals

State before:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
h2 : IsPeriodicPt f ((2 * M.natAbs ^ 2).gcd (2 * (M + 1).natAbs ^ 2)) 0
⊢ -1 * M + 1 * (M + 1) = 1
Tactic:
rw [one_mul, neg_one_mul, neg_add_cancel_left]
State after:
no goals

State before:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : IsPeriodicPt f 2 0
a : ℤ
h3 : a ≠ 0
⊢ f a = f (-a)
Tactic:
specialize h1 a
State after:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
a : ℤ
h3 : a ≠ 0
h1 : f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
⊢ f a = f (-a)

State before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
a : ℤ
h3 : a ≠ 0
h1 : f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
⊢ f a = f (-a)
Tactic:
rw [h0.mul_const, zero_eq_mul] at h1
State after:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
a : ℤ
h3 : a ≠ 0
h1 : a = 0 ∨ f a - f (-a) = 0
⊢ f a = f (-a)

State before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
a : ℤ
h3 : a ≠ 0
h1 : a = 0 ∨ f a - f (-a) = 0
⊢ f a = f (-a)
Tactic:
exact eq_of_sub_eq_zero (h1.resolve_left h3)
State after:
no goals

State before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
h2 : ∀ (a : ℤ), a ≠ 0 → f a = 0
⊢ f = 0
Tactic:
have h3 : f (f 2) = 1 * f 1 + 1 * f 1 := h 1 1
State after:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
h2 : ∀ (a : ℤ), a ≠ 0 → f a = 0
h3 : f (f 2) = 1 * f 1 + 1 * f 1
⊢ f = 0

State before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
h2 : ∀ (a : ℤ), a ≠ 0 → f a = 0
h3 : f (f 2) = 1 * f 1 + 1 * f 1
⊢ f = 0
Tactic:
rw [h2 1 one_ne_zero, h2 _ two_ne_zero] at h3
State after:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
h2 : ∀ (a : ℤ), a ≠ 0 → f a = 0
h3 : f 0 = 1 * 0 + 1 * 0
⊢ f = 0

State before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
h2 : ∀ (a : ℤ), a ≠ 0 → f a = 0
h3 : f 0 = 1 * 0 + 1 * 0
⊢ f = 0
Tactic:
exact funext λ a ↦ (ne_or_eq a 0).elim (h2 a) (λ h4 ↦ h4.symm ▸ h3)
State after:
no goals