Theorem: Cpdt.Chapter7.Computation.run_bottom (Cpdt/Chapter7/DomainTheory.lean)

State before:
α : Type
⊢ ∀ (v : α), ¬run bottom v
Tactic:
intro v
State after:
α : Type
v : α
⊢ ¬run bottom v

State before:
α : Type
v : α
⊢ ¬run bottom v
Tactic:
simp[run, bottom]
State after:
α : Type
v : α
⊢ ¬∃ n, False

State before:
α : Type
v : α
⊢ ¬∃ n, False
Tactic:
intro h
State after:
α : Type
v : α
h : ∃ n, False
⊢ False

State before:
α : Type
v : α
h : ∃ n, False
⊢ False
Tactic:
cases h
State after:
case intro
α : Type
v : α
w✝ : Nat
h✝ : False
⊢ False

State before:
case intro
α : Type
v : α
w✝ : Nat
h✝ : False
⊢ False
Tactic:
assumption
State after:
no goals