Theorem: Term.mem_pos (WTA.lean)

State before:
i : Nat
w : Nat⋆
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
⊢ i⬝w ∈ Hom.hom pos (app σ cs) → ∃ h, w ∈ Hom.hom pos (cs { val := i, isLt := h })
Tactic:
intro h
State after:
i : Nat
w : Nat⋆
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
h : i⬝w ∈ Hom.hom pos (app σ cs)
⊢ ∃ h, w ∈ Hom.hom pos (cs { val := i, isLt := h })

State before:
i : Nat
w : Nat⋆
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
h : i⬝w ∈ Hom.hom pos (app σ cs)
⊢ ∃ h, w ∈ Hom.hom pos (cs { val := i, isLt := h })
Tactic:
rw [pos_app] at h
State after:
i : Nat
w : Nat⋆
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
h :
  i⬝w ∈ fun x =>
    match x with
    | [] => True
    | i :: tl => ∃ h, tl ∈ Hom.hom pos (cs { val := i, isLt := h })
⊢ ∃ h, w ∈ Hom.hom pos (cs { val := i, isLt := h })

State before:
i : Nat
w : Nat⋆
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
h :
  i⬝w ∈ fun x =>
    match x with
    | [] => True
    | i :: tl => ∃ h, tl ∈ Hom.hom pos (cs { val := i, isLt := h })
⊢ ∃ h, w ∈ Hom.hom pos (cs { val := i, isLt := h })
Tactic:
simp [Membership.mem] at h
State after:
i : Nat
w : Nat⋆
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
h : ∃ h, Hom.hom pos (cs { val := i, isLt := h }) w
⊢ ∃ h, w ∈ Hom.hom pos (cs { val := i, isLt := h })

State before:
i : Nat
w : Nat⋆
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
h : ∃ h, Hom.hom pos (cs { val := i, isLt := h }) w
⊢ ∃ h, w ∈ Hom.hom pos (cs { val := i, isLt := h })
Tactic:
exact h
State after:
no goals