internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.Extra.CharTwo.symmDiff_singleton_sum_eq
Proof state before:
case pos
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
i : ι
S : Finset ι
h : i ∈ S
⊢ (symmDiff {i} S).sum f = f i + S.sum f
Tactic:
rw [symmDiff_singleton_eq_erase h, ← S.add_sum_erase f h, CharTwo.add_add_cancel_left]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.symmDiff_singleton_sum_eq
Proof state before:
case neg
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
i : ι
S : Finset ι
h : i ∉ S
⊢ (symmDiff {i} S).sum f = f i + S.sum f
Tactic:
rw [symmDiff_singleton_eq_insert h, Finset.sum_insert h]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.symmDiff_sum_eq
Proof state before:
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S T : Finset ι
⊢ (symmDiff S T).sum f = S.sum f + T.sum f
Tactic:
revert T
Proof state after:
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ ∀ (T : Finset ι), (symmDiff S T).sum f = S.sum f + T.sum f
Theorem: IMOSL.Extra.CharTwo.symmDiff_sum_eq
Proof state before:
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ ∀ (T : Finset ι), (symmDiff S T).sum f = S.sum f + T.sum f
Tactic:
apply Finset.induction
Proof state after:
case empty
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ (symmDiff S ∅).sum f = S.sum f + ∅.sum f

case insert
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s → (symmDiff S s).sum f = S.sum f + s.sum f → (symmDiff S (insert a s)).sum f = S.sum f + (insert a s).sum f
Theorem: IMOSL.Extra.CharTwo.symmDiff_sum_eq
Proof state before:
case empty
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ (symmDiff S ∅).sum f = S.sum f + ∅.sum f
Tactic:
have h : symmDiff S ∅ = S := by exact symmDiff_bot _
Proof state after:
case empty
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
h : symmDiff S ∅ = S
⊢ (symmDiff S ∅).sum f = S.sum f + ∅.sum f
Theorem: IMOSL.Extra.CharTwo.symmDiff_sum_eq
Proof state before:
case empty
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
h : symmDiff S ∅ = S
⊢ (symmDiff S ∅).sum f = S.sum f + ∅.sum f
Tactic:
rw [Finset.sum_empty, add_zero, h]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.symmDiff_sum_eq
Proof state before:
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ symmDiff S ∅ = S
Tactic:
exact symmDiff_bot _
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.symmDiff_sum_eq
Proof state before:
case insert
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s → (symmDiff S s).sum f = S.sum f + s.sum f → (symmDiff S (insert a s)).sum f = S.sum f + (insert a s).sum f
Tactic:
intro i T h h0
Proof state after:
case insert
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
i : ι
T : Finset ι
h : i ∉ T
h0 : (symmDiff S T).sum f = S.sum f + T.sum f
⊢ (symmDiff S (insert i T)).sum f = S.sum f + (insert i T).sum f
Theorem: IMOSL.Extra.CharTwo.symmDiff_sum_eq
Proof state before:
case insert
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
i : ι
T : Finset ι
h : i ∉ T
h0 : (symmDiff S T).sum f = S.sum f + T.sum f
⊢ (symmDiff S (insert i T)).sum f = S.sum f + (insert i T).sum f
Tactic:
rw [Finset.sum_insert h, add_left_comm, ← h0, ← symmDiff_singleton_eq_insert h,
  symmDiff_left_comm, symmDiff_singleton_sum_eq]
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.floor_f_natAbs_le
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ ⌊f r⌋.natAbs ≤ ⌊r⌋.natAbs
Tactic:
rw [← Nat.cast_le (α := ℤ), Int.cast_natAbs, Int.cast_natAbs,
  Int.cast_abs, Int.cast_id, Int.cast_abs, Int.cast_id]
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ |⌊f r⌋| ≤ |⌊r⌋|
Theorem: IMOSL.IMO2006A1.floor_f_natAbs_le
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ |⌊f r⌋| ≤ |⌊r⌋|
Tactic:
rcases le_total 0 ⌊r⌋ with h | h
Proof state after:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : 0 ≤ ⌊r⌋
⊢ |⌊f r⌋| ≤ |⌊r⌋|

