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

State before:
⊢ Surjective Bool.not
Tactic:
unfold Surjective
State after:
⊢ ∀ (b : Bool), ∃ a, Bool.not a = b

State before:
⊢ ∀ (b : Bool), ∃ a, Bool.not a = b
Tactic:
intro b
State after:
b : Bool
⊢ ∃ a, Bool.not a = b

State before:
b : Bool
⊢ ∃ a, Bool.not a = b
Tactic:
cases b with 
| true => exact ⟨ false, rfl ⟩ 
| false => exact ⟨ true, rfl ⟩
State after:
no goals

State before:
case true

⊢ ∃ a, Bool.not a = true
Tactic:
exact ⟨ false, rfl ⟩
State after:
no goals

State before:
case false

⊢ ∃ a, Bool.not a = false
Tactic:
exact ⟨ true, rfl ⟩
State after:
no goals