internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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)
Proof 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)
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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]
Proof 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)
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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
Proof 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)
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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]
Proof 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
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.f_alt_formula
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ (↑⌊r⌋ - 1) * f r - ↑⌊r⌋ ^ 2 = ↑⌊r⌋ * ((↑⌊r⌋ - 1) * r - ↑⌊r⌋ ^ 2)
Tactic:
rw [sq, f, Int.fract, mul_sub, mul_sub, sub_sub, ← add_one_mul (α := R), sub_add_cancel,
  mul_sub, sub_left_inj, ← mul_assoc, sub_one_mul, ← mul_sub_one, mul_assoc]
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
rcases h with ⟨N, _, h⟩
Proof state after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋) (k + N) = (fun x => -↑C) (k + w✝)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋) (k + N) = (fun x => -↑C) (k + w✝)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
simp only at h
Proof state after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
have h0 (k) : (C + 1) * f^[(k + 1) + N] r + C ^ 2
    = -C * ((C + 1) * f^[k + N] r + C ^ 2) := by
  have h0 := f_alt_formula (f^[k + N] r)
  rw [h, Int.cast_neg, Int.cast_natCast, neg_sq, ← neg_add', neg_mul, ← neg_add',
    neg_mul, neg_inj, neg_mul, ← neg_add', mul_neg, ← neg_mul] at h0
  rwa [Nat.add_right_comm, f.iterate_succ_apply']
Proof state after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
replace h0 : ∀ k, (C + 1) * f^[k + N] r + C ^ 2
    = (-C) ^ k * ((C + 1) * f^[N] r + C ^ 2) :=
  Nat.rec (by rw [Nat.zero_add, pow_zero, one_mul])
    (λ k h1 ↦ by rw [h0, h1, ← mul_assoc, ← pow_succ'])
Proof state after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ((↑C + 1) * f^[N] r + ↑C ^ 2)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ((↑C + 1) * f^[N] r + ↑C ^ 2)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
set ε := (C + 1) * f^[N] r + C ^ 2
Proof state after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
refine ⟨ε, ?_, N, 0, λ k ↦ eq_neg_add_of_add_eq <| (add_comm _ _).trans (h0 k)⟩
Proof state after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ Infinitesimal ε
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ Infinitesimal ε
Tactic:
replace h0 (k) : |(C + 1) * Int.fract (f^[k + N] r) - C| = C ^ k • |ε| := by
  specialize h0 k
  rw [sq, ← Int.fract_add_floor (f^[k + N] r), h, Int.cast_neg, Int.cast_natCast, mul_add,
    mul_neg, add_one_mul (C : R) C, add_assoc, neg_add_rev, neg_add_cancel_right] at h0
  rw [sub_eq_add_neg, h0, abs_mul, abs_pow, abs_neg,
    Nat.abs_cast, nsmul_eq_mul, Nat.cast_pow]
Proof state after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
⊢ Infinitesimal ε
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
⊢ Infinitesimal ε
Tactic:
replace h (s : R) : |(C + 1) * Int.fract s - C| < ((C + 1 + C : ℕ) : R) := by
  apply (abs_sub _ _).trans_lt
  rw [Nat.abs_cast, Nat.cast_add, add_lt_add_iff_right, ← Nat.cast_succ,
    abs_mul, Nat.abs_cast, abs_eq_self.mpr (Int.fract_nonneg s)]
  refine mul_lt_of_lt_one_right (Nat.cast_pos.mpr C.succ_pos) (Int.fract_lt_one _)
Proof state after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
h : ∀ (s : R), |(↑C + 1) * Int.fract s - ↑C| < ↑(C + 1 + C)
⊢ Infinitesimal ε
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
h : ∀ (s : R), |(↑C + 1) * Int.fract s - ↑C| < ↑(C + 1 + C)
⊢ Infinitesimal ε
Tactic:
exact Infinitesimal.iff_nsmul_Nat_bdd.mpr ⟨C + 1 + C, λ k ↦
  (nsmul_le_nsmul_left (abs_nonneg ε) (Nat.lt_pow_self hC k).le).trans_lt <|
    (h0 _).symm.trans_lt (h (f^[k + N] r))⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
k : ℕ
⊢ (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
Tactic:
have h0 := f_alt_formula (f^[k + N] r)
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
k : ℕ
h0 :
  (↑⌊f^[k + N] r⌋ - 1) * f (f^[k + N] r) - ↑⌊f^[k + N] r⌋ ^ 2 =
    ↑⌊f^[k + N] r⌋ * ((↑⌊f^[k + N] r⌋ - 1) * f^[k + N] r - ↑⌊f^[k + N] r⌋ ^ 2)
⊢ (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
k : ℕ
h0 :
  (↑⌊f^[k + N] r⌋ - 1) * f (f^[k + N] r) - ↑⌊f^[k + N] r⌋ ^ 2 =
    ↑⌊f^[k + N] r⌋ * ((↑⌊f^[k + N] r⌋ - 1) * f^[k + N] r - ↑⌊f^[k + N] r⌋ ^ 2)
⊢ (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
Tactic:
rw [h, Int.cast_neg, Int.cast_natCast, neg_sq, ← neg_add', neg_mul, ← neg_add',
  neg_mul, neg_inj, neg_mul, ← neg_add', mul_neg, ← neg_mul] at h0
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
k : ℕ
h0 : (↑C + 1) * f (f^[k + N] r) + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
⊢ (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
k : ℕ
h0 : (↑C + 1) * f (f^[k + N] r) + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
⊢ (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
Tactic:
rwa [Nat.add_right_comm, f.iterate_succ_apply']
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
⊢ (↑C + 1) * f^[Nat.zero + N] r + ↑C ^ 2 = (-↑C) ^ Nat.zero * ((↑C + 1) * f^[N] r + ↑C ^ 2)
Tactic:
rw [Nat.zero_add, pow_zero, one_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
k : ℕ
h1 : (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ((↑C + 1) * f^[N] r + ↑C ^ 2)
⊢ (↑C + 1) * f^[k.succ + N] r + ↑C ^ 2 = (-↑C) ^ k.succ * ((↑C + 1) * f^[N] r + ↑C ^ 2)
Tactic:
rw [h0, h1, ← mul_assoc, ← pow_succ']
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
k : ℕ
⊢ |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
Tactic:
specialize h0 k
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
k : ℕ
h0 : (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
k : ℕ
h0 : (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
Tactic:
rw [sq, ← Int.fract_add_floor (f^[k + N] r), h, Int.cast_neg, Int.cast_natCast, mul_add,
  mul_neg, add_one_mul (C : R) C, add_assoc, neg_add_rev, neg_add_cancel_right] at h0
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
k : ℕ
h0 : (↑C + 1) * Int.fract (f^[k + N] r) + -↑C = (-↑C) ^ k * ε
⊢ |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
k : ℕ
h0 : (↑C + 1) * Int.fract (f^[k + N] r) + -↑C = (-↑C) ^ k * ε
⊢ |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
Tactic:
rw [sub_eq_add_neg, h0, abs_mul, abs_pow, abs_neg,
  Nat.abs_cast, nsmul_eq_mul, Nat.cast_pow]
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
s : R
⊢ |(↑C + 1) * Int.fract s - ↑C| < ↑(C + 1 + C)
Tactic:
apply (abs_sub _ _).trans_lt
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
s : R
⊢ |(↑C + 1) * Int.fract s| + |↑C| < ↑(C + 1 + C)
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
s : R
⊢ |(↑C + 1) * Int.fract s| + |↑C| < ↑(C + 1 + C)
Tactic:
rw [Nat.abs_cast, Nat.cast_add, add_lt_add_iff_right, ← Nat.cast_succ,
  abs_mul, Nat.abs_cast, abs_eq_self.mpr (Int.fract_nonneg s)]
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
s : R
⊢ ↑C.succ * Int.fract s < ↑(C + 1)
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
s : R
⊢ ↑C.succ * Int.fract s < ↑(C + 1)
Tactic:
refine mul_lt_of_lt_one_right (Nat.cast_pos.mpr C.succ_pos) (Int.fract_lt_one _)
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.final_solution_general
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ (EventuallyEqual (fun x => f^[x] r) fun x => 0) ∨
    (∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])) ∨
      ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
rcases floor_f_iter_eventually_const r with ⟨C, h⟩
Proof state after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
⊢ (EventuallyEqual (fun x => f^[x] r) fun x => 0) ∨
    (∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])) ∨
      ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Theorem: IMOSL.IMO2006A1.final_solution_general
Proof state before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
⊢ (EventuallyEqual (fun x => f^[x] r) fun x => 0) ∨
    (∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])) ∨
      ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
refine C.eq_zero_or_pos.imp ?_ (λ h0 ↦ (h0 : 1 ≤ C).eq_or_lt.imp ?_ ?_)
Proof state after:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
⊢ C = 0 → EventuallyEqual (fun x => f^[x] r) fun x => 0

case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
h0 : 1 ≤ C
⊢ 1 = C → ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])

case intro.refine_3
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
h0 : 1 ≤ C
⊢ 1 < C →
    ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Theorem: IMOSL.IMO2006A1.final_solution_general
Proof state before:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
⊢ C = 0 → EventuallyEqual (fun x => f^[x] r) fun x => 0
Tactic:
rintro rfl
Proof state after:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑0
⊢ EventuallyEqual (fun x => f^[x] r) fun x => 0
Theorem: IMOSL.IMO2006A1.final_solution_general
Proof state before:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑0
⊢ EventuallyEqual (fun x => f^[x] r) fun x => 0
Tactic:
exact case_floor_eventually_zero h
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.final_solution_general
Proof state before:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
h0 : 1 ≤ C
⊢ 1 = C → ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])
Tactic:
rintro rfl
Proof state after:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑1
h0 : 1 ≤ 1
⊢ ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])
Theorem: IMOSL.IMO2006A1.final_solution_general
Proof state before:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑1
h0 : 1 ≤ 1
⊢ ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])
Tactic:
exact case_floor_eventually_neg_one h
Proof state after:
no goals