Theorem: Term.algebra_iso_stringAlgebra (WTA.lean)

State before:
Γ : Type
inst✝ : Alphabet Γ
⊢ stringAlgebra Γ ≅ Term.algebra (RankedAlphabet.lift Γ) Empty
Tactic:
unfold Isomorphic
State after:
Γ : Type
inst✝ : Alphabet Γ
⊢ Nonempty (Iso (stringAlgebra Γ) (Term.algebra (RankedAlphabet.lift Γ) Empty))

State before:
Γ : Type
inst✝ : Alphabet Γ
⊢ Nonempty (Iso (stringAlgebra Γ) (Term.algebra (RankedAlphabet.lift Γ) Empty))
Tactic:
apply Nonempty.intro
State after:
case val
Γ : Type
inst✝ : Alphabet Γ
⊢ Iso (stringAlgebra Γ) (Term.algebra (RankedAlphabet.lift Γ) Empty)

State before:
case val
Γ : Type
inst✝ : Alphabet Γ
⊢ Iso (stringAlgebra Γ) (Term.algebra (RankedAlphabet.lift Γ) Empty)
Tactic:
exact {
  hom := treeₑ
  property := by
    intro σ w
    cases σ
    all_goals simp [Term.algebra, stringAlgebra]
    case none =>
      simp [Function.comp, treeₑ, Term.algebra]
      funext ⟨_, h⟩
      simp [RankedAlphabet.lift] at h
      contradiction
    case some σ =>
      simp [stringAlgebra, RankedAlphabet.lift] at w
      generalize hw : w ⟨0, stringAlgebra.proof_1⟩ = w'
      simp [treeₑ, Function.comp]
      funext ⟨i, hi⟩
      have hi : i = 0 := by 
        simp [RankedAlphabet.lift] at hi
        cases i
        case zero => rfl
        case succ => contradiction
      simp [hw, hi]
  bij := {
    inj := by 
      simp [Function.Injective]
      intro σ₁ σ₂ h
      induction σ₁ generalizing σ₂ <;> cases σ₂ <;> simp [treeₑ, Term.algebra] at *
      case cons.cons σ _ hi _ _ =>
        have ⟨h₁, h₂⟩ := h
        injection h₁ with h₁          
        have : Nonempty (Fin $ (RankedAlphabet.lift Γ).rank $ some σ) := 
          .intro ⟨0, by simp [RankedAlphabet.lift]⟩ 
        simp [h₁, hi _ (const_func_ext h₂)]
    surj := by
      simp [Function.Surjective]
      intro a
      induction a
      case var => contradiction
      case app σ w hi =>
        cases σ 
        case none => 
          exists .ε
          simp [treeₑ, Term.algebra]
          funext ⟨_, h⟩
          simp [RankedAlphabet.lift] at h
          contradiction
        case some σ => 
          have ⟨a, h⟩ := hi ⟨0, by simp [RankedAlphabet.lift]⟩
          exists σ⬝a
          simp [h, treeₑ]
          refine congrArg _ ?_
          funext ⟨i, hi⟩
          have hi : i = 0 := by 
            simp [RankedAlphabet.lift] at hi
            cases i
            case zero => rfl
            case succ => contradiction
          simp [hi]
  }
}
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
⊢ ∀ (σ : (RankedAlphabet.lift Γ).alphabet)
    (cs : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) σ),
    treeₑ (Algebra.θ (stringAlgebra Γ) σ cs) = Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) σ (treeₑ ∘ cs)
Tactic:
intro σ w
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : (RankedAlphabet.lift Γ).alphabet
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) σ
⊢ treeₑ (Algebra.θ (stringAlgebra Γ) σ w) = Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) σ (treeₑ ∘ w)

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : (RankedAlphabet.lift Γ).alphabet
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) σ
⊢ treeₑ (Algebra.θ (stringAlgebra Γ) σ w) = Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) σ (treeₑ ∘ w)
Tactic:
cases σ
State after:
case none
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ treeₑ (Algebra.θ (stringAlgebra Γ) none w) = Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) none (treeₑ ∘ w)

case some
Γ : Type
inst✝ : Alphabet Γ
val✝ : Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) (some val✝)
⊢ treeₑ (Algebra.θ (stringAlgebra Γ) (some val✝) w) =
    Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) (some val✝) (treeₑ ∘ w)

State before:
case none
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ treeₑ (Algebra.θ (stringAlgebra Γ) none w) = Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) none (treeₑ ∘ w)

