internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2006A1.final_solution_general
Proof state before:
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 * ε
Tactic:
intro h0
Proof state after:
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
h0 : 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_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
h0 : 1 < C
⊢ ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
exact ⟨C, h0, case_floor_eventually_neg_of_one_lt h0 h⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.Archimedean_f_iter_classification
Proof state before:
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
⊢ (∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε) →
    ∃ C, 1 < C ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2
Tactic:
rintro ⟨C, h, ε, h0, h1⟩
Proof state after:
case intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
h : 1 < C
ε : R
h0 : Infinitesimal ε
h1 : EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
⊢ ∃ C, 1 < C ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2
Theorem: IMOSL.IMO2006A1.Archimedean_f_iter_classification
Proof state before:
case intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
h : 1 < C
ε : R
h0 : Infinitesimal ε
h1 : EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
⊢ ∃ C, 1 < C ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2
Tactic:
simp only [h0.zero_of_Archimedean, mul_zero, add_zero] at h1
Proof state after:
case intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
h : 1 < C
ε : R
h0 : Infinitesimal ε
h1 : EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2
⊢ ∃ C, 1 < C ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2
Theorem: IMOSL.IMO2006A1.Archimedean_f_iter_classification
Proof state before:
case intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
h : 1 < C
ε : R
h0 : Infinitesimal ε
h1 : EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2
⊢ ∃ C, 1 < C ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2
Tactic:
exact ⟨C, h, h1⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.final_solution
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2006A1.final_solution
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2006A1.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2006A1.final_solution
Proof 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 ↦ ?_⟩
Proof 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
Theorem: IMOSL.IMO2006A1.final_solution
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2006A1.final_solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.final_solution
Proof 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]
Proof 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)
Theorem: IMOSL.IMO2006A1.final_solution
Proof 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] _
Proof state after:
no goals
Theorem: IMOSL.IMO2006A1.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2006A1.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2006A1.final_solution
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2021A3.targetSum_general_lower_bound
Proof state before:
a : ℕ
l : List ℕ
⊢ (map Nat.succ (a :: l)).prod ≤ 2 ^ targetSum (a :: l) * (a :: l).length.factorial
Tactic:
rw [map_cons, prod_cons, targetSum, pow_add,
  length_cons, Nat.factorial_succ, mul_mul_mul_comm]
Proof state after:
a : ℕ
l : List ℕ
⊢ a.succ * (map Nat.succ l).prod ≤ 2 ^ (a / l.length.succ) * (l.length + 1) * (2 ^ targetSum l * l.length.factorial)
Theorem: IMOSL.IMO2021A3.targetSum_general_lower_bound
Proof state before:
a : ℕ
l : List ℕ
⊢ a.succ * (map Nat.succ l).prod ≤ 2 ^ (a / l.length.succ) * (l.length + 1) * (2 ^ targetSum l * l.length.factorial)
Tactic:
exact Nat.mul_le_mul (succ_le_mul_two_pow_div a l.length.succ_pos)
  (targetSum_general_lower_bound l)
Proof state after:
no goals
Theorem: IMOSL.IMO2021A3.targetSum_perm_iota_n_lower_bound
Proof state before:
l : List ℕ
n : ℕ
h : l ~ iota n
⊢ n.size ≤ targetSum l
Tactic:
have h0 := targetSum_general_lower_bound l
Proof state after:
l : List ℕ
n : ℕ
h : l ~ iota n
h0 : (map Nat.succ l).prod ≤ 2 ^ targetSum l * l.length.factorial
⊢ n.size ≤ targetSum l
Theorem: IMOSL.IMO2021A3.targetSum_perm_iota_n_lower_bound
Proof state before:
l : List ℕ
n : ℕ
h : l ~ iota n
h0 : (map Nat.succ l).prod ≤ 2 ^ targetSum l * l.length.factorial
⊢ n.size ≤ targetSum l
Tactic:
rw [(h.map Nat.succ).prod_eq, h.length_eq,
  prod_map_succ_iota, length_iota] at h0
