internlm/Lean-Github huggingface dataset:
Theorem: Term.pos_zero
Proof 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'
Proof 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 })
Theorem: Term.pos_zero
Proof 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 *
Proof 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
Theorem: Term.pos_zero
Proof 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']
Proof state after:
no goals
Theorem: Term.pos_zero
Proof 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'
Proof 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.ε
Theorem: Term.mem_pos
Proof 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
Proof 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 })
Theorem: Term.mem_pos
Proof 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
Proof 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 })
Theorem: Term.mem_pos
Proof 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
Proof 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 })
Theorem: Term.mem_pos
Proof 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
Proof state after:
no goals
Theorem: Term.ε_mem_pos
Proof state before:
Δ : RankedAlphabet
H : Type
ξ : (Term.algebra Δ H).carrier
⊢ Word.ε ∈ Hom.hom pos ξ
Tactic:
sorry
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof state before:
Γ : Type
inst✝ : Alphabet Γ
⊢ stringAlgebra Γ ≅ Term.algebra (RankedAlphabet.lift Γ) Empty
Tactic:
unfold Isomorphic
Proof state after:
Γ : Type
inst✝ : Alphabet Γ
⊢ Nonempty (Iso (stringAlgebra Γ) (Term.algebra (RankedAlphabet.lift Γ) Empty))
Theorem: Term.algebra_iso_stringAlgebra
Proof state before:
Γ : Type
inst✝ : Alphabet Γ
⊢ Nonempty (Iso (stringAlgebra Γ) (Term.algebra (RankedAlphabet.lift Γ) Empty))
Tactic:
apply Nonempty.intro
Proof state after:
case val
Γ : Type
inst✝ : Alphabet Γ
⊢ Iso (stringAlgebra Γ) (Term.algebra (RankedAlphabet.lift Γ) Empty)
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
  }
}
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof 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)
Theorem: Term.algebra_iso_stringAlgebra
Proof 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 σ
Proof 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)
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof 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)
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof 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)
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof state after:
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ (fun x => nomatch x) = fun x => treeₑ (w x)
Theorem: Term.algebra_iso_stringAlgebra
Proof 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⟩
Proof 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 })
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof 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 })
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
⊢ treeₑ (σ⬝w { val := 0, isLt := stringAlgebra.proof_1 }) = app (some σ) (treeₑ ∘ w)
Theorem: Term.algebra_iso_stringAlgebra
Proof 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'
Proof state after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
⊢ treeₑ (σ⬝w') = app (some σ) (treeₑ ∘ w)
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof 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)
Theorem: Term.algebra_iso_stringAlgebra
Proof 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⟩
Proof 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 })
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof 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✝ })
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi : i < 1
⊢ i = 0
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof 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
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof state after:
Γ : Type
inst✝ : Alphabet Γ
⊢ ∀ (a₁ a₂ : (stringAlgebra Γ).carrier), treeₑ a₁ = treeₑ a₂ → a₁ = a₂
Theorem: Term.algebra_iso_stringAlgebra
Proof state before:
Γ : Type
inst✝ : Alphabet Γ
⊢ ∀ (a₁ a₂ : (stringAlgebra Γ).carrier), treeₑ a₁ = treeₑ a₂ → a₁ = a₂
Tactic:
intro σ₁ σ₂ h
Proof state after:
Γ : Type
inst✝ : Alphabet Γ
σ₁ σ₂ : (stringAlgebra Γ).carrier
h : treeₑ σ₁ = treeₑ σ₂
⊢ σ₁ = σ₂
Theorem: Term.algebra_iso_stringAlgebra
Proof state before:
Γ : Type
inst✝ : Alphabet Γ
σ₁ σ₂ : (stringAlgebra Γ).carrier
h : treeₑ σ₁ = treeₑ σ₂
⊢ σ₁ = σ₂
Tactic:
induction σ₁ generalizing σ₂ <;> cases σ₂ <;> simp [treeₑ, Term.algebra] at *
Proof 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✝
Theorem: Term.algebra_iso_stringAlgebra
Proof 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₂)]
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof 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✝
Theorem: Term.algebra_iso_stringAlgebra
Proof 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₁
Proof 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✝
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]⟩
Proof 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✝
Theorem: Term.algebra_iso_stringAlgebra
Proof 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₂)]
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof state after:
Γ : Type
inst✝ : Alphabet Γ
⊢ ∀ (b : (Term.algebra (RankedAlphabet.lift Γ) Empty).carrier), ∃ a, treeₑ a = b
Theorem: Term.algebra_iso_stringAlgebra
Proof state before:
Γ : Type
inst✝ : Alphabet Γ
⊢ ∀ (b : (Term.algebra (RankedAlphabet.lift Γ) Empty).carrier), ∃ a, treeₑ a = b
Tactic:
intro a
Proof state after:
Γ : Type
inst✝ : Alphabet Γ
a : (Term.algebra (RankedAlphabet.lift Γ) Empty).carrier
⊢ ∃ a_1, treeₑ a_1 = a