case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ⌊r⌋ ≤ 0
⊢ |⌊f r⌋| ≤ |⌊r⌋|
Theorem: IMOSL.IMO2006A1.floor_f_natAbs_le
Proof state before:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : 0 ≤ ⌊r⌋
⊢ |⌊f r⌋| ≤ |⌊r⌋|
Tactic:
rw [abs_eq_self.mpr h, abs_eq_self.mpr (floor_f_nonneg h), ← Int.cast_le (R := R)]
Proof state after:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : 0 ≤ ⌊r⌋
⊢ ↑⌊f r⌋ ≤ ↑⌊r⌋
Theorem: IMOSL.IMO2006A1.floor_f_natAbs_le
Proof state before:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : 0 ≤ ⌊r⌋
⊢ ↑⌊f r⌋ ≤ ↑⌊r⌋
Tactic:
exact (Int.floor_le _).trans <| mul_le_of_le_one_right
  (Int.cast_nonneg.mpr h) (Int.fract_lt_one r).le
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.floor_f_natAbs_le
Proof state before:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ⌊r⌋ ≤ 0
⊢ |⌊f r⌋| ≤ |⌊r⌋|
Tactic:
rw [abs_eq_neg_self.mpr h, abs_eq_neg_self.mpr (floor_f_nonpos h),
  neg_le_neg_iff, Int.le_floor]
