internlm/Lean-Github huggingface dataset:
Theorem: exercise2_6
Proof state before:
case h
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
⊢ ∀ n ≥ max N₁ N₂, k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Tactic:
intro n hn
Proof state after:
case h
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ max N₁ N₂
⊢ k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Theorem: exercise2_6
Proof state before:
case h
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ max N₁ N₂
⊢ k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Tactic:
rw [useful_fact] at hn
Proof state after:
case h
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Theorem: exercise2_6
Proof state before:
case h
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Tactic:
simp
Proof state after:
case h
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ k * (t₁ n + t₂ n) ≤ s₁ n + s₂ n
Theorem: exercise2_6
Proof state before:
case h
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ k * (t₁ n + t₂ n) ≤ s₁ n + s₂ n
Tactic:
rw [mul_add]
Proof state after:
case h
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ k * t₁ n + k * t₂ n ≤ s₁ n + s₂ n
Theorem: exercise2_6
Proof state before:
case h
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ k * t₁ n + k * t₂ n ≤ s₁ n + s₂ n
Tactic:
gcongr
Proof state after:
case h.h₁
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ k * t₁ n ≤ s₁ n

case h.h₂
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ k * t₂ n ≤ s₂ n
Theorem: exercise2_6
Proof state before:
case h.h₁
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ k * t₁ n ≤ s₁ n
Tactic:
apply hN₁
Proof state after:
case h.h₁.a
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ n ≥ N₁
Theorem: exercise2_6
Proof state before:
case h.h₁.a
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ n ≥ N₁
Tactic:
exact hn.1
Proof state after:
no goals
Theorem: exercise2_6
Proof state before:
case h.h₂
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ k * t₂ n ≤ s₂ n
Tactic:
apply hN₂
Proof state after:
case h.h₂.a
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ n ≥ N₂
Theorem: exercise2_6
Proof state before:
case h.h₂.a
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
n : ℕ
hn : n ≥ N₁ ∧ n ≥ N₂
⊢ n ≥ N₂
Tactic:
exact hn.2
Proof state after:
no goals
Theorem: exercise2_7
Proof state before:
s t : ℕ → ℕ
k : ℕ
⊢ ∃ s, EventuallyGrowsFaster (fun n => s (n + 1)) s ∧ ∀ (n : ℕ), s n ≠ 0
Tactic:
use fun n ↦ n ^ n
Proof state after:
case h
s t : ℕ → ℕ
k : ℕ
⊢ (EventuallyGrowsFaster (fun n => (n + 1) ^ (n + 1)) fun n => n ^ n) ∧ ∀ (n : ℕ), n ^ n ≠ 0
Theorem: exercise2_7
Proof state before:
case h
s t : ℕ → ℕ
k : ℕ
⊢ (EventuallyGrowsFaster (fun n => (n + 1) ^ (n + 1)) fun n => n ^ n) ∧ ∀ (n : ℕ), n ^ n ≠ 0
Tactic:
constructor
Proof state after:
case h.left
s t : ℕ → ℕ
k : ℕ
⊢ EventuallyGrowsFaster (fun n => (n + 1) ^ (n + 1)) fun n => n ^ n

case h.right
s t : ℕ → ℕ
k : ℕ
⊢ ∀ (n : ℕ), n ^ n ≠ 0
Theorem: exercise2_7
Proof state before:
case h.left
s t : ℕ → ℕ
k : ℕ
⊢ EventuallyGrowsFaster (fun n => (n + 1) ^ (n + 1)) fun n => n ^ n
Tactic:
intro k
Proof state after:
case h.left
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * (fun n => n ^ n) n ≤ (fun n => (n + 1) ^ (n + 1)) n
Theorem: exercise2_7
Proof state before:
case h.left
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * (fun n => n ^ n) n ≤ (fun n => (n + 1) ^ (n + 1)) n
Tactic:
use k
Proof state after:
case h
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∀ n ≥ k, k * (fun n => n ^ n) n ≤ (fun n => (n + 1) ^ (n + 1)) n
Theorem: exercise2_7
Proof state before:
case h
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∀ n ≥ k, k * (fun n => n ^ n) n ≤ (fun n => (n + 1) ^ (n + 1)) n
Tactic:
intro n hn
Proof state after:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * (fun n => n ^ n) n ≤ (fun n => (n + 1) ^ (n + 1)) n
Theorem: exercise2_7
Proof state before:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * (fun n => n ^ n) n ≤ (fun n => (n + 1) ^ (n + 1)) n
Tactic:
simp
Proof state after:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * n ^ n ≤ (n + 1) ^ (n + 1)
Theorem: exercise2_7
Proof state before:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * n ^ n ≤ (n + 1) ^ (n + 1)
Tactic:
calc k * n ^ n ≤ n * n ^ n := by gcongr
  _ = n ^ (n + 1) := by ring
  _ ≤ (n + 1) ^ (n + 1) := by
    gcongr
    simp