Proof state after:
l : List ℕ
n : ℕ
h : l ~ iota n
h0 : (n + 1).factorial ≤ 2 ^ targetSum l * n.factorial
⊢ n.size ≤ targetSum l
Theorem: IMOSL.IMO2021A3.targetSum_perm_iota_n_lower_bound
Proof state before:
l : List ℕ
n : ℕ
h : l ~ iota n
h0 : (n + 1).factorial ≤ 2 ^ targetSum l * n.factorial
⊢ n.size ≤ targetSum l
Tactic:
exact Nat.size_le.mpr (Nat.le_of_mul_le_mul_right h0 n.factorial_pos)
Proof state after:
no goals
Theorem: IMOSL.IMO2021A3.iota_map_add_append_iota_eq_iota
Proof state before:
n k : ℕ
⊢ map n.add (iota (k + 1)) ++ iota n = iota (n + (k + 1))
Tactic:
rw [iota_succ, map_cons, cons_append]
Proof state after:
n k : ℕ
⊢ n.add (k + 1) :: (map n.add (iota k) ++ iota n) = iota (n + (k + 1))
Theorem: IMOSL.IMO2021A3.iota_map_add_append_iota_eq_iota
Proof state before:
n k : ℕ
⊢ n.add (k + 1) :: (map n.add (iota k) ++ iota n) = iota (n + (k + 1))
Tactic:
exact congr_arg₂ _ rfl (iota_map_add_append_iota_eq_iota n k)
Proof state after:
no goals
Theorem: IMOSL.IMO2021A3.lowerBoundMk_perm_iota
Proof state before:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ lowerBoundMk (Nat.bit false (k + 1)) ~ iota (Nat.bit false (k + 1))
Tactic:
rw [lowerBoundMk_bit0_succ, Nat.bit_false, Nat.bit0_val]
Proof state after:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ map (k + 1).add (iota k) ++ (2 * k + 2) :: lowerBoundMk (k + 1) ~ iota (2 * (k + 1))
Theorem: IMOSL.IMO2021A3.lowerBoundMk_perm_iota
Proof state before:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ map (k + 1).add (iota k) ++ (2 * k + 2) :: lowerBoundMk (k + 1) ~ iota (2 * (k + 1))
Tactic:
refine perm_middle.trans (((h.append_left _).trans ?_).cons _)
Proof state after:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ map (k + 1).add (iota k) ++ iota (k + 1) ~ iota (Nat.mul 2 k + 1)
Theorem: IMOSL.IMO2021A3.lowerBoundMk_perm_iota
Proof state before:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ map (k + 1).add (iota k) ++ iota (k + 1) ~ iota (Nat.mul 2 k + 1)
Tactic:
rw [iota_map_add_append_iota_eq_iota, add_right_comm, ← two_mul]
Proof state after:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ iota (2 * k + 1) ~ iota (Nat.mul 2 k + 1)
Theorem: IMOSL.IMO2021A3.lowerBoundMk_perm_iota
Proof state before:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ iota (2 * k + 1) ~ iota (Nat.mul 2 k + 1)
Tactic:
exact Perm.refl _
Proof state after:
no goals
Theorem: IMOSL.IMO2021A3.lowerBoundMk_perm_iota
Proof state before:
b : Bool
n✝ n : ℕ
h : lowerBoundMk n ~ iota n
⊢ lowerBoundMk (Nat.bit true n) ~ iota (Nat.bit true n)
Tactic:
rw [lowerBoundMk_bit1, Nat.bit_true, Nat.bit1_val]
Proof state after:
b : Bool
n✝ n : ℕ
h : lowerBoundMk n ~ iota n
⊢ map n.add (iota n) ++ (2 * n + 1) :: lowerBoundMk n ~ iota (2 * n + 1)
Theorem: IMOSL.IMO2021A3.lowerBoundMk_perm_iota
Proof state before:
b : Bool
n✝ n : ℕ
h : lowerBoundMk n ~ iota n
⊢ map n.add (iota n) ++ (2 * n + 1) :: lowerBoundMk n ~ iota (2 * n + 1)
Tactic:
refine perm_middle.trans (((h.append_left _).trans ?_).cons _)
Proof state after:
b : Bool
n✝ n : ℕ
h : lowerBoundMk n ~ iota n
⊢ map n.add (iota n) ++ iota n ~ iota (2 * n)
Theorem: IMOSL.IMO2021A3.lowerBoundMk_perm_iota
Proof state before:
b : Bool
n✝ n : ℕ
h : lowerBoundMk n ~ iota n
⊢ map n.add (iota n) ++ iota n ~ iota (2 * n)
Tactic:
rw [iota_map_add_append_iota_eq_iota, ← two_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2021A3.targetSum_map_add_iota_length_succ
Proof state before:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ targetSum (map n.add (iota (k + 1)) ++ l) = targetSum l
Tactic:
rw [iota_succ, map_cons, cons_append, targetSum, length_cons,
  targetSum_map_add_iota_length_succ h k, Nat.add_eq_right]
Proof state after:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ n.add (k + 1) / (map n.add (iota k) ++ l).length.succ = 0
Theorem: IMOSL.IMO2021A3.targetSum_map_add_iota_length_succ
Proof state before:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ n.add (k + 1) / (map n.add (iota k) ++ l).length.succ = 0
Tactic:
refine Nat.div_eq_of_lt ?_
Proof state after:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ n.add (k + 1) < (map n.add (iota k) ++ l).length.succ
Theorem: IMOSL.IMO2021A3.targetSum_map_add_iota_length_succ
Proof state before:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ n.add (k + 1) < (map n.add (iota k) ++ l).length.succ
Tactic:
rw [length_append, length_map, length_iota, h]
Proof state after:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ n.add (k + 1) < (k + n.succ).succ
Theorem: IMOSL.IMO2021A3.lowerBoundMk_targetSum
Proof state before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n k : ℕ
h : targetSum (lowerBoundMk (k + 1)) = (k + 1).size
⊢ targetSum (lowerBoundMk (Nat.bit false (k + 1))) = (Nat.bit false (k + 1)).size
Tactic:
have h0 : ((2 * k + 2) :: lowerBoundMk (k + 1)).length = (k + 1).succ :=
  congr_arg Nat.succ (lowerBoundMk_length (k + 1))
Proof state after:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n k : ℕ
h : targetSum (lowerBoundMk (k + 1)) = (k + 1).size
h0 : ((2 * k + 2) :: lowerBoundMk (k + 1)).length = (k + 1).succ
⊢ targetSum (lowerBoundMk (Nat.bit false (k + 1))) = (Nat.bit false (k + 1)).size
Theorem: IMOSL.IMO2021A3.lowerBoundMk_targetSum
Proof state before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n k : ℕ
h : targetSum (lowerBoundMk (k + 1)) = (k + 1).size
h0 : ((2 * k + 2) :: lowerBoundMk (k + 1)).length = (k + 1).succ
⊢ targetSum (lowerBoundMk (Nat.bit false (k + 1))) = (Nat.bit false (k + 1)).size
Tactic:
rw [lowerBoundMk_bit0_succ, Nat.bit_false, Nat.size_bit0 k.succ_ne_zero,
  (k + 1).size.succ_eq_add_one, targetSum_map_add_iota_length_succ h0,
  targetSum, h0, h, add_comm, Nat.add_right_inj]
Proof state after:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n k : ℕ
h : targetSum (lowerBoundMk (k + 1)) = (k + 1).size
h0 : ((2 * k + 2) :: lowerBoundMk (k + 1)).length = (k + 1).succ
⊢ (2 * k + 2) / (k + 1).succ = 1
Theorem: IMOSL.IMO2021A3.lowerBoundMk_targetSum
Proof state before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n k : ℕ
h : targetSum (lowerBoundMk (k + 1)) = (k + 1).size
h0 : ((2 * k + 2) :: lowerBoundMk (k + 1)).length = (k + 1).succ
⊢ (2 * k + 2) / (k + 1).succ = 1
Tactic:
exact Nat.div_eq_of_lt_le
  ((one_mul _).trans_le <| Nat.add_le_add_right (X0 _) 2)
  (Nat.mul_lt_mul_of_pos_left (k + 1).lt_succ_self X)
Proof state after:
no goals
Theorem: IMOSL.IMO2021A3.lowerBoundMk_targetSum
Proof state before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n✝ n : ℕ
h : targetSum (lowerBoundMk n) = n.size
⊢ targetSum (lowerBoundMk (Nat.bit true n)) = (Nat.bit true n).size
Tactic:
have h0 : ((2 * n + 1) :: lowerBoundMk n).length = n.succ :=
  congr_arg Nat.succ (lowerBoundMk_length n)
Proof state after:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n✝ n : ℕ
h : targetSum (lowerBoundMk n) = n.size
h0 : ((2 * n + 1) :: lowerBoundMk n).length = n.succ
⊢ targetSum (lowerBoundMk (Nat.bit true n)) = (Nat.bit true n).size
Theorem: IMOSL.IMO2021A3.lowerBoundMk_targetSum
Proof state before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n✝ n : ℕ
h : targetSum (lowerBoundMk n) = n.size
h0 : ((2 * n + 1) :: lowerBoundMk n).length = n.succ
⊢ targetSum (lowerBoundMk (Nat.bit true n)) = (Nat.bit true n).size
Tactic:
rw [lowerBoundMk_bit1, Nat.bit_true, Nat.size_bit1,
  targetSum_map_add_iota_length_succ h0, targetSum, h0, h,
  n.size.succ_eq_add_one, add_comm, Nat.add_right_inj]
Proof state after:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n✝ n : ℕ
h : targetSum (lowerBoundMk n) = n.size
h0 : ((2 * n + 1) :: lowerBoundMk n).length = n.succ
⊢ (2 * n + 1) / n.succ = 1
Theorem: IMOSL.IMO2021A3.lowerBoundMk_targetSum
Proof state before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n✝ n : ℕ
h : targetSum (lowerBoundMk n) = n.size
h0 : ((2 * n + 1) :: lowerBoundMk n).length = n.succ
⊢ (2 * n + 1) / n.succ = 1
Tactic:
exact Nat.div_eq_of_lt_le
  ((one_mul _).trans_le <| Nat.succ_le_succ (X0 _)) (Nat.le_refl _)
Proof state after:
no goals
Theorem: IMOSL.IMO2014A1.d_zero
Proof state before:
z : ℕ → ℤ
⊢ d z 0 = z 0
Tactic:
rw [d, sum_range_one, Int.Nat.cast_ofNat_Int, Int.zero_mul, sub_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2014A1.d_succ
Proof state before:
z : ℕ → ℤ
n : ℕ
⊢ d z (n + 1) = (range (n + 1)).sum z - ↑n * z (n + 1)
Tactic:
rw [d, sum_range_succ, Int.natCast_add, Int.natCast_one,
  add_one_mul (α := ℤ), add_sub_add_right_eq_sub]
Proof state after:
no goals
Theorem: IMOSL.IMO2014A1.d_one
Proof state before:
z : ℕ → ℤ
⊢ d z 1 = z 0
Tactic:
rw [d_succ, sum_range_one, Nat.cast_zero, zero_mul, sub_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2014A1.main_lemma
Proof state before:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ d z (n + 1) ≤ d z n - ↑n
Tactic:
rw [d_succ, d, sub_sub, ← mul_add_one (α := ℤ)]
Proof state after:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ (range (n + 1)).sum z - ↑n * z (n + 1) ≤ (range (n + 1)).sum z - ↑n * (z n + 1)
Theorem: IMOSL.IMO2014A1.main_lemma
Proof state before:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ (range (n + 1)).sum z - ↑n * z (n + 1) ≤ (range (n + 1)).sum z - ↑n * (z n + 1)
Tactic:
exact Int.sub_le_sub_left
  (Int.mul_le_mul_of_nonneg_left (h n.lt_succ_self) (Int.ofNat_zero_le n)) _
Proof state after:
no goals
Theorem: IMOSL.IMO2014A1.binom_bound
Proof state before:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ d z (n + 1) ≤ z 0 - ↑((n + 1).choose 2)
Tactic:
rw [Nat.choose, Nat.choose_one_right, Nat.cast_add,
  ← sub_sub, sub_right_comm]
Proof state after:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ d z (n + 1) ≤ z 0 - ↑(n.choose (1 + 1)) - ↑n
Theorem: IMOSL.IMO2014A1.binom_bound
Proof state before:
z : ℕ → ℤ
h : StrictMono z
n : ℕ
⊢ d z (n + 1) ≤ z 0 - ↑(n.choose (1 + 1)) - ↑n
Tactic:
exact Int.le_sub_right_of_add_le <|
  (Int.add_le_of_le_sub_right (main_lemma h n)).trans (binom_bound n)
Proof state after:
no goals
Theorem: IMOSL.IMO2014A1.final_solution_part2
Proof state before:
z : ℕ → ℤ
h : StrictMono z
h0 : 0 < z 0
N : ℕ
⊢ N = greatestDPos h ↔ ↑N * z N < (range (N + 1)).sum z ∧ (range (N + 1)).sum z ≤ ↑N * z (N + 1)
Tactic:
rw [eq_greatestDPos_iff h h0, d_succ]
Proof state after:
z : ℕ → ℤ
h : StrictMono z
h0 : 0 < z 0
N : ℕ
⊢ 0 < d z N ∧ (range (N + 1)).sum z - ↑N * z (N + 1) ≤ 0 ↔
    ↑N * z N < (range (N + 1)).sum z ∧ (range (N + 1)).sum z ≤ ↑N * z (N + 1)
Theorem: IMOSL.IMO2014A1.final_solution_part2
Proof state before:
z : ℕ → ℤ
h : StrictMono z
h0 : 0 < z 0
N : ℕ
⊢ 0 < d z N ∧ (range (N + 1)).sum z - ↑N * z (N + 1) ≤ 0 ↔
    ↑N * z N < (range (N + 1)).sum z ∧ (range (N + 1)).sum z ≤ ↑N * z (N + 1)
Tactic:
exact and_congr sub_pos sub_nonpos
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.add
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ k • |ε₁ + ε₂| < 1
Tactic:
apply (nsmul_le_nsmul_right (abs_add ε₁ ε₂) k).trans_lt
Proof state after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ k • (|ε₁| + |ε₂|) < 1
Theorem: IMOSL.Extra.Infinitesimal.add
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ k • (|ε₁| + |ε₂|) < 1
Tactic:
apply lt_of_nsmul_lt_nsmul_right 2
Proof state after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ 2 • k • (|ε₁| + |ε₂|) < 2 • 1
Theorem: IMOSL.Extra.Infinitesimal.add
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ 2 • k • (|ε₁| + |ε₂|) < 2 • 1
Tactic:
rw [← mul_nsmul', nsmul_add, two_nsmul]
Proof state after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ (2 * k) • |ε₁| + (2 * k) • |ε₂| < 1 + 1