case some
Γ : Type
inst✝ : Alphabet Γ
val✝ : Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) (some val✝)
⊢ treeₑ (Algebra.θ (stringAlgebra Γ) (some val✝) w) =
    Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) (some val✝) (treeₑ ∘ w)
Tactic:
all_goals simp [Term.algebra, stringAlgebra]
State after:
case none
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ treeₑ Word.ε = app none (treeₑ ∘ w)

case some
Γ : Type
inst✝ : Alphabet Γ
val✝ : Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) (some val✝)
⊢ treeₑ (val✝⬝w { val := 0, isLt := stringAlgebra.proof_1 }) = app (some val✝) (treeₑ ∘ w)

State before:
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ treeₑ Word.ε = app none (treeₑ ∘ w)
Tactic:
case none =>
  simp [Function.comp, treeₑ, Term.algebra]
  funext ⟨_, h⟩
  simp [RankedAlphabet.lift] at h
  contradiction
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ treeₑ (σ⬝w { val := 0, isLt := stringAlgebra.proof_1 }) = app (some σ) (treeₑ ∘ w)
Tactic:
case some σ =>
  simp [stringAlgebra, RankedAlphabet.lift] at w
  generalize hw : w ⟨0, stringAlgebra.proof_1⟩ = w'
  simp [treeₑ, Function.comp]
  funext ⟨i, hi⟩
  have hi : i = 0 := by 
    simp [RankedAlphabet.lift] at hi
    cases i
    case zero => rfl
    case succ => contradiction
  simp [hw, hi]
State after:
no goals

State before:
case some
Γ : Type
inst✝ : Alphabet Γ
val✝ : Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) (some val✝)
⊢ treeₑ (Algebra.θ (stringAlgebra Γ) (some val✝) w) =
    Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) (some val✝) (treeₑ ∘ w)
Tactic:
simp [Term.algebra, stringAlgebra]
State after:
case some
Γ : Type
inst✝ : Alphabet Γ
val✝ : Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) (some val✝)
⊢ treeₑ (val✝⬝w { val := 0, isLt := stringAlgebra.proof_1 }) = app (some val✝) (treeₑ ∘ w)

State before:
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ treeₑ Word.ε = app none (treeₑ ∘ w)
Tactic:
simp [Function.comp, treeₑ, Term.algebra]
State after:
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ (fun x => nomatch x) = fun x => treeₑ (w x)

State before:
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ (fun x => nomatch x) = fun x => treeₑ (w x)
Tactic:
funext ⟨_, h⟩
State after:
case h
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
val✝ : Nat
h : val✝ < RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ (nomatch { val := val✝, isLt := h }) = treeₑ (w { val := val✝, isLt := h })

State before:
case h
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
val✝ : Nat
h : val✝ < RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ (nomatch { val := val✝, isLt := h }) = treeₑ (w { val := val✝, isLt := h })
Tactic:
simp [RankedAlphabet.lift] at h
State after:
case h
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
val✝ : Nat
h : val✝ < 0
⊢ (nomatch { val := val✝, isLt := h }) = treeₑ (w { val := val✝, isLt := h })