Proof state after:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ⌊r⌋ ≤ 0
⊢ ↑⌊r⌋ ≤ f r
Theorem: IMOSL.IMO2006A1.floor_f_natAbs_le
Proof state before:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ⌊r⌋ ≤ 0
⊢ ↑⌊r⌋ ≤ f r
Tactic:
exact le_mul_of_le_one_right (Int.cast_nonpos.mpr h) (Int.fract_lt_one r).le
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.floor_f_iter_natAbs_eventually_const
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋.natAbs) fun x => C
Tactic:
have ha : Antitone (λ k ↦ ⌊f^[k] r⌋.natAbs) := λ k m h0 ↦ by
  rcases Nat.exists_eq_add_of_le h0 with ⟨c, rfl⟩; simp only
  rw [Nat.add_comm, f.iterate_add_apply]
  exact floor_f_iter_natAbs_le _ c
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
ha : Antitone fun k => ⌊f^[k] r⌋.natAbs
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋.natAbs) fun x => C
Theorem: IMOSL.IMO2006A1.floor_f_iter_natAbs_eventually_const
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
ha : Antitone fun k => ⌊f^[k] r⌋.natAbs
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋.natAbs) fun x => C
Tactic:
rcases NatSeq_antitone_imp_const ha with ⟨C, N, ha⟩
Proof state after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
ha✝ : Antitone fun k => ⌊f^[k] r⌋.natAbs
C N : ℕ
ha : ∀ (n : ℕ), ⌊f^[n + N] r⌋.natAbs = C
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋.natAbs) fun x => C
Theorem: IMOSL.IMO2006A1.floor_f_iter_natAbs_eventually_const
Proof state before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
ha✝ : Antitone fun k => ⌊f^[k] r⌋.natAbs
C N : ℕ
ha : ∀ (n : ℕ), ⌊f^[n + N] r⌋.natAbs = C
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋.natAbs) fun x => C
Tactic:
exact ⟨C, N, 0, ha⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.floor_f_iter_natAbs_eventually_const
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k m : ℕ
h0 : k ≤ m
⊢ (fun k => ⌊f^[k] r⌋.natAbs) m ≤ (fun k => ⌊f^[k] r⌋.natAbs) k
Tactic:
rcases Nat.exists_eq_add_of_le h0 with ⟨c, rfl⟩
Proof state after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ (fun k => ⌊f^[k] r⌋.natAbs) (k + c) ≤ (fun k => ⌊f^[k] r⌋.natAbs) k
Theorem: IMOSL.IMO2006A1.floor_f_iter_natAbs_eventually_const
Proof state before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ (fun k => ⌊f^[k] r⌋.natAbs) (k + c) ≤ (fun k => ⌊f^[k] r⌋.natAbs) k
Tactic:
simp only
Proof state after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ ⌊f^[k + c] r⌋.natAbs ≤ ⌊f^[k] r⌋.natAbs
Theorem: IMOSL.IMO2006A1.floor_f_iter_natAbs_eventually_const
Proof state before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ ⌊f^[k + c] r⌋.natAbs ≤ ⌊f^[k] r⌋.natAbs
Tactic:
rw [Nat.add_comm, f.iterate_add_apply]
Proof state after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ ⌊f^[c] (f^[k] r)⌋.natAbs ≤ ⌊f^[k] r⌋.natAbs
Theorem: IMOSL.IMO2006A1.floor_f_iter_natAbs_eventually_const
Proof state before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ ⌊f^[c] (f^[k] r)⌋.natAbs ≤ ⌊f^[k] r⌋.natAbs
Tactic:
exact floor_f_iter_natAbs_le _ c
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.floor_f_iter_eventually_const
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
Tactic:
rcases floor_f_iter_natAbs_eventually_const r with ⟨C, N, K, h⟩
Proof state after:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋.natAbs) (k + N) = (fun x => C) (k + K)
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
Theorem: IMOSL.IMO2006A1.floor_f_iter_eventually_const
Proof state before:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋.natAbs) (k + N) = (fun x => C) (k + K)
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
Tactic:
refine ⟨C, N, K, λ n ↦ (Int.natAbs_eq_iff.mp (h n)).elim (λ h0 ↦ h0.trans ?_) id⟩
Proof state after:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋.natAbs) (k + N) = (fun x => C) (k + K)
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑((fun x => C) (n + K))
⊢ ↑((fun x => C) (n + K)) = (fun x => -↑C) (n + K)
Theorem: IMOSL.IMO2006A1.floor_f_iter_eventually_const
Proof state before:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋.natAbs) (k + N) = (fun x => C) (k + K)
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑((fun x => C) (n + K))
⊢ ↑((fun x => C) (n + K)) = (fun x => -↑C) (n + K)
Tactic:
simp only at h h0 ⊢
Proof state after:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
⊢ ↑C = -↑C
Theorem: IMOSL.IMO2006A1.floor_f_iter_eventually_const
Proof state before:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
⊢ ↑C = -↑C
Tactic:
rcases C.eq_zero_or_pos with rfl | h1
Proof state after:
case intro.intro.intro.inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N K n : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = 0
h0 : ⌊f^[n + N] r⌋ = ↑0
⊢ ↑0 = -↑0

case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
⊢ ↑C = -↑C
Theorem: IMOSL.IMO2006A1.floor_f_iter_eventually_const
Proof state before:
case intro.intro.intro.inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N K n : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = 0
h0 : ⌊f^[n + N] r⌋ = ↑0
⊢ ↑0 = -↑0

