Theorem: TreeDomain.ε_mem (WTA.lean)

State before:
W : Set (Nat⋆)
⊢ TreeDomain W → Word.ε ∈ W
Tactic:
intro h
State after:
W : Set (Nat⋆)
h : TreeDomain W
⊢ Word.ε ∈ W

State before:
W : Set (Nat⋆)
h : TreeDomain W
⊢ Word.ε ∈ W
Tactic:
apply h.prefixClosed .ε
State after:
W : Set (Nat⋆)
h : TreeDomain W
⊢ Word.ε ∈ Set.bUnion (Set.image Word.prefixes)

State before:
W : Set (Nat⋆)
h : TreeDomain W
⊢ Word.ε ∈ Set.bUnion (Set.image Word.prefixes)
Tactic:
simp [Set.bUnion, Membership.mem]
State after:
W : Set (Nat⋆)
h : TreeDomain W
⊢ ∃ m, Set.image Word.prefixes m ∧ m Word.ε

State before:
W : Set (Nat⋆)
h : TreeDomain W
⊢ ∃ m, Set.image Word.prefixes m ∧ m Word.ε
Tactic:
have ⟨m, _⟩ := Set.Nonempty.iff_exists_mem.mp h.nonempty
State after:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ ∃ m, Set.image Word.prefixes m ∧ m Word.ε

State before:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ ∃ m, Set.image Word.prefixes m ∧ m Word.ε
Tactic:
exists m.prefixes
State after:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Set.image Word.prefixes (Word.prefixes m) ∧ Word.prefixes m Word.ε

State before:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Set.image Word.prefixes (Word.prefixes m) ∧ Word.prefixes m Word.ε
Tactic:
constructor
State after:
case left
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Set.image Word.prefixes (Word.prefixes m)

case right
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Word.prefixes m Word.ε

State before:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Set.image Word.prefixes (Word.prefixes m)
Tactic:
case left => exists m
State after:
no goals

State before:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Word.prefixes m Word.ε
Tactic:
case right => apply Word.ε_mem_prefixes
State after:
no goals

State before:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Set.image Word.prefixes (Word.prefixes m)
Tactic:
exists m
State after:
no goals

State before:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Word.prefixes m Word.ε
Tactic:
apply Word.ε_mem_prefixes
State after:
no goals