State before:
case h
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
val✝ : Nat
h : val✝ < 0
⊢ (nomatch { val := val✝, isLt := h }) = treeₑ (w { val := val✝, isLt := h })
Tactic:
contradiction
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ treeₑ (σ⬝w { val := 0, isLt := stringAlgebra.proof_1 }) = app (some σ) (treeₑ ∘ w)
Tactic:
simp [stringAlgebra, RankedAlphabet.lift] at w
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
⊢ treeₑ (σ⬝w { val := 0, isLt := stringAlgebra.proof_1 }) = app (some σ) (treeₑ ∘ w)

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
⊢ treeₑ (σ⬝w { val := 0, isLt := stringAlgebra.proof_1 }) = app (some σ) (treeₑ ∘ w)
Tactic:
generalize hw : w ⟨0, stringAlgebra.proof_1⟩ = w'
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
⊢ treeₑ (σ⬝w') = app (some σ) (treeₑ ∘ w)

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
⊢ treeₑ (σ⬝w') = app (some σ) (treeₑ ∘ w)
Tactic:
simp [treeₑ, Function.comp]
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
⊢ (fun x => treeₑ w') = fun x => treeₑ (w x)

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
⊢ (fun x => treeₑ w') = fun x => treeₑ (w x)
Tactic:
funext ⟨i, hi⟩
State after:
case h
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ treeₑ w' = treeₑ (w { val := i, isLt := hi })

State before:
case h
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ treeₑ w' = treeₑ (w { val := i, isLt := hi })
Tactic:
have hi : i = 0 := by 
  simp [RankedAlphabet.lift] at hi
  cases i
  case zero => rfl
  case succ => contradiction
State after:
case h
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi✝ : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
hi : i = 0
⊢ treeₑ w' = treeₑ (w { val := i, isLt := hi✝ })

State before:
case h
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi✝ : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
hi : i = 0
⊢ treeₑ w' = treeₑ (w { val := i, isLt := hi✝ })
Tactic:
simp [hw, hi]
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ i = 0
Tactic:
simp [RankedAlphabet.lift] at hi
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi : i < 1
⊢ i = 0

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi : i < 1
⊢ i = 0
Tactic:
cases i
State after:
case zero
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
hi : Nat.zero < 1
⊢ Nat.zero = 0

case succ
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
n✝ : Nat
hi : Nat.succ n✝ < 1
⊢ Nat.succ n✝ = 0

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
hi : Nat.zero < 1
⊢ Nat.zero = 0
Tactic:
case zero => rfl
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
n✝ : Nat
hi : Nat.succ n✝ < 1
⊢ Nat.succ n✝ = 0
Tactic:
case succ => contradiction
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
hi : Nat.zero < 1
⊢ Nat.zero = 0
Tactic:
rfl
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
n✝ : Nat
hi : Nat.succ n✝ < 1
⊢ Nat.succ n✝ = 0
Tactic:
contradiction
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
⊢ Function.Injective
    { hom := treeₑ,
        property :=
          (_ :
            ∀ (σ : (RankedAlphabet.lift Γ).alphabet)
              (w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) σ),
              treeₑ (Algebra.θ (stringAlgebra Γ) σ w) =
                Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) σ (treeₑ ∘ w)) }.hom
Tactic:
simp [Function.Injective]
State after:
Γ : Type
inst✝ : Alphabet Γ
⊢ ∀ (a₁ a₂ : (stringAlgebra Γ).carrier), treeₑ a₁ = treeₑ a₂ → a₁ = a₂

State before:
Γ : Type
inst✝ : Alphabet Γ
⊢ ∀ (a₁ a₂ : (stringAlgebra Γ).carrier), treeₑ a₁ = treeₑ a₂ → a₁ = a₂
Tactic:
intro σ₁ σ₂ h
State after:
Γ : Type
inst✝ : Alphabet Γ
σ₁ σ₂ : (stringAlgebra Γ).carrier
h : treeₑ σ₁ = treeₑ σ₂
⊢ σ₁ = σ₂

State before:
Γ : Type
inst✝ : Alphabet Γ
σ₁ σ₂ : (stringAlgebra Γ).carrier
h : treeₑ σ₁ = treeₑ σ₂
⊢ σ₁ = σ₂
Tactic:
induction σ₁ generalizing σ₂ <;> cases σ₂ <;> simp [treeₑ, Term.algebra] at *
State after:
case cons.cons
Γ : Type
inst✝ : Alphabet Γ
head✝¹ : Γ
tail✝¹ : List Γ
tail_ih✝ : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some head✝¹ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
tail✝¹ : List Γ
hi : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some σ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
⊢ σ :: tail✝¹ = head✝ :: tail✝
Tactic:
case cons.cons σ _ hi _ _ =>
  have ⟨h₁, h₂⟩ := h
  injection h₁ with h₁          
  have : Nonempty (Fin $ (RankedAlphabet.lift Γ).rank $ some σ) := 
    .intro ⟨0, by simp [RankedAlphabet.lift]⟩ 
  simp [h₁, hi _ (const_func_ext h₂)]
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
tail✝¹ : List Γ
hi : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some σ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
⊢ σ :: tail✝¹ = head✝ :: tail✝
Tactic:
have ⟨h₁, h₂⟩ := h
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
tail✝¹ : List Γ
hi : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some σ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₁ : some σ = some head✝
h₂ : (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
⊢ σ :: tail✝¹ = head✝ :: tail✝

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
tail✝¹ : List Γ
hi : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some σ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₁ : some σ = some head✝
h₂ : (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
⊢ σ :: tail✝¹ = head✝ :: tail✝
Tactic:
injection h₁ with h₁
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
tail✝¹ : List Γ
hi : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some σ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₂ : (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₁ : σ = head✝
⊢ σ :: tail✝¹ = head✝ :: tail✝

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
tail✝¹ : List Γ
hi : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some σ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₂ : (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₁ : σ = head✝
⊢ σ :: tail✝¹ = head✝ :: tail✝
Tactic:
have : Nonempty (Fin $ (RankedAlphabet.lift Γ).rank $ some σ) := 
  .intro ⟨0, by simp [RankedAlphabet.lift]⟩
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
tail✝¹ : List Γ
hi : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some σ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₂ : (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₁ : σ = head✝
this : Nonempty (Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)))
⊢ σ :: tail✝¹ = head✝ :: tail✝

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
tail✝¹ : List Γ
hi : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some σ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₂ : (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₁ : σ = head✝
this : Nonempty (Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)))
⊢ σ :: tail✝¹ = head✝ :: tail✝
Tactic:
simp [h₁, hi _ (const_func_ext h₂)]
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
tail✝¹ : List Γ
hi : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some σ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₂ : (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
h₁ : σ = head✝
⊢ 0 < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
Tactic:
simp [RankedAlphabet.lift]
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
⊢ Function.Surjective
    { hom := treeₑ,
        property :=
          (_ :
            ∀ (σ : (RankedAlphabet.lift Γ).alphabet)
              (w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) σ),
              treeₑ (Algebra.θ (stringAlgebra Γ) σ w) =
                Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) σ (treeₑ ∘ w)) }.hom
Tactic:
simp [Function.Surjective]
State after:
Γ : Type
inst✝ : Alphabet Γ
⊢ ∀ (b : (Term.algebra (RankedAlphabet.lift Γ) Empty).carrier), ∃ a, treeₑ a = b

State before:
Γ : Type
inst✝ : Alphabet Γ
⊢ ∀ (b : (Term.algebra (RankedAlphabet.lift Γ) Empty).carrier), ∃ a, treeₑ a = b
Tactic:
intro a
State after:
Γ : Type
inst✝ : Alphabet Γ
a : (Term.algebra (RankedAlphabet.lift Γ) Empty).carrier
⊢ ∃ a_1, treeₑ a_1 = a

State before:
Γ : Type
inst✝ : Alphabet Γ
a : (Term.algebra (RankedAlphabet.lift Γ) Empty).carrier
⊢ ∃ a_1, treeₑ a_1 = a
Tactic:
induction a
State after:
case var
Γ : Type
inst✝ : Alphabet Γ
h✝ : Empty
⊢ ∃ a, treeₑ a = var h✝

case app
Γ : Type
inst✝ : Alphabet Γ
σ✝ : (RankedAlphabet.lift Γ).alphabet
v✝ : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) σ✝) → Term (RankedAlphabet.lift Γ) Empty
v_ih✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) σ✝)), ∃ a_1, treeₑ a_1 = v✝ a
⊢ ∃ a, treeₑ a = app σ✝ v✝

