awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
l' : Λ' K Γ Λ σ
h_1 : l' ∈ trSupp (Γ := Γ) M S
this_1 :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt (Γ := Γ) S q →
      (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ
lS : l ∈ S
h_2 : l' ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))
this :
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (M l)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (M l), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
h : l' ∈ trStmts₁ (Γ := Γ) (M l)
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
exact this.2 _ h

Premises used: And.right
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
l' : Λ' K Γ Λ σ
h_1 : l' ∈ trSupp (Γ := Γ) M S
this_1 :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt (Γ := Γ) S q →
      (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ
lS : l ∈ S
h : l' ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))
this :
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (M l)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (M l), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
inl :
  ∀ (h : normal (Γ := Γ) l ∈ trSupp (Γ := Γ) M S)
    (h : normal (Γ := Γ) l ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (normal (Γ := Γ) l))
inr : ∀ (h : l' ∈ trStmts₁ (Γ := Γ) (M l)), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
inl₁ :
  ∀ (h : normal (Γ := Γ) l ∈ trSupp (Γ := Γ) M S)
    (h : normal (Γ := Γ) l ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (normal (Γ := Γ) l))
inr₁ : ∀ (h : l' ∈ trStmts₁ (Γ := Γ) (M l)), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ h]

Premises used: Finset.mem_insert, And.right, And.left, Iff.mp, rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
l' : Λ' K Γ Λ σ
h : l' ∈ trSupp (Γ := Γ) M S
suffices :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt (Γ := Γ) S q →
      (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
suffices ∀ (q) (_ : TM2.SupportsStmt S q) (_ : ∀ x ∈ trStmts₁ q, x ∈ trSupp M S),
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
        ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l') by
      rcases Finset.mem_biUnion.1 h with ⟨l, lS, h⟩
      have :=
        this _ (ss.2 l lS) fun x hx ↦ Finset.mem_biUnion.2 ⟨_, lS, Finset.mem_insert_of_mem hx⟩
      rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ h]
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
⊢ ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt (Γ := Γ) S q →
      (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
stmtStRec ?_ ?_ ?_ ?_ ?_

Premises used: Turing.TM2to1.stmtStRec
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
refine_1 :
  ∀ (q : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt (Γ := Γ) S q →
        (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')) →
      TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q) →
        (∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ ∀ (q : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt (Γ := Γ) S q →
        (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')) →
      TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q) →
        (∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S
⊢ TM2.SupportsStmt (Γ := Γ) S q

Tactic:
rw [TM2to1.supports_run] at ss'

Premises used: Turing.TM2to1.supports_run
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S
ss'₁ : TM2.SupportsStmt (Γ := Γ) S q
⊢ ∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S

Tactic:
rw [TM2to1.supports_run] at ss'

Premises used: Turing.TM2to1.supports_run
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub : ∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S
⊢ ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S

Tactic:
simp only [TM2to1.trStmts₁_run, Finset.mem_union, Finset.mem_insert, Finset.mem_singleton]
        at sub

Premises used: Finset.mem_singleton, Turing.TM2to1.trStmts₁_run, Finset.mem_insert, Finset.mem_union
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
⊢ go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S

Tactic:
have hgo := sub _ (Or.inl <| Or.inl rfl)
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
⊢ ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S

Tactic:
have hret := sub _ (Or.inl <| Or.inr rfl)
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)

Tactic:
obtain ⟨IH₁, IH₂⟩ := IH ss' fun x hx ↦ sub x <| Or.inr hx

Premises used: Or.inr
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
⊢ ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
obtain ⟨IH₁, IH₂⟩ := IH ss' fun x hx ↦ sub x <| Or.inr hx

Premises used: Or.inr
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
simp : ∀ (a : Γ' K Γ) (v : σ), go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q))

Tactic:
simp only [trNormal_run, TM1.SupportsStmt]

Premises used: Turing.TM2to1.trNormal_run, Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
a : Γ' K Γ
v : σ
⊢ go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S

Tactic:
hgo

Premises used: Set.Mem
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
a : Γ' K Γ
v : σ
⊢ go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S

Tactic:
exact hgo
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
refine_1 :
  ∀ (l : Λ' K Γ Λ σ) (h : l ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q)),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
refine ⟨by simp only [trNormal_run, TM1.SupportsStmt]; intros; exact hgo, fun l h ↦ ?_⟩
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q)
⊢ l ∈ {go (Γ := Γ) k s q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q

Tactic:
rw [trStmts₁_run] at h

Premises used: Turing.TM2to1.trStmts₁_run
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : l ∈ {go (Γ := Γ) k s q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
⊢ (l = go (Γ := Γ) k s q ∨ l = ret (Γ := Γ) q) ∨ l ∈ trStmts₁ (Γ := Γ) q

Tactic:
simp only [Finset.mem_union, Finset.mem_insert, Finset.mem_singleton]
        at h

Premises used: Finset.mem_singleton, Finset.mem_insert, Finset.mem_union
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : (l = go (Γ := Γ) k s q ∨ l = ret (Γ := Γ) q) ∨ l ∈ trStmts₁ (Γ := Γ) q
refine_1 : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k s q))
refine_1₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (ret (Γ := Γ) q))
refine_1₂ : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)

Tactic:
rcases h with (⟨rfl | rfl⟩ | h)

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
refine_1 :
  ∀ (a : σ → Γ k)
    (sub :
      ∀ (x : Λ' K Γ Λ σ),
        (x = go (Γ := Γ) k (StAct.push (Γ := Γ) a) q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q →
          x ∈ trSupp (Γ := Γ) M S)
    (hgo : go (Γ := Γ) k (StAct.push (Γ := Γ) a) q ∈ trSupp (Γ := Γ) M S),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k (StAct.push (Γ := Γ) a) q))
refine_1₁ :
  ∀ (a : σ → Option (Γ k) → σ)
    (sub :
      ∀ (x : Λ' K Γ Λ σ),
        (x = go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q →
          x ∈ trSupp (Γ := Γ) M S)
    (hgo : go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q ∈ trSupp (Γ := Γ) M S),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q))
refine_1₂ :
  ∀ (a : σ → Option (Γ k) → σ)
    (sub :
      ∀ (x : Λ' K Γ Λ σ),
        (x = go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q →
          x ∈ trSupp (Γ := Γ) M S)
    (hgo : go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q ∈ trSupp (Γ := Γ) M S),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q))
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k s q))

Tactic:
cases s
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
q : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt (Γ := Γ) S q →
    (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S q
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
a : σ → Γ k
sub :
  ∀ (x : Λ' K Γ Λ σ),
    (x = go (Γ := Γ) k (StAct.push (Γ := Γ) a) q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q →
      x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k (StAct.push (Γ := Γ) a) q ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k (StAct.push (Γ := Γ) a) q))

Tactic:
⟨fun _ _ ↦ hret, fun _ _ ↦ hgo⟩

Premises used: And.intro, Turing.TM1.SupportsStmt