awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
⊢ TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
have : TM1.step (tr M) ⟨some (Λ'.act s q'), (), T⟩ = some ⟨some (Λ'.normal q'), (), match s with
        | TM0.Stmt.move d => T.move d
        | TM0.Stmt.write a => T.write a⟩ := by
      cases s <;> rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = some (q', s)
⊢ Reaches₁ (TM1.step (tr M)) { l := some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
    {
      l :=
        match (motive := Bool → Option (Λ' Γ Λ))
          match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
            M q'
              (Tape.head
                (match (motive := TM0.Stmt Γ → Tape Γ) s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T)) with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }

Tactic:
TransGen.head ?_ (TransGen.head' this ?_)

Premises used: Relation.TransGen.head, Relation.TransGen.head', StateTransition.Reaches₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := Option.some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    Option.some
      { l := Option.some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = Option.some (q', s)
some :
  { l := Option.some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } ∈
    TM1.step (tr M) { l := Option.some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
some₁ :
  ReflTransGen (fun (a b : TM1.Cfg Γ (Λ' Γ Λ) Unit) ↦ b ∈ TM1.step (tr M) a)
    { l := Option.some (Λ'.normal q'), var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
    {
      l :=
        match (motive := Bool → Option (Λ' Γ Λ))
          match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
            M q'
              (Tape.head
                (match (motive := TM0.Stmt Γ → Tape Γ) s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T)) with
          | Option.some val => true
          | none => false with
        | true => Option.some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
⊢ Reaches₁ (TM1.step (tr M)) { l := Option.some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
    {
      l :=
        match (motive := Bool → Option (Λ' Γ Λ))
          match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
            M q'
              (Tape.head
                (match (motive := TM0.Stmt Γ → Tape Γ) s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T)) with
          | Option.some val => true
          | none => false with
        | true => Option.some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }

Tactic:
refine TransGen.head ?_ (TransGen.head' this ?_)

Premises used: Relation.TransGen.head, Relation.TransGen.head'
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = some (q', s)
⊢ { l := some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } ∈
    TM1.step (tr M) { l := some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }

Tactic:
grind [TM1.step, TM1.stepAux, tr]

Premises used: Turing.TM1.step, Turing.TM1.stepAux, Turing.TM0to1.tr
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = some (q', s)
⊢ ReflTransGen (fun (a b : TM1.Cfg Γ (Λ' Γ Λ) Unit) ↦ b ∈ TM1.step (tr M) a)
    { l := some (Λ'.normal q'), var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
    {
      l :=
        match (motive := Bool → Option (Λ' Γ Λ))
          match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
            M q'
              (Tape.head
                (match (motive := TM0.Stmt Γ → Tape Γ) s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T)) with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }

Tactic:
grind [TM1.step, TM1.stepAux, tr]

Premises used: Turing.TM1.step, Turing.TM1.stepAux, Turing.TM0to1.tr
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q : Stmt Γ Λ σ
push :
  ∀ (k : K) (a : σ → Γ k) (a_1 : Stmt Γ Λ σ), Stmt.push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a a_1)
peek :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ),
    Stmt.peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.peek (Γ := Γ) k a a_1)
pop :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ),
    Stmt.pop (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.pop (Γ := Γ) k a a_1)
load : ∀ (a : σ → σ) (a_1 : Stmt Γ Λ σ), Stmt.load (Γ := Γ) a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.load (Γ := Γ) a a_1)
branch :
  ∀ (a : σ → Bool) (a_1 a_2 : Stmt Γ Λ σ),
    Stmt.branch (Γ := Γ) a a_1 a_2 ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) a a_1 a_2)
goto :
  ∀ (a : σ → Λ),
    Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) a)) (Stmt.goto (Γ := Γ) a)
halt : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.halt (Γ := Γ))) (Stmt.halt (Γ := Γ))
⊢ q ∈ stmts₁ (Γ := Γ) q

Tactic:
cases q
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
a : σ → Γ k
a_1 : Stmt Γ Λ σ
⊢ push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (push (Γ := Γ) k a a_1)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
⊢ peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (peek (Γ := Γ) k a a_1)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
⊢ pop (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (pop (Γ := Γ) k a a_1)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a : σ → σ
a_1 : Stmt Γ Λ σ
⊢ load (Γ := Γ) a a_1 ∈ stmts₁ (Γ := Γ) (load (Γ := Γ) a a_1)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a : σ → Bool
a_1 a_2 : Stmt Γ Λ σ
⊢ branch (Γ := Γ) a a_1 a_2 ∈ stmts₁ (Γ := Γ) (branch (Γ := Γ) a a_1 a_2)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a : σ → Λ
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (goto (Γ := Γ) a)) (goto (Γ := Γ) a)

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (halt (Γ := Γ))) (halt (Γ := Γ))

Tactic:
simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁_1
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁
IH₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂
h₁₂ : q₁_1 ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
⊢ q₁_1 = branch (Γ := Γ) f q₁ q₂ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₁ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₂

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] 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
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁_1
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁
IH₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂
h₁₂ : q₁_1 = Stmt.branch (Γ := Γ) f q₁ q₂ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₁ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₂
branch :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁ q₂))
    (IH₁ : ∀ (h₁₂ : Stmt.branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁)
    (IH₂ : ∀ (h₁₂ : Stmt.branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂),
    q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
branch₁ :
  ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₁),
    q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
branch₂ :
  ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₂),
    q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
⊢ q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)

Tactic:
rcases h₁₂ with (rfl | h₁₂ | h₁₂)

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (branch (Γ := Γ) f q₁ q₂)
IH₁ : ∀ (h₁₂ : branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁
IH₂ : ∀ (h₁₂ : branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂
⊢ q₀ ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)

Tactic:
unfold stmts₁ at h₀₁

Premises used: Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁
IH₂ : ∀ (h₁₂ : branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂
h₀₁ : q₀ ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
⊢ q₀ ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)

Tactic:
h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁
IH₂ : ∀ (h₁₂ : branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂
h₀₁ : q₀ ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
⊢ q₀ ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁_1
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁
IH₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂
h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₁
⊢ q₀ ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)

Tactic:
Finset.mem_insert_of_mem (Finset.mem_union_left _ (IH₁ h₁₂))

Premises used: Set.Mem, setOf, Finset.mem_insert_of_mem, Finset.mem_union_left
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁_1
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁
IH₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂
h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₁
⊢ q₀ ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)

Tactic:
exact Finset.mem_insert_of_mem (Finset.mem_union_left _ (IH₁ h₁₂))

Premises used: Finset.mem_insert_of_mem, Finset.mem_union_left
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁_1
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁
IH₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂
h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₂
⊢ q₀ ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)

Tactic:
Finset.mem_insert_of_mem (Finset.mem_union_right _ (IH₂ h₁₂))

Premises used: Set.Mem, setOf, Finset.mem_insert_of_mem, Finset.mem_union_right
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁_1
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁
IH₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂
h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₂
⊢ q₀ ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)

Tactic:
exact Finset.mem_insert_of_mem (Finset.mem_union_right _ (IH₂ h₁₂))

Premises used: Finset.mem_insert_of_mem, Finset.mem_union_right
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
l : σ → Λ
h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) {goto (Γ := Γ) l} q₁
⊢ q₁ = goto (Γ := Γ) l

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] 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
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
l : σ → Λ
h₁₂ : q₁ = goto (Γ := Γ) l
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (goto (Γ := Γ) l)) q₀

Tactic:
subst h₁₂
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
l : σ → Λ
h₀₁ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (goto (Γ := Γ) l)) q₀
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {goto (Γ := Γ) l} q₀

Tactic:
h₀₁

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
l : σ → Λ
h₀₁ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (goto (Γ := Γ) l)) q₀
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {goto (Γ := Γ) l} q₀

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) {halt (Γ := Γ)} q₁
⊢ q₁ = halt (Γ := Γ)

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] 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
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
h₁₂ : q₁ = halt (Γ := Γ)
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (halt (Γ := Γ))) q₀

