Theorem: extraction_ge (GlimpseOfLean/Solutions/Topics/SequenceLimits.lean)

State before:
φ : ℕ → ℕ
⊢ extraction φ → ∀ (N N' : ℕ), ∃ n ≥ N', φ n ≥ N
Tactic:
intro h N N'
State after:
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ ∃ n ≥ N', φ n ≥ N

State before:
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ ∃ n ≥ N', φ n ≥ N
Tactic:
use max N N'
State after:
case h
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N' ∧ φ (max N N') ≥ N

State before:
case h
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N' ∧ φ (max N N') ≥ N
Tactic:
constructor
State after:
case h.left
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N'

case h.right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N

State before:
case h.left
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N'

case h.right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N
Tactic:
apply le_max_right
State after:
case h.right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N

State before:
case h.right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N
Tactic:
calc
  N ≤ max N N' := by apply le_max_left
  _ ≤ φ (max N N') := by apply id_le_extraction' h
State after:
no goals

State before:
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ N ≤ max N N'
Tactic:
apply le_max_left
State after:
no goals

State before:
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≤ φ (max N N')
Tactic:
apply id_le_extraction' h
State after:
no goals