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
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
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'.1 fun x hx ↦ sub x <| Finset.mem_union_left _ hx

Premises used: And.left, Finset.mem_union_left, 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
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)

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

Premises used: And.right, Finset.mem_union_right, 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
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
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'.2 fun x hx ↦ sub x <| Finset.mem_union_right _ hx

Premises used: And.right, Finset.mem_union_right, 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
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ 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:
⟨⟨IH₁₁, IH₂₁⟩, fun l h ↦ ?_⟩

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
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
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
refine_3 :
  ∀ (l : Λ' K Γ Λ σ) (h : l ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
⊢ 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:
refine ⟨⟨IH₁₁, IH₂₁⟩, 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
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
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
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₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
⊢ l ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂

Tactic:
rw [trStmts₁] at h

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
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
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₁ ∪ trStmts₁ (Γ := Γ) q₂
refine_3 : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₁), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
refine_3₁ : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₂), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)

Tactic:
rcases Finset.mem_union.1 h with (h | h)

Premises used: Iff.mp, 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
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
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h_1 : l ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂
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
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
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h_1 : l ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂
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
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
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h_1 : l ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂
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
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
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h_1 : l ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂
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
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
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
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₁ ∪ trStmts₁ (Γ := Γ) q₂
refine_3 : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₁), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
refine_3₁ : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₂), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
refine_3₂ : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₁), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
refine_3₃ : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₂), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)

Tactic:
rcases Finset.mem_union.1 h with (h | h) <;> [exact IH₁₂ _ h; exact IH₂₂ _ h]

Premises used: Iff.mp, 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
l : σ → Λ
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.goto (Γ := Γ) l)
refine_4 :
  (∀ (x : Λ' K Γ Λ σ),
      Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) x →
        x ∈ trSupp (Γ := Γ) M S) →
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) ∧
      ∀ (l' : Λ' K Γ Λ σ),
        Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) l' →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ (∀ (x : Λ' K Γ Λ σ),
      Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) x →
        x ∈ trSupp (Γ := Γ) M S) →
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) ∧
      ∀ (l' : Λ' K Γ Λ σ),
        Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) l' →
          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
l : σ → Λ
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.goto (Γ := Γ) l)
h :
  ∀ (x : Λ' K Γ Λ σ),
    Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) x → x ∈ trSupp (Γ := Γ) M S
refine_4 :
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) ∧
    ∀ (l' : Λ' K Γ Λ σ),
      Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) l' →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
simp only [trStmts₁, Finset.notMem_empty]

Premises used: Finset.notMem_empty, 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
l : σ → Λ
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.goto (Γ := Γ) l)
h :
  ∀ (x : Λ' K Γ Λ σ),
    Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) x → x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
⟨?_, fun _ ↦ False.elim⟩

Premises used: False.elim, 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
l : σ → Λ
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.goto (Γ := Γ) l)
h :
  ∀ (x : Λ' K Γ Λ σ),
    Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) x → x ∈ trSupp (Γ := Γ) M S
refine_4 : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l))
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
refine ⟨?_, fun _ ↦ False.elim⟩
-- 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 : σ → Λ
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.goto (Γ := Γ) l)
h :
  ∀ (x : Λ' K Γ Λ σ),
    Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) x → x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l))

Tactic:
fun _ v ↦ Finset.mem_biUnion.2 ⟨_, ss' v, Finset.mem_insert_self _ _⟩

Premises used: Iff.mpr, Finset.mem_insert_self, Set.Mem, setOf, And.intro, Exists.intro, Turing.TM1.SupportsStmt, Turing.TM2to1.trStmts₁, Finset.mem_biUnion, Turing.TM2to1.Λ'.normal
-- 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 : σ → Λ
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.goto (Γ := Γ) l)
h :
  ∀ (x : Λ' K Γ Λ σ),
    Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) x → x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l))

Tactic:
exact fun _ v ↦ Finset.mem_biUnion.2 ⟨_, ss' v, Finset.mem_insert_self _ _⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.mem_biUnion