Proof state after:
no goals
Theorem: exercise2_7
Proof state before:
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * n ^ n ≤ n * n ^ n
Tactic:
gcongr
Proof state after:
no goals
Theorem: exercise2_7
Proof state before:
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ n * n ^ n = n ^ (n + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: exercise2_7
Proof state before:
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ n ^ (n + 1) ≤ (n + 1) ^ (n + 1)
Tactic:
gcongr
Proof state after:
case hab
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ n ≤ n + 1
Theorem: exercise2_7
Proof state before:
case hab
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ n ≤ n + 1
Tactic:
simp
Proof state after:
no goals
Theorem: exercise2_7
Proof state before:
case h.right
s t : ℕ → ℕ
k : ℕ
⊢ ∀ (n : ℕ), n ^ n ≠ 0
Tactic:
intro n
Proof state after:
case h.right
s t : ℕ → ℕ
k n : ℕ
⊢ n ^ n ≠ 0
Theorem: exercise2_7
Proof state before:
case h.right
s t : ℕ → ℕ
k n : ℕ
⊢ n ^ n ≠ 0
Tactic:
apply pow_self_ne_zero
Proof state after:
no goals
Theorem: exercise2_7'
Proof state before:
s t : ℕ → ℕ
k : ℕ
⊢ ∃ s, EventuallyGrowsFaster (fun n => s (n + 1)) s ∧ ∀ (n : ℕ), s n ≠ 0
Tactic:
use fun n ↦ n!
Proof state after:
case h
s t : ℕ → ℕ
k : ℕ
⊢ (EventuallyGrowsFaster (fun n => (n + 1)!) fun n => n !) ∧ ∀ (n : ℕ), n ! ≠ 0
Theorem: exercise2_7'
Proof state before:
case h
s t : ℕ → ℕ
k : ℕ
⊢ (EventuallyGrowsFaster (fun n => (n + 1)!) fun n => n !) ∧ ∀ (n : ℕ), n ! ≠ 0
Tactic:
constructor
Proof state after:
case h.left
s t : ℕ → ℕ
k : ℕ
⊢ EventuallyGrowsFaster (fun n => (n + 1)!) fun n => n !

case h.right
s t : ℕ → ℕ
k : ℕ
⊢ ∀ (n : ℕ), n ! ≠ 0
Theorem: exercise2_7'
Proof state before:
case h.left
s t : ℕ → ℕ
k : ℕ
⊢ EventuallyGrowsFaster (fun n => (n + 1)!) fun n => n !
Tactic:
intro k
Proof state after:
case h.left
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * (fun n => n !) n ≤ (fun n => (n + 1)!) n
Theorem: exercise2_7'
Proof state before:
case h.left
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * (fun n => n !) n ≤ (fun n => (n + 1)!) n
Tactic:
use k
Proof state after:
case h
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∀ n ≥ k, k * (fun n => n !) n ≤ (fun n => (n + 1)!) n
Theorem: exercise2_7'
Proof state before:
case h
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∀ n ≥ k, k * (fun n => n !) n ≤ (fun n => (n + 1)!) n
Tactic:
intro n hn
Proof state after:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * (fun n => n !) n ≤ (fun n => (n + 1)!) n
Theorem: exercise2_7'
Proof state before:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * (fun n => n !) n ≤ (fun n => (n + 1)!) n
Tactic:
simp
Proof state after:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * n ! ≤ (n + 1)!
Theorem: exercise2_7'
Proof state before:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * n ! ≤ (n + 1)!
Tactic:
calc k * n! ≤ n * n! := by gcongr
  _ ≤ (n + 1) * n! := by
    gcongr
    exact?
  _ = (n + 1)! := by rfl
Proof state after:
no goals
Theorem: exercise2_7'
Proof state before:
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * n ! ≤ n * n !
Tactic:
gcongr
Proof state after:
no goals
Theorem: exercise2_7'
Proof state before:
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ n * n ! ≤ (n + 1) * n !
Tactic:
gcongr
Proof state after:
case bc
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ n ≤ n + 1
Theorem: exercise2_7'
Proof state before:
case bc
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ n ≤ n + 1
Tactic:
exact?
Proof state after:
no goals
Theorem: exercise2_7'
Proof state before:
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ (n + 1) * n ! = (n + 1)!
Tactic:
rfl
Proof state after:
no goals
Theorem: exercise2_7'
Proof state before:
case h.right
s t : ℕ → ℕ
k : ℕ
⊢ ∀ (n : ℕ), n ! ≠ 0
Tactic:
intro n
Proof state after:
case h.right
s t : ℕ → ℕ
k n : ℕ
⊢ n ! ≠ 0
Theorem: exercise2_7'
Proof state before:
case h.right
s t : ℕ → ℕ
k n : ℕ
⊢ n ! ≠ 0
Tactic:
exact?
Proof state after:
no goals
Theorem: useful_fact2
Proof state before:
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ ∃ k ≥ m, k + 1 = n
Tactic:
use n - 1
Proof state after:
case h
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ n - 1 ≥ m ∧ n - 1 + 1 = n
Theorem: useful_fact2
Proof state before:
case h
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ n - 1 ≥ m ∧ n - 1 + 1 = n
Tactic:
constructor
Proof state after:
case h.left
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ n - 1 ≥ m

case h.right
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ n - 1 + 1 = n
Theorem: useful_fact2
Proof state before:
case h.left
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ n - 1 ≥ m
Tactic:
exact?
Proof state after:
no goals
Theorem: useful_fact2
Proof state before:
case h.right
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ n - 1 + 1 = n
Tactic:
have : 1 ≤ n := by exact?
Proof state after:
case h.right
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
this : 1 ≤ n
⊢ n - 1 + 1 = n
Theorem: useful_fact2
Proof state before:
case h.right
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
this : 1 ≤ n
⊢ n - 1 + 1 = n
Tactic:
exact?
Proof state after:
no goals
Theorem: useful_fact2
Proof state before:
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ 1 ≤ n
Tactic:
exact?
Proof state after:
no goals
Theorem: exercise2_8
Proof state before:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
⊢ ∀ (k : ℕ), ∃ N, ∀ n ≥ N, s n ≥ k
Tactic:
have h3s : ∀ n, 1 ≤ s n := by
  intro n
  exact?
Proof state after:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
⊢ ∀ (k : ℕ), ∃ N, ∀ n ≥ N, s n ≥ k
Theorem: exercise2_8
Proof state before:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
⊢ ∀ (k : ℕ), ∃ N, ∀ n ≥ N, s n ≥ k
Tactic:
intro k
Proof state after:
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k : ℕ
⊢ ∃ N, ∀ n ≥ N, s n ≥ k
Theorem: exercise2_8
Proof state before:
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k : ℕ
⊢ ∃ N, ∀ n ≥ N, s n ≥ k
Tactic:
obtain ⟨N, hN⟩ := hs k
Proof state after:
case intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ n ≥ N, k * s n ≤ (fun n => s (n + 1)) n
⊢ ∃ N, ∀ n ≥ N, s n ≥ k
Theorem: exercise2_8
Proof state before:
case intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ n ≥ N, k * s n ≤ (fun n => s (n + 1)) n
⊢ ∃ N, ∀ n ≥ N, s n ≥ k
Tactic:
simp at hN
Proof state after:
case intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
⊢ ∃ N, ∀ n ≥ N, s n ≥ k
Theorem: exercise2_8
Proof state before:
case intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
⊢ ∃ N, ∀ n ≥ N, s n ≥ k
Tactic:
use N + 1
Proof state after:
case h
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
⊢ ∀ n ≥ N + 1, s n ≥ k
Theorem: exercise2_8
Proof state before:
case h
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
⊢ ∀ n ≥ N + 1, s n ≥ k
Tactic:
intros n hn
Proof state after:
case h
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
n : ℕ
hn : n ≥ N + 1
⊢ s n ≥ k
Theorem: exercise2_8
Proof state before:
case h
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
n : ℕ
hn : n ≥ N + 1
⊢ s n ≥ k
Tactic:
obtain ⟨n', hn'N, hn'n⟩ := useful_fact2 hn
Proof state after:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
⊢ s n ≥ k
Theorem: exercise2_8
Proof state before:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
⊢ s n ≥ k
Tactic:
specialize hN n' hn'N
Proof state after:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s (n' + 1)
⊢ s n ≥ k
Theorem: exercise2_8
Proof state before:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s (n' + 1)
⊢ s n ≥ k
Tactic:
rw [hn'n] at hN
Proof state after:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ s n ≥ k
Theorem: exercise2_8
Proof state before:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ s n ≥ k
Tactic:
calc k = k * 1 := by simp
  _ ≤ k * s n' := by
    gcongr
    apply h3s
  _ ≤ s n := by assumption
Proof state after:
no goals
Theorem: exercise2_8
Proof state before:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
⊢ ∀ (n : ℕ), 1 ≤ s n
Tactic:
intro n
Proof state after:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
n : ℕ
⊢ 1 ≤ s n
Theorem: exercise2_8
Proof state before:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
n : ℕ
⊢ 1 ≤ s n
Tactic:
exact?
Proof state after:
no goals
Theorem: exercise2_8
Proof state before:
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ k = k * 1
Tactic:
simp
Proof state after:
no goals
Theorem: exercise2_8
Proof state before:
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ k * 1 ≤ k * s n'
Tactic:
gcongr
Proof state after:
case bc
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ 1 ≤ s n'
Theorem: exercise2_8
Proof state before:
case bc
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ 1 ≤ s n'
Tactic:
apply h3s
Proof state after:
no goals
Theorem: exercise2_8
Proof state before:
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ k * s n' ≤ s n
Tactic:
assumption
Proof state after:
no goals
Theorem: exercise4_1
Proof state before:
n : ℕ
⊢ ∑ i in range (n + 1), ↑(i ^ 3) = (∑ i in range (n + 1), ↑i) ^ 2
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_2
Proof state before:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder ι
wf : WellFoundedLT ι
A C : ι → Set α
hC : ∀ (i : ι), C i = A i \ ⋃ j, ⋃ (_ : j < i), A j
⊢ Pairwise (Disjoint on C) ∧ ⋃ i, C i = ⋃ i, A i
Tactic:
have h := wf.wf.has_min
Proof state after:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder ι
wf : WellFoundedLT ι
A C : ι → Set α
hC : ∀ (i : ι), C i = A i \ ⋃ j, ⋃ (_ : j < i), A j
h : ∀ (s : Set ι), Set.Nonempty s → ∃ a ∈ s, ∀ x ∈ s, ¬x < a
⊢ Pairwise (Disjoint on C) ∧ ⋃ i, C i = ⋃ i, A i
Theorem: exercise4_2
Proof state before:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder ι
wf : WellFoundedLT ι
A C : ι → Set α
hC : ∀ (i : ι), C i = A i \ ⋃ j, ⋃ (_ : j < i), A j
h : ∀ (s : Set ι), Set.Nonempty s → ∃ a ∈ s, ∀ x ∈ s, ¬x < a
⊢ Pairwise (Disjoint on C) ∧ ⋃ i, C i = ⋃ i, A i
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_4
Proof state before:
n : ℕ
⊢ ¬Nat.Prime n ↔ n = 0 ∨ n = 1 ∨ ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
n : ℕ
hn : Nat.Prime (2 ^ n - 1)
⊢ Nat.Prime n
Tactic:
by_contra h2n
Proof state after:
n : ℕ
hn : Nat.Prime (2 ^ n - 1)
h2n : ¬Nat.Prime n
⊢ False
Theorem: exercise4_5
Proof state before:
n : ℕ
hn : Nat.Prime (2 ^ n - 1)
h2n : ¬Nat.Prime n
⊢ False
Tactic:
rw [exercise4_4] at h2n
Proof state after:
n : ℕ
hn : Nat.Prime (2 ^ n - 1)
h2n : n = 0 ∨ n = 1 ∨ ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
⊢ False
Theorem: exercise4_5
Proof state before:
n : ℕ
hn : Nat.Prime (2 ^ n - 1)
h2n : n = 0 ∨ n = 1 ∨ ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
⊢ False
Tactic:
obtain rfl|rfl|⟨a, b, ha, hb, rfl⟩ := h2n
Proof state after:
case inl
hn : Nat.Prime (2 ^ 0 - 1)
⊢ False

case inr.inl
hn : Nat.Prime (2 ^ 1 - 1)
⊢ False

case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ False
Theorem: exercise4_5
Proof state before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ False
Tactic:
have h : (2 : ℤ) ^ a - 1 ∣ (2 : ℤ) ^ (a * b) - 1
Proof state after:
case h
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 2 ^ a - 1 ∣ 2 ^ (a * b) - 1

case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False
Theorem: exercise4_5
Proof state before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False
Tactic:
have h2 : 2 ^ 2 ≤ 2 ^ a := by sorry
Proof state after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
⊢ False
Theorem: exercise4_5
Proof state before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
⊢ False
Tactic:
have h3 : 1 ≤ 2 ^ a := by sorry
Proof state after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ False
Theorem: exercise4_5
Proof state before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ False
Tactic:
have h4 : 2 ^ a - 1 ≠ 1 := by zify; simp [h3]; linarith
Proof state after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
⊢ False
Theorem: exercise4_5
Proof state before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
⊢ False
Tactic:
have h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1 := by
  apply tsub_lt_tsub_right_of_le h3
  sorry
Proof state after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
⊢ False
Theorem: exercise4_5
Proof state before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
⊢ False
Tactic:
have h6' : 2 ^ 0 ≤ 2 ^ (a * b) := by sorry
Proof state after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
⊢ False
Theorem: exercise4_5
Proof state before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
⊢ False
Tactic:
have h6 : 1 ≤ 2 ^ (a * b) := h6'
Proof state after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
⊢ False