-- 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₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
branch :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₁_1), q₀ ∈ stmts₁ (Γ := Γ) q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂)
    (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂)), q₀ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂)
branch₁ :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₁_1), q₀ ∈ stmts₁ (Γ := Γ) q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂)
    (h₁₂ : q₁ = Stmt.branch (Γ := Γ) f q₁_1 q₂ ∨ q₁ ∈ stmts₁ (Γ := Γ) q₁_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) q₂),
    q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁_1 q₂) (stmts₁ (Γ := Γ) q₁_1 ∪ stmts₁ (Γ := Γ) q₂)
goto :
  ∀ (l : σ → Λ) (h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) l)) q₁),
    Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) l)) q₀
goto₁ :
  ∀ (l : σ → Λ) (h₁₂ : q₁ = Stmt.goto (Γ := Γ) l), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.goto (Γ := Γ) l} q₀
halt :
  ∀ (h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.halt (Γ := Γ))) q₁),
    Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.halt (Γ := Γ))) q₀
halt₁ : ∀ (h₁₂ : q₁ = Stmt.halt (Γ := Γ)), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.halt (Γ := Γ)} q₀
load :
  ∀ (a : σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
    (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.load (Γ := Γ) a q)), q₀ ∈ stmts₁ (Γ := Γ) (Stmt.load (Γ := Γ) a q)
load₁ :
  ∀ (a : σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
    (h₁₂ : q₁ = Stmt.load (Γ := Γ) a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q),
    q₀ ∈ insert (Stmt.load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)
push :
  ∀ (k : K) (a : σ → Γ k) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
    (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a q)), q₀ ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a q)
push₁ :
  ∀ (k : K) (a : σ → Γ k) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
    (h₁₂ : q₁ = Stmt.push (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q),
    q₀ ∈ insert (Stmt.push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
peek :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
    (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.peek (Γ := Γ) k a q)), q₀ ∈ stmts₁ (Γ := Γ) (Stmt.peek (Γ := Γ) k a q)
peek₁ :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
    (h₁₂ : q₁ = Stmt.peek (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q),
    q₀ ∈ insert (Stmt.peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
pop :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
    (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.pop (Γ := Γ) k a q)), q₀ ∈ stmts₁ (Γ := Γ) (Stmt.pop (Γ := Γ) k a q)
pop₁ :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
    (h₁₂ : q₁ = Stmt.pop (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q),
    q₀ ∈ insert (Stmt.pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ stmts₁ (Γ := Γ) q₂

Tactic:
induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] at h₁₂)
  | branch f q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · exact Finset.mem_insert_of_mem (Finset.mem_union_left _ (IH₁ h₁₂))
    · exact Finset.mem_insert_of_mem (Finset.mem_union_right _ (IH₂ h₁₂))
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | load _ q IH | _ _ _ q IH =>
    rcases h₁₂ with (rfl | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · exact Finset.mem_insert_of_mem (IH h₁₂)

Premises used: Finset.mem_singleton, Turing.TM2.Stmt.branch, Finset.mem_insert, Turing.TM2.Stmt.load, Turing.TM2.Stmt.goto, Finset.mem_union, Turing.TM2.Stmt.halt, Turing.TM2.stmts₁, rfl