case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
⊢ ↑C = -↑C
Tactic:
rfl
Proof state after:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
⊢ ↑C = -↑C
Theorem: IMOSL.IMO2006A1.floor_f_iter_eventually_const
Proof state before:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
⊢ ↑C = -↑C
Tactic:
specialize h (n + 1)
Proof state after:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
h : ⌊f^[n + 1 + N] r⌋.natAbs = C
⊢ ↑C = -↑C
Theorem: IMOSL.IMO2006A1.floor_f_iter_eventually_const
Proof state before:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
h : ⌊f^[n + 1 + N] r⌋.natAbs = C
⊢ ↑C = -↑C
Tactic:
rw [Nat.add_right_comm, f.iterate_succ_apply'] at h
Proof state after:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
h : ⌊f (f^[n + N] r)⌋.natAbs = C
⊢ ↑C = -↑C
Theorem: IMOSL.IMO2006A1.floor_f_iter_eventually_const
Proof state before:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
h : ⌊f (f^[n + N] r)⌋.natAbs = C
⊢ ↑C = -↑C
Tactic:
replace h1 : 0 < ⌊f^[n + N] r⌋ := by rwa [h0, Nat.cast_pos]
Proof state after:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h : ⌊f (f^[n + N] r)⌋.natAbs = C
h1 : 0 < ⌊f^[n + N] r⌋
⊢ ↑C = -↑C
Theorem: IMOSL.IMO2006A1.floor_f_iter_eventually_const
Proof state before:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h : ⌊f (f^[n + N] r)⌋.natAbs = C
h1 : 0 < ⌊f^[n + N] r⌋
⊢ ↑C = -↑C
Tactic:
rw [← h, Int.natCast_natAbs, abs_eq_self.mpr (floor_f_nonneg h1.le)] at h0
Proof state after:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ⌊f (f^[n + N] r)⌋
h : ⌊f (f^[n + N] r)⌋.natAbs = C
h1 : 0 < ⌊f^[n + N] r⌋
⊢ ↑C = -↑C
Theorem: IMOSL.IMO2006A1.floor_f_iter_eventually_const
Proof state before:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ⌊f (f^[n + N] r)⌋
h : ⌊f (f^[n + N] r)⌋.natAbs = C
h1 : 0 < ⌊f^[n + N] r⌋
⊢ ↑C = -↑C
Tactic:
exact absurd h0.symm (floor_f_lt_of_floor_pos h1).ne
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.floor_f_iter_eventually_const
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
h : ⌊f (f^[n + N] r)⌋.natAbs = C
⊢ 0 < ⌊f^[n + N] r⌋
Tactic:
rwa [h0, Nat.cast_pos]
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.case_floor_eventually_zero
Proof state before:
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:
rw [EventuallyEqual.const_right_iff] at h ⊢
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ∃ N, ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
⊢ ∃ N, ∀ (k : ℕ), f^[k + N] r = 0
Theorem: IMOSL.IMO2006A1.case_floor_eventually_zero
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ∃ N, ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
⊢ ∃ N, ∀ (k : ℕ), f^[k + N] r = 0
Tactic:
rcases h with ⟨N, h⟩
Proof state after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
⊢ ∃ N, ∀ (k : ℕ), f^[k + N] r = 0
Theorem: IMOSL.IMO2006A1.case_floor_eventually_zero
Proof state before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
⊢ ∃ N, ∀ (k : ℕ), f^[k + N] r = 0
Tactic:
refine ⟨N + 1, λ k ↦ ?_⟩
Proof state after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
k : ℕ
⊢ f^[k + (N + 1)] r = 0
Theorem: IMOSL.IMO2006A1.case_floor_eventually_zero
Proof state before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
k : ℕ
⊢ f^[k + (N + 1)] r = 0
Tactic:
rw [← Nat.add_assoc, f.iterate_succ_apply', f, h, Int.cast_zero, zero_mul]
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
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
Proof 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])
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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⟩
Proof 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])
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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, ?_, ?_⟩
Proof 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])
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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
Proof 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
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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
Proof 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
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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
Proof 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
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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 ↦ ?_))
Proof 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
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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
Proof 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
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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
Proof 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
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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
Proof 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
Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_one
Proof 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
Proof state after:
no goals
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 : ℕ
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]
Proof 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])
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
⊢ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [- -f^[N] r, -f^[N] r - 1])
Tactic:
refine ⟨N, 0, λ k ↦ ?_⟩
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 : ℕ
⊢ (fun x => f^[x] r) (k + N) = NatSeq_ofList [- -f^[N] r, -f^[N] r - 1] (k + 0)