Theorem: HW2.problem_1 (BrownCs22/Homework/Hw2sols.lean)

State before:
⊢ ∃ n, ∀ (x : ℕ), n ≤ x
Tactic:
existsi 0
State after:
⊢ ∀ (x : ℕ), 0 ≤ x

State before:
⊢ ∀ (x : ℕ), 0 ≤ x
Tactic:
intro x
State after:
x : ℕ
⊢ 0 ≤ x

State before:
x : ℕ
⊢ 0 ≤ x
Tactic:
linarith
State after:
no goals