Theorem: Term.pos_zero (WTA.lean)

State before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
⊢ Hom.hom pos (app σ (Vector.ε' h)) = Set.singleton Word.ε
Tactic:
simp [pos_app (H := H) σ (Vector.ε' h)]
State after:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
⊢ (fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) =
    Set.singleton Word.ε

State before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
⊢ (fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) =
    Set.singleton Word.ε
Tactic:
refine Set.mem_ext ?_
State after:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
⊢ ∀ (a : Nat⋆),
    (a ∈ fun x =>
        match x with
        | [] => True
        | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) ↔
      a ∈ Set.singleton Word.ε

State before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
⊢ ∀ (a : Nat⋆),
    (a ∈ fun x =>
        match x with
        | [] => True
        | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) ↔
      a ∈ Set.singleton Word.ε
Tactic:
intro w
State after:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ (w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) ↔
    w ∈ Set.singleton Word.ε

State before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ (w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) ↔
    w ∈ Set.singleton Word.ε
Tactic:
constructor
State after:
case mp
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ (w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) →
    w ∈ Set.singleton Word.ε

case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ w ∈ Set.singleton Word.ε →
    w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })

State before:
case mp
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ (w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) →
    w ∈ Set.singleton Word.ε

case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ w ∈ Set.singleton Word.ε →
    w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })
Tactic:
all_goals
  intro h'
  simp [Set.singleton, Membership.mem] at *
State after:
case mp
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' :
  match w with
  | [] => True
  | i :: tl => ∃ h_1, Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 }) tl
⊢ w = Word.ε

case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' : w = Word.ε
⊢ match w with
  | [] => True
  | i :: tl => ∃ h_1, Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 }) tl

State before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' : w = Word.ε
⊢ match w with
  | [] => True
  | i :: tl => ∃ h_1, Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 }) tl
Tactic:
case mpr => simp [h']
State after:
no goals

State before:
case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ w ∈ Set.singleton Word.ε →
    w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })
Tactic:
intro h'
State after:
case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' : w ∈ Set.singleton Word.ε
⊢ w ∈ fun x =>
    match x with
    | [] => True
    | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })

State before:
case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' : w ∈ Set.singleton Word.ε
⊢ w ∈ fun x =>
    match x with
    | [] => True
    | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })
Tactic:
simp [Set.singleton, Membership.mem] at *
State after:
case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' : w = Word.ε
⊢ match w with
  | [] => True
  | i :: tl => ∃ h_1, Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 }) tl

State before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' : w = Word.ε
⊢ match w with
  | [] => True
  | i :: tl => ∃ h_1, Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 }) tl
Tactic:
simp [h']
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' :
  match w with
  | [] => True
  | i :: tl => ∃ h_1, Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 }) tl
⊢ w = Word.ε
Tactic:
split at h'
State after:
case h_1
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
x✝ : Nat⋆
h' : True
⊢ [] = Word.ε

case h_2
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
x✝ : Nat⋆
i✝ : Nat
tl✝ : Nat⋆
h' : ∃ h_1, Hom.hom pos (Vector.ε' h { val := i✝, isLt := h_1 }) tl✝
⊢ i✝ :: tl✝ = Word.ε