Tactic:
subst h₁₂
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
h₀₁ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (halt (Γ := Γ))) q₀
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {halt (Γ := Γ)} q₀

Tactic:
h₀₁

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
h₀₁ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (halt (Γ := Γ))) q₀
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {halt (Γ := Γ)} q₀

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
a : σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ ∈ insert (load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)
⊢ q₁ = load (Γ := Γ) a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] 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
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
a : σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ = Stmt.load (Γ := Γ) a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q
load :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (Stmt.load (Γ := Γ) a q))
    (IH : ∀ (h₁₂ : Stmt.load (Γ := Γ) a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q),
    q₀ ∈ insert (Stmt.load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)
load₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ insert (Stmt.load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (Stmt.load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)

Tactic:
rcases h₁₂ with (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
q₀ : Stmt Γ Λ σ
a : σ → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (load (Γ := Γ) a q)
IH : ∀ (h₁₂ : load (Γ := Γ) a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)

Tactic:
unfold stmts₁ at h₀₁

Premises used: Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
a : σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : load (Γ := Γ) a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₀₁ : q₀ ∈ insert (load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)

Tactic:
h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
a : σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : load (Γ := Γ) a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₀₁ : q₀ ∈ insert (load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
a : σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)

Tactic:
Finset.mem_insert_of_mem (IH h₁₂)

Premises used: Set.Mem, setOf, Finset.mem_insert_of_mem
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
a : σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)

Tactic:
exact Finset.mem_insert_of_mem (IH h₁₂)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
k : K
a : σ → Γ k
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₁ = push (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q

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

Premises used: Finset.mem_singleton, Finset.mem_insert, Finset.mem_union