Theorem: HTPI.I_0_empty (HTPILib/Chap8Part1.lean)

State before:
⊢ empty (I 0)
Tactic:
define
State after:
⊢ ¬∃ x, x ∈ I 0

State before:
⊢ ¬∃ x, x ∈ I 0
Tactic:
by_contra h1
State after:
h1 : ∃ x, x ∈ I 0
⊢ False

State before:
h1 : ∃ x, x ∈ I 0
⊢ False
Tactic:
obtain (x : Nat) (h2 : x ∈ I 0) from h1
State after:
h1 : ∃ x, x ∈ I 0
x : ℕ
h2 : x ∈ I 0
⊢ False

State before:
h1 : ∃ x, x ∈ I 0
x : ℕ
h2 : x ∈ I 0
⊢ False
Tactic:
define at h2
State after:
h1 : ∃ x, x ∈ I 0
x : ℕ
h2 : x < 0
⊢ False

State before:
h1 : ∃ x, x ∈ I 0
x : ℕ
h2 : x < 0
⊢ False
Tactic:
linarith
State after:
no goals