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

State before:
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ ∃ k ≥ m, k + 1 = n
Tactic:
use n - 1
State after:
case h
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ n - 1 ≥ m ∧ n - 1 + 1 = n

State before:
case h
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ n - 1 ≥ m ∧ n - 1 + 1 = n
Tactic:
constructor
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

State before:
case h.left
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ n - 1 ≥ m
Tactic:
exact?
State after:
no goals

State before:
case h.right
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ n - 1 + 1 = n
Tactic:
have : 1 ≤ n := by exact?
State after:
case h.right
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
this : 1 ≤ n
⊢ n - 1 + 1 = n

State before:
case h.right
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
this : 1 ≤ n
⊢ n - 1 + 1 = n
Tactic:
exact?
State after:
no goals

State before:
s t : ℕ → ℕ
k n m : ℕ
hn : n ≥ m + 1
⊢ 1 ≤ n
Tactic:
exact?
State after:
no goals