Theorem: Regex.NFA.zero_lt_size (Regex/NFA/Basic.lean)

State before:
nfa : NFA
⊢ 0 < nfa.nodes.size
Tactic:
apply Nat.zero_lt_of_ne_zero
State after:
case h
nfa : NFA
⊢ nfa.nodes.size ≠ 0

State before:
case h
nfa : NFA
⊢ nfa.nodes.size ≠ 0
Tactic:
intro h
State after:
case h
nfa : NFA
h : nfa.nodes.size = 0
⊢ False

State before:
case h
nfa : NFA
h : nfa.nodes.size = 0
⊢ False
Tactic:
exact (h ▸ nfa.start).elim0
State after:
no goals