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

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -1
⊢ ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])
Tactic:
rw [EventuallyEqual.const_right_iff] at h
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ∃ N, ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
⊢ ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ∃ N, ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
⊢ ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])
Tactic:
rcases h with ⟨N, h⟩
State after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
⊢ ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])

State before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
⊢ ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])
Tactic:
refine ⟨-f^[N] r, ?_, ?_⟩
State after:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
⊢ 0 < -f^[N] r ∧ -f^[N] r < 1

case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
⊢ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [- -f^[N] r, -f^[N] r - 1])

State before:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
⊢ 0 < -f^[N] r ∧ -f^[N] r < 1
Tactic:
have h0 := h 0
State after:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
h0 : ⌊f^[0 + N] r⌋ = -1
⊢ 0 < -f^[N] r ∧ -f^[N] r < 1

State before:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
h0 : ⌊f^[0 + N] r⌋ = -1
⊢ 0 < -f^[N] r ∧ -f^[N] r < 1
Tactic:
rw [Nat.zero_add, Int.floor_eq_iff, Int.cast_neg, Int.cast_one, and_comm] at h0
State after:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
h0 : f^[N] r < -1 + 1 ∧ -1 ≤ f^[N] r
⊢ 0 < -f^[N] r ∧ -f^[N] r < 1

State before:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
h0 : f^[N] r < -1 + 1 ∧ -1 ≤ f^[N] r
⊢ 0 < -f^[N] r ∧ -f^[N] r < 1
Tactic:
revert h0
State after:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
⊢ f^[N] r < -1 + 1 ∧ -1 ≤ f^[N] r → 0 < -f^[N] r ∧ -f^[N] r < 1

State before:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
⊢ f^[N] r < -1 + 1 ∧ -1 ≤ f^[N] r → 0 < -f^[N] r ∧ -f^[N] r < 1
Tactic:
refine And.imp (λ h0 ↦ neg_pos_of_neg (h0.trans_eq <| neg_add_self 1))
(λ h0 ↦ neg_lt_of_neg_lt (h0.lt_or_eq.resolve_right λ h1 ↦ ?_))
State after:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
h0 : -1 ≤ f^[N] r
h1 : -1 = f^[N] r
⊢ False

State before:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
h0 : -1 ≤ f^[N] r
h1 : -1 = f^[N] r
⊢ False
Tactic:
replace h0 : Int.fract (-1 : R) = 0 := Int.fract_neg_eq_zero.mpr Int.fract_one
State after:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
h1 : -1 = f^[N] r
h0 : Int.fract (-1) = 0
⊢ False

State before:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
h1 : -1 = f^[N] r
h0 : Int.fract (-1) = 0
⊢ False
Tactic:
specialize h 1
State after:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h1 : -1 = f^[N] r
h0 : Int.fract (-1) = 0
h : ⌊f^[1 + N] r⌋ = -1
⊢ False

State before:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h1 : -1 = f^[N] r
h0 : Int.fract (-1) = 0
h : ⌊f^[1 + N] r⌋ = -1
⊢ False
Tactic:
rw [f.iterate_add_apply, f.iterate_one,
← h1, f, h0, mul_zero, Int.floor_zero, zero_eq_neg] at h
State after:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h1 : -1 = f^[N] r
h0 : Int.fract (-1) = 0
h : 1 = 0
⊢ False

State before:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h1 : -1 = f^[N] r
h0 : Int.fract (-1) = 0
h : 1 = 0
⊢ False
Tactic:
exact one_ne_zero h
State after:
no goals

State before:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
⊢ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [- -f^[N] r, -f^[N] r - 1])
Tactic:
have h0 (k : ℕ) : f^[(k + 1) + N] r = -f^[k + N] r - 1 := by
  rw [Nat.add_right_comm, f.iterate_succ_apply', f, Int.fract, h,
    Int.cast_neg, Int.cast_one, neg_one_mul, neg_sub', neg_neg]
State after:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
⊢ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [- -f^[N] r, -f^[N] r - 1])

State before:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
⊢ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [- -f^[N] r, -f^[N] r - 1])
Tactic:
refine ⟨N, 0, λ k ↦ ?_⟩
State after:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
⊢ (fun x => f^[x] r) (k + N) = NatSeq_ofList [- -f^[N] r, -f^[N] r - 1] (k + 0)

State before:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
⊢ (fun x => f^[x] r) (k + N) = NatSeq_ofList [- -f^[N] r, -f^[N] r - 1] (k + 0)
Tactic:
change f^[k + N] r = [_, _].getI (k % 2)
State after:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
⊢ f^[k + N] r = [- -f^[N] r, -f^[N] r - 1].getI (k % 2)

State before:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
⊢ f^[k + N] r = [- -f^[N] r, -f^[N] r - 1].getI (k % 2)
Tactic:
rw [neg_neg, ← N.zero_add, ← h0, zero_add 1, ← add_assoc, k.add_zero, ← h.map_mod_nat]
State after:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
⊢ f^[k % 2 + N] r = [f^[0 + N] r, f^[1 + N] r].getI (k % 2)

State before:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
⊢ f^[k % 2 + N] r = [f^[0 + N] r, f^[1 + N] r].getI (k % 2)
Tactic:
obtain h1 | h1 : k % 2 = 0 ∨ k % 2 = 1 := Nat.mod_two_eq_zero_or_one k
State after:
case intro.refine_2.inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
h1 : k % 2 = 0
⊢ f^[k % 2 + N] r = [f^[0 + N] r, f^[1 + N] r].getI (k % 2)

case intro.refine_2.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
h1 : k % 2 = 1
⊢ f^[k % 2 + N] r = [f^[0 + N] r, f^[1 + N] r].getI (k % 2)

State before:
case intro.refine_2.inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
h1 : k % 2 = 0
⊢ f^[k % 2 + N] r = [f^[0 + N] r, f^[1 + N] r].getI (k % 2)

case intro.refine_2.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
h1 : k % 2 = 1
⊢ f^[k % 2 + N] r = [f^[0 + N] r, f^[1 + N] r].getI (k % 2)
Tactic:
all_goals rw [h1]; rfl
State after:
no goals

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
k : ℕ
⊢ f^[k + 1 + N] r = -f^[k + N] r - 1
Tactic:
rw [Nat.add_right_comm, f.iterate_succ_apply', f, Int.fract, h,
  Int.cast_neg, Int.cast_one, neg_one_mul, neg_sub', neg_neg]
State after:
no goals

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -1
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
k : ℕ
⊢ -f^[k + 1 + N] r - 1 = (fun x => f^[x + N] r) k
Tactic:
rw [h0, neg_sub, sub_neg_eq_add, add_sub_cancel_left]
State after:
no goals

State before:
case intro.refine_2.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
h1 : k % 2 = 1
⊢ f^[k % 2 + N] r = [f^[0 + N] r, f^[1 + N] r].getI (k % 2)
Tactic:
rw [h1]
State after:
case intro.refine_2.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
h1 : k % 2 = 1
⊢ f^[1 + N] r = [f^[0 + N] r, f^[1 + N] r].getI 1

State before:
case intro.refine_2.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h0 : ∀ (k : ℕ), f^[k + 1 + N] r = -f^[k + N] r - 1
h : Function.Periodic (fun x => f^[x + N] r) 2
k : ℕ
h1 : k % 2 = 1
⊢ f^[1 + N] r = [f^[0 + N] r, f^[1 + N] r].getI 1
Tactic:
rfl
State after:
no goals