State before:
Γ : Type
inst✝ : Alphabet Γ
h✝ : Empty
⊢ ∃ a, treeₑ a = var h✝
Tactic:
case var => contradiction
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : (RankedAlphabet.lift Γ).alphabet
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) σ) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) σ)), ∃ a_1, treeₑ a_1 = w a
⊢ ∃ a, treeₑ a = app σ w
Tactic:
case app σ w hi =>
  cases σ 
  case none => 
    exists .ε
    simp [treeₑ, Term.algebra]
    funext ⟨_, h⟩
    simp [RankedAlphabet.lift] at h
    contradiction
  case some σ => 
    have ⟨a, h⟩ := hi ⟨0, by simp [RankedAlphabet.lift]⟩
    exists σ⬝a
    simp [h, treeₑ]
    refine congrArg _ ?_
    funext ⟨i, hi⟩
    have hi : i = 0 := by 
      simp [RankedAlphabet.lift] at hi
      cases i
      case zero => rfl
      case succ => contradiction
    simp [hi]
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
h✝ : Empty
⊢ ∃ a, treeₑ a = var h✝
Tactic:
contradiction
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : (RankedAlphabet.lift Γ).alphabet
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) σ) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) σ)), ∃ a_1, treeₑ a_1 = w a
⊢ ∃ a, treeₑ a = app σ w
Tactic:
cases σ
State after:
case none
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
⊢ ∃ a, treeₑ a = app none w

case some
Γ : Type
inst✝ : Alphabet Γ
val✝ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some val✝)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some val✝))), ∃ a_1, treeₑ a_1 = w a
⊢ ∃ a, treeₑ a = app (some val✝) w

