Theorem: not_succ_surj (Instructor/Lectures/grad/sets_relations.lean)

State before:
⊢ ¬Surjective fun n => n + 1
Tactic:
unfold Surjective
State after:
⊢ ¬∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b

State before:
⊢ ¬∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b
Tactic:
intro h
State after:
h : ∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b
⊢ False

State before:
h : ∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b
⊢ False
Tactic:
let contra := h 0
State after:
h : ∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b
contra : ∃ a, (fun n => n + 1) a = 0 := h 0
⊢ False

State before:
h : ∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b
contra : ∃ a, (fun n => n + 1) a = 0 := h 0
⊢ False
Tactic:
simp [Nat.add] at contra
State after:
no goals