Theorem: exercise2_6 (LeanCourse/Assignments/Solutions/Solutions2.lean)

State before:
s t : ℕ → ℕ
k : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
⊢ EventuallyGrowsFaster (s₁ + s₂) (t₁ + t₂)
Tactic:
intro k
State after:
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n

State before:
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Tactic:
obtain ⟨N₁, hN₁⟩ := h₁ k
State after:
case intro
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, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n

State before:
case intro
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, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Tactic:
obtain ⟨N₂, hN₂⟩ := h₂ k
State after:
case intro.intro
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, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n

State before:
case intro.intro
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, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Tactic:
use max N₁ N₂
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 ≥ max N₁ N₂, k * (t₁ + t₂) n ≤ (s₁ + s₂) n

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
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

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
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

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
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

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]
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

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
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

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₁
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₁

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
State after:
no goals

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₂
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₂

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
State after:
no goals