internlm/Lean-Github huggingface dataset:
Theorem: Term.algebra_iso_stringAlgebra
Proof state before:
Γ : Type
inst✝ : Alphabet Γ
a : (Term.algebra (RankedAlphabet.lift Γ) Empty).carrier
⊢ ∃ a_1, treeₑ a_1 = a
Tactic:
induction a
Proof 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✝
Theorem: Term.algebra_iso_stringAlgebra
Proof state before:
Γ : Type
inst✝ : Alphabet Γ
h✝ : Empty
⊢ ∃ a, treeₑ a = var h✝
Tactic:
case var => contradiction
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof state before:
Γ : Type
inst✝ : Alphabet Γ
h✝ : Empty
⊢ ∃ a, treeₑ a = var h✝
Tactic:
contradiction
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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 σ
Proof 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
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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 .ε
Proof 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
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof 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
Theorem: Term.algebra_iso_stringAlgebra
Proof 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⟩
Proof 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 }
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof 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 }
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]⟩
Proof 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
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof 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
Theorem: Term.algebra_iso_stringAlgebra
Proof 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ₑ]
Proof 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
Theorem: Term.algebra_iso_stringAlgebra
Proof 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 _ ?_
Proof 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
Theorem: Term.algebra_iso_stringAlgebra
Proof 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⟩
Proof 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 }
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof 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✝ }
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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]
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof 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
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof 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
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_iso_stringAlgebra
Proof 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
Proof state after:
no goals
Theorem: TreeDomain.ε_mem
Proof state before:
W : Set (Nat⋆)
⊢ TreeDomain W → Word.ε ∈ W
Tactic:
intro h
Proof state after:
W : Set (Nat⋆)
h : TreeDomain W
⊢ Word.ε ∈ W
Theorem: TreeDomain.ε_mem
Proof state before:
W : Set (Nat⋆)
h : TreeDomain W
⊢ Word.ε ∈ W
Tactic:
apply h.prefixClosed .ε
Proof state after:
W : Set (Nat⋆)
h : TreeDomain W
⊢ Word.ε ∈ Set.bUnion (Set.image Word.prefixes)
Theorem: TreeDomain.ε_mem
Proof state before:
W : Set (Nat⋆)
h : TreeDomain W
⊢ Word.ε ∈ Set.bUnion (Set.image Word.prefixes)
Tactic:
simp [Set.bUnion, Membership.mem]
Proof state after:
W : Set (Nat⋆)
h : TreeDomain W
⊢ ∃ m, Set.image Word.prefixes m ∧ m Word.ε
Theorem: TreeDomain.ε_mem
Proof 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
Proof state after:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ ∃ m, Set.image Word.prefixes m ∧ m Word.ε
Theorem: TreeDomain.ε_mem
Proof 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
Proof state after:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Set.image Word.prefixes (Word.prefixes m) ∧ Word.prefixes m Word.ε
Theorem: TreeDomain.ε_mem
Proof 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
Proof 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.ε
Theorem: TreeDomain.ε_mem
Proof 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
Proof state after:
no goals
Theorem: TreeDomain.ε_mem
Proof state before:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Word.prefixes m Word.ε
Tactic:
case right => apply Word.ε_mem_prefixes
Proof state after:
no goals
Theorem: TreeDomain.ε_mem
Proof state before:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Set.image Word.prefixes (Word.prefixes m)
Tactic:
exists m
Proof state after:
no goals
Theorem: TreeDomain.ε_mem
Proof state before:
W : Set (Nat⋆)
h : TreeDomain W
m : Nat⋆
h✝ : m ∈ W
⊢ Word.prefixes m Word.ε
Tactic:
apply Word.ε_mem_prefixes
Proof state after:
no goals
Theorem: id_le_extraction'
Proof state before:
case zero
φ : ℕ → ℕ
hyp : extraction φ
⊢ 0 ≤ φ 0
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: id_le_extraction'
Proof state before:
case succ
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
ih : n ≤ φ n
⊢ n + 1 ≤ φ (n + 1)
Tactic:
exact Nat.succ_le_of_lt (by linarith [hyp n (n+1) (by linarith)])
Proof state after:
no goals
Theorem: id_le_extraction'
Proof state before:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
ih : n ≤ φ n
⊢ n < φ (n + 1)
Tactic:
linarith [hyp n (n+1) (by linarith)]
Proof state after:
no goals
Theorem: extraction_ge
Proof state before:
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ ∃ n ≥ N', φ n ≥ N
Tactic:
use max N N'
Proof state after:
case h
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N' ∧ φ (max N N') ≥ N
Theorem: extraction_ge
Proof state before:
case h
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N' ∧ φ (max N N') ≥ N
Tactic:
constructor
Proof state after:
case h.left
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N'

case h.right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N
Theorem: extraction_ge
Proof state before:
case h.left
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N'

case h.right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N
Tactic:
apply le_max_right
Proof state after:
case h.right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N
Theorem: extraction_ge
Proof state before:
case h.right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N
Tactic:
calc
  N ≤ max N N' := by apply le_max_left
  _ ≤ φ (max N N') := by apply id_le_extraction' h
Proof state after:
no goals
Theorem: subseq_tendsto_of_tendsto'
Proof state before:
case intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Tactic:
use N
Proof state after:
case h
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Theorem: subseq_tendsto_of_tendsto'
Proof state before:
case h
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Tactic:
intro n hn
Proof state after:
case h
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - l| ≤ ε
Theorem: subseq_tendsto_of_tendsto'
Proof state before:
case h
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - l| ≤ ε
Tactic:
apply hN
Proof state after:
case h.a
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ φ n ≥ N
Theorem: subseq_tendsto_of_tendsto'
Proof state before:
case h.a
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ φ n ≥ N
Tactic:
calc
  N ≤ n := hn
  _ ≤ φ n := id_le_extraction' hφ n
Proof state after:
no goals