State before:
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
⊢ ∃ a, treeₑ a = app none w
Tactic:
case none => 
  exists .ε
  simp [treeₑ, Term.algebra]
  funext ⟨_, h⟩
  simp [RankedAlphabet.lift] at h
  contradiction
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
⊢ ∃ a, treeₑ a = app (some σ) w
Tactic:
case some σ => 
  have ⟨a, h⟩ := hi ⟨0, by simp [RankedAlphabet.lift]⟩
  exists σ⬝a
  simp [h, treeₑ]
  refine congrArg _ ?_
  funext ⟨i, hi⟩
  have hi : i = 0 := by 
    simp [RankedAlphabet.lift] at hi
    cases i
    case zero => rfl
    case succ => contradiction
  simp [hi]
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
⊢ ∃ a, treeₑ a = app none w
Tactic:
exists .ε
State after:
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
⊢ treeₑ Word.ε = app none w

State before:
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
⊢ treeₑ Word.ε = app none w
Tactic:
simp [treeₑ, Term.algebra]
State after:
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
⊢ (fun x => nomatch x) = w

State before:
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
⊢ (fun x => nomatch x) = w
Tactic:
funext ⟨_, h⟩
State after:
case h
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
val✝ : Nat
h : val✝ < RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ (nomatch { val := val✝, isLt := h }) = w { val := val✝, isLt := h }

State before:
case h
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
val✝ : Nat
h : val✝ < RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ (nomatch { val := val✝, isLt := h }) = w { val := val✝, isLt := h }
Tactic:
simp [RankedAlphabet.lift] at h
State after:
case h
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
val✝ : Nat
h : val✝ < 0
⊢ (nomatch { val := val✝, isLt := h }) = w { val := val✝, isLt := h }

State before:
case h
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
val✝ : Nat
h : val✝ < 0
⊢ (nomatch { val := val✝, isLt := h }) = w { val := val✝, isLt := h }
Tactic:
contradiction
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
⊢ ∃ a, treeₑ a = app (some σ) w
Tactic:
have ⟨a, h⟩ := hi ⟨0, by simp [RankedAlphabet.lift]⟩
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
⊢ ∃ a, treeₑ a = app (some σ) w

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
⊢ ∃ a, treeₑ a = app (some σ) w
Tactic:
exists σ⬝a
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
⊢ treeₑ (σ⬝a) = app (some σ) w

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
⊢ treeₑ (σ⬝a) = app (some σ) w
Tactic:
simp [h, treeₑ]
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
⊢ (app (some σ) fun x => w { val := 0, isLt := (_ : 0 < 1) }) = app (some σ) w

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
⊢ (app (some σ) fun x => w { val := 0, isLt := (_ : 0 < 1) }) = app (some σ) w
Tactic:
refine congrArg _ ?_
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
⊢ (fun x => w { val := 0, isLt := (_ : 0 < 1) }) = w

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
⊢ (fun x => w { val := 0, isLt := (_ : 0 < 1) }) = w
Tactic:
funext ⟨i, hi⟩
State after:
case h
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
i : Nat
hi : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ w { val := 0, isLt := (_ : 0 < 1) } = w { val := i, isLt := hi }

State before:
case h
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
i : Nat
hi : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ w { val := 0, isLt := (_ : 0 < 1) } = w { val := i, isLt := hi }
Tactic:
have hi : i = 0 := by 
  simp [RankedAlphabet.lift] at hi
  cases i
  case zero => rfl
  case succ => contradiction
State after:
case h
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝¹ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
i : Nat
hi✝ : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
hi : i = 0
⊢ w { val := 0, isLt := (_ : 0 < 1) } = w { val := i, isLt := hi✝ }

State before:
case h
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝¹ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
i : Nat
hi✝ : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
hi : i = 0
⊢ w { val := 0, isLt := (_ : 0 < 1) } = w { val := i, isLt := hi✝ }
Tactic:
simp [hi]
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
⊢ 0 < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
Tactic:
simp [RankedAlphabet.lift]
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
i : Nat
hi : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ i = 0
Tactic:
simp [RankedAlphabet.lift] at hi
State after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
i : Nat
hi : i < 1
⊢ i = 0

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
i : Nat
hi : i < 1
⊢ i = 0
Tactic:
cases i
State after:
case zero
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
hi : Nat.zero < 1
⊢ Nat.zero = 0

case succ
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
n✝ : Nat
hi : Nat.succ n✝ < 1
⊢ Nat.succ n✝ = 0

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
hi : Nat.zero < 1
⊢ Nat.zero = 0
Tactic:
case zero => rfl
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
n✝ : Nat
hi : Nat.succ n✝ < 1
⊢ Nat.succ n✝ = 0
Tactic:
case succ => contradiction
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
hi : Nat.zero < 1
⊢ Nat.zero = 0
Tactic:
rfl
State after:
no goals

State before:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
n✝ : Nat
hi : Nat.succ n✝ < 1
⊢ Nat.succ n✝ = 0
Tactic:
contradiction
State after:
no goals