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
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:
exact ⟨fun _ _ ↦ hret, fun _ _ ↦ 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
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 : σ → 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))

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

Premises used: And.intro, 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
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 : σ → 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))

Tactic:
exact ⟨fun _ _ ↦ hret, fun _ _ ↦ 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
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 : σ → 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))

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

Premises used: And.intro, 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
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 : σ → 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))

Tactic:
exact ⟨⟨fun _ _ ↦ hret, fun _ _ ↦ hret⟩, fun _ _ ↦ 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')
⊢ match (motive := TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ → Prop)
    match (motive := Λ' K Γ Λ σ → TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ) ret (Γ := Γ) q with
    | normal q => trNormal (Γ := Γ) (M q)
    | go k s q =>
      branch (fun (a : Γ' K Γ) (x : σ) ↦ (a.2 k).isNone)
        (trStAct (Γ := Γ) (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) s)
        (move Dir.right (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k s q))
    | ret q =>
      branch (fun (a : Γ' K Γ) (x : σ) ↦ a.1) (trNormal (Γ := Γ) q)
        (move Dir.left (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q)) with
  | move a q => TM1.SupportsStmt (trSupp (Γ := Γ) M S) q
  | write a q => TM1.SupportsStmt (trSupp (Γ := Γ) M S) q
  | load a q => TM1.SupportsStmt (trSupp (Γ := Γ) M S) q
  | branch a q₁ q₂ => TM1.SupportsStmt (trSupp (Γ := Γ) M S) q₁ ∧ TM1.SupportsStmt (trSupp (Γ := Γ) M S) q₂
  | goto l => ∀ (a : Γ' K Γ) (v : σ), l a v ∈ trSupp (Γ := Γ) M S
  | halt => True

Tactic:
⟨IH₁, fun _ _ ↦ hret⟩

Premises used: And.intro
-- 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')
⊢ match (motive := TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ → Prop)
    match (motive := Λ' K Γ Λ σ → TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ) ret (Γ := Γ) q with
    | normal q => trNormal (Γ := Γ) (M q)
    | go k s q =>
      branch (fun (a : Γ' K Γ) (x : σ) ↦ (a.2 k).isNone)
        (trStAct (Γ := Γ) (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) s)
        (move Dir.right (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k s q))
    | ret q =>
      branch (fun (a : Γ' K Γ) (x : σ) ↦ a.1) (trNormal (Γ := Γ) q)
        (move Dir.left (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q)) with
  | move a q => TM1.SupportsStmt (trSupp (Γ := Γ) M S) q
  | write a q => TM1.SupportsStmt (trSupp (Γ := Γ) M S) q
  | load a q => TM1.SupportsStmt (trSupp (Γ := Γ) M S) q
  | branch a q₁ q₂ => TM1.SupportsStmt (trSupp (Γ := Γ) M S) q₁ ∧ TM1.SupportsStmt (trSupp (Γ := Γ) M S) q₂
  | goto l => ∀ (a : Γ' K Γ) (v : σ), l a v ∈ trSupp (Γ := Γ) M S
  | halt => True

Tactic:
exact ⟨IH₁, fun _ _ ↦ hret⟩
-- 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₁ (Γ := Γ) q
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)

Tactic:
IH₂ _ 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₁ (Γ := Γ) q
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)

Tactic:
exact IH₂ _ 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
a : σ → σ
refine_2 :
  ∀ (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 (TM2.Stmt.load (Γ := Γ) a q) →
        (∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q), x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a 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 (TM2.Stmt.load (Γ := Γ) a q) →
        (∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q), x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a 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
a : σ → σ
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 (TM2.Stmt.load (Γ := Γ) a q)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q), x ∈ trSupp (Γ := Γ) M S
refine_2 :
  ∀ (sub : ∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) ∧
      ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
unfold TM2to1.trStmts₁ at sub ⊢

Premises used: Turing.TM2to1.trStmts₁
-- 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
a : σ → σ
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 (TM2.Stmt.load (Γ := Γ) a q)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
IH ss' sub

Premises used: Turing.TM2to1.trNormal, 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
a : σ → σ
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 (TM2.Stmt.load (Γ := Γ) a q)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
exact IH ss' sub
-- 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
p : σ → Bool
refine_3 :
  ∀ (q₁ 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 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 (TM2.Stmt.branch (Γ := Γ) p q₁ q₂) →
          (∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂), x ∈ trSupp (Γ := Γ) M S) →
            TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)) ∧
              ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂),
                TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ ∀ (q₁ 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 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 (TM2.Stmt.branch (Γ := Γ) p q₁ q₂) →
          (∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂), x ∈ trSupp (Γ := Γ) M S) →
            TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)) ∧
              ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ 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
p : σ → Bool
q₁ : TM2.Stmt Γ Λ σ
refine_3 :
  ∀ (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 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 (TM2.Stmt.branch (Γ := Γ) p q₁ q₂) →
          (∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂), x ∈ trSupp (Γ := Γ) M S) →
            TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)) ∧
              ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ 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 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 (TM2.Stmt.branch (Γ := Γ) p q₁ q₂) →
          (∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂), x ∈ trSupp (Γ := Γ) M S) →
            TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)) ∧
              ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ 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
p : σ → Bool
q₁ 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')
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 (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂), x ∈ trSupp (Γ := Γ) M S
⊢ ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S

Tactic:
unfold TM2to1.trStmts₁ at sub

Premises used: Turing.TM2to1.trStmts₁
-- 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
p : σ → Bool
q₁ 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')
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 (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)

Tactic:
obtain ⟨IH₁₁, IH₁₂⟩ := IH₁ ss'.1 fun x hx ↦ sub x <| Finset.mem_union_left _ hx

Premises used: And.left, Finset.mem_union_left, Turing.TM2to1.trStmts₁