Theorem: HTPI.eq_zero_of_I_zero_equinum (HTPILib/Chap8Part2.lean)

State before:
n : ℕ
h1 : I 0 ∼ I n
⊢ n = 0
Tactic:
rewrite [←numElts_def, zero_elts_iff_empty] at h1
State after:
n : ℕ
h1 : empty (I n)
⊢ n = 0

State before:
n : ℕ
h1 : empty (I n)
⊢ n = 0
Tactic:
contradict h1 with h2
State after:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ ∃ x, x ∈ I n

State before:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ ∃ x, x ∈ I n
Tactic:
apply Exists.intro 0
State after:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ 0 ∈ I n

State before:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ 0 ∈ I n
Tactic:
define
State after:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ 0 < n

State before:
n : ℕ
h1 : empty (I n)
h2 : ¬n = 0
⊢ 0 < n
Tactic:
show 0 < n from Nat.pos_of_ne_zero h2
State after:
no goals