Theorem: Alphabet.card_pos (FormalSystems/Preliminaries/Alphabet.lean)

State before:
α : Type u_1
alphabet : Alphabet α
⊢ Fintype.card α > 0
Tactic:
apply Finset.card_pos.mpr
State after:
α : Type u_1
alphabet : Alphabet α
⊢ Finset.univ.Nonempty

State before:
α : Type u_1
alphabet : Alphabet α
⊢ Finset.univ.Nonempty
Tactic:
exists alphabet.default
State after:
α : Type u_1
alphabet : Alphabet α
⊢ default ∈ Finset.univ

State before:
α : Type u_1
alphabet : Alphabet α
⊢ default ∈ Finset.univ
Tactic:
exact alphabet.complete alphabet.default
State after:
no goals