Theorem: IMOSL.IMO2006A1.final_solution (IMOSLLean4/IMO2006/A1/A1.lean)

State before:
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
⊢ ∃ N, ∀ (k : ℕ), N ≤ k → f^[k + 2] r = f^[k] r
Tactic:
rcases Archimedean_f_iter_classification r with
  ⟨N, _, h⟩ | ⟨s, -, N, M, h⟩ | ⟨C, hC, N, _, h⟩
State after:
case inl.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
N w✝ : ℕ
h : ∀ (k : ℕ), (fun x => f^[x] r) (k + N) = (fun x => 0) (k + w✝)
⊢ ∃ N, ∀ (k : ℕ), N ≤ k → f^[k + 2] r = f^[k] r

case inr.inl.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r s : R
N M : ℕ
h : ∀ (k : ℕ), (fun x => f^[x] r) (k + N) = NatSeq_ofList [-s, s - 1] (k + M)
⊢ ∃ N, ∀ (k : ℕ), N ≤ k → f^[k + 2] r = f^[k] r

case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (fun x => (↑C + 1) * f^[x] r) (k + N) = (fun x => -↑C ^ 2) (k + w✝)
⊢ ∃ N, ∀ (k : ℕ), N ≤ k → f^[k + 2] r = f^[k] r

State before:
case inl.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
N w✝ : ℕ
h : ∀ (k : ℕ), (fun x => f^[x] r) (k + N) = (fun x => 0) (k + w✝)
⊢ ∃ N, ∀ (k : ℕ), N ≤ k → f^[k + 2] r = f^[k] r

case inr.inl.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r s : R
N M : ℕ
h : ∀ (k : ℕ), (fun x => f^[x] r) (k + N) = NatSeq_ofList [-s, s - 1] (k + M)
⊢ ∃ N, ∀ (k : ℕ), N ≤ k → f^[k + 2] r = f^[k] r

case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (fun x => (↑C + 1) * f^[x] r) (k + N) = (fun x => -↑C ^ 2) (k + w✝)
⊢ ∃ N, ∀ (k : ℕ), N ≤ k → f^[k + 2] r = f^[k] r
Tactic:
all_goals
  simp only at h; refine ⟨N, λ k h0 ↦ ?_⟩
  rcases Nat.exists_eq_add_of_le' h0 with ⟨k, rfl⟩
State after:
case inl.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
N w✝ : ℕ
h : ∀ (k : ℕ), f^[k + N] r = 0
k : ℕ
h0 : N ≤ k + N
⊢ f^[k + N + 2] r = f^[k + N] r

case inr.inl.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r s : R
N M : ℕ
h : ∀ (k : ℕ), f^[k + N] r = NatSeq_ofList [-s, s - 1] (k + M)
k : ℕ
h0 : N ≤ k + N
⊢ f^[k + N + 2] r = f^[k + N] r

case inr.inr.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r = -↑C ^ 2
k : ℕ
h0 : N ≤ k + N
⊢ f^[k + N + 2] r = f^[k + N] r

State before:
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (fun x => (↑C + 1) * f^[x] r) (k + N) = (fun x => -↑C ^ 2) (k + w✝)
⊢ ∃ N, ∀ (k : ℕ), N ≤ k → f^[k + 2] r = f^[k] r
Tactic:
simp only at h
State after:
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r = -↑C ^ 2
⊢ ∃ N, ∀ (k : ℕ), N ≤ k → f^[k + 2] r = f^[k] r

State before:
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r = -↑C ^ 2
⊢ ∃ N, ∀ (k : ℕ), N ≤ k → f^[k + 2] r = f^[k] r
Tactic:
refine ⟨N, λ k h0 ↦ ?_⟩
State after:
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r = -↑C ^ 2
k : ℕ
h0 : N ≤ k
⊢ f^[k + 2] r = f^[k] r

State before:
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r = -↑C ^ 2
k : ℕ
h0 : N ≤ k
⊢ f^[k + 2] r = f^[k] r
Tactic:
rcases Nat.exists_eq_add_of_le' h0 with ⟨k, rfl⟩
State after:
case inr.inr.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r = -↑C ^ 2
k : ℕ
h0 : N ≤ k + N
⊢ f^[k + N + 2] r = f^[k + N] r

State before:
case inl.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
N w✝ : ℕ
h : ∀ (k : ℕ), f^[k + N] r = 0
k : ℕ
h0 : N ≤ k + N
⊢ f^[k + N + 2] r = f^[k + N] r
Tactic:
rw [h, Nat.add_right_comm, h]
State after:
no goals

State before:
case inr.inl.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r s : R
N M : ℕ
h : ∀ (k : ℕ), f^[k + N] r = NatSeq_ofList [-s, s - 1] (k + M)
k : ℕ
h0 : N ≤ k + N
⊢ f^[k + N + 2] r = f^[k + N] r
Tactic:
rw [h, Nat.add_right_comm, h, Nat.add_right_comm]
State after:
case inr.inl.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r s : R
N M : ℕ
h : ∀ (k : ℕ), f^[k + N] r = NatSeq_ofList [-s, s - 1] (k + M)
k : ℕ
h0 : N ≤ k + N
⊢ NatSeq_ofList [-s, s - 1] (k + M + 2) = NatSeq_ofList [-s, s - 1] (k + M)

State before:
case inr.inl.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r s : R
N M : ℕ
h : ∀ (k : ℕ), f^[k + N] r = NatSeq_ofList [-s, s - 1] (k + M)
k : ℕ
h0 : N ≤ k + N
⊢ NatSeq_ofList [-s, s - 1] (k + M + 2) = NatSeq_ofList [-s, s - 1] (k + M)
Tactic:
exact NatSeq_ofList_periodic [-s, s - 1] _
State after:
no goals

State before:
case inr.inr.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r = -↑C ^ 2
k : ℕ
h0 : N ≤ k + N
⊢ f^[k + N + 2] r = f^[k + N] r
Tactic:
replace h0 := (h (k + 2)).trans (h k).symm
State after:
case inr.inr.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r = -↑C ^ 2
k : ℕ
h0 : (↑C + 1) * f^[k + 2 + N] r = (↑C + 1) * f^[k + N] r
⊢ f^[k + N + 2] r = f^[k + N] r

State before:
case inr.inr.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r = -↑C ^ 2
k : ℕ
h0 : (↑C + 1) * f^[k + 2 + N] r = (↑C + 1) * f^[k + N] r
⊢ f^[k + N + 2] r = f^[k + N] r
Tactic:
rw [Nat.add_right_comm, mul_eq_mul_left_iff] at h0
State after:
case inr.inr.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r = -↑C ^ 2
k : ℕ
h0 : f^[k + N + 2] r = f^[k + N] r ∨ ↑C + 1 = 0
⊢ f^[k + N + 2] r = f^[k + N] r

State before:
case inr.inr.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r = -↑C ^ 2
k : ℕ
h0 : f^[k + N + 2] r = f^[k + N] r ∨ ↑C + 1 = 0
⊢ f^[k + N + 2] r = f^[k + N] r
Tactic:
exact h0.resolve_right (add_pos (Nat.cast_pos.mpr (pos_of_gt hC)) one_pos).ne.symm
State after:
no goals