-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ (Γ := Γ) q₂
hs : SupportsStmt (Γ := Γ) S q₂
branch :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂))
    (hs : SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁_1 q₂)), SupportsStmt (Γ := Γ) S q₁
branch₁ :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S q₁_1 ∧ SupportsStmt (Γ := Γ) S q₂)
    (h : q₁ = Stmt.branch (Γ := Γ) f q₁_1 q₂ ∨ q₁ ∈ stmts₁ (Γ := Γ) q₁_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) q₂),
    SupportsStmt (Γ := Γ) S q₁
goto :
  ∀ (l : σ → Λ) (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) l)) q₁)
    (hs : SupportsStmt (Γ := Γ) S (Stmt.goto (Γ := Γ) l)), SupportsStmt (Γ := Γ) S q₁
goto₁ : ∀ (l : σ → Λ) (hs : ∀ (v : σ), l v ∈ S) (h : q₁ = Stmt.goto (Γ := Γ) l), SupportsStmt (Γ := Γ) S q₁
halt :
  ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.halt (Γ := Γ))) q₁)
    (hs : SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (Stmt.halt (Γ := Γ))), SupportsStmt (Γ := Γ) S q₁
halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt (Γ := Γ)), SupportsStmt (Γ := Γ) S q₁
load :
  ∀ (a : σ → σ) (a_1 : Stmt Γ Λ σ)
    (IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.load (Γ := Γ) a a_1)) (hs : SupportsStmt (Γ := Γ) S (Stmt.load (Γ := Γ) a a_1)),
    SupportsStmt (Γ := Γ) S q₁
load₁ :
  ∀ (a : σ → σ) (a_1 : Stmt Γ Λ σ)
    (IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S a_1) (h : q₁ = Stmt.load (Γ := Γ) a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1),
    SupportsStmt (Γ := Γ) S q₁
push :
  ∀ (k : K) (a : σ → Γ k) (a_1 : Stmt Γ Λ σ)
    (IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a a_1)) (hs : SupportsStmt (Γ := Γ) S (Stmt.push (Γ := Γ) k a a_1)),
    SupportsStmt (Γ := Γ) S q₁
push₁ :
  ∀ (k : K) (a : σ → Γ k) (a_1 : Stmt Γ Λ σ)
    (IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S a_1) (h : q₁ = Stmt.push (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1),
    SupportsStmt (Γ := Γ) S q₁
peek :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ)
    (IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.peek (Γ := Γ) k a a_1)) (hs : SupportsStmt (Γ := Γ) S (Stmt.peek (Γ := Γ) k a a_1)),
    SupportsStmt (Γ := Γ) S q₁
peek₁ :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ)
    (IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S a_1) (h : q₁ = Stmt.peek (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1),
    SupportsStmt (Γ := Γ) S q₁
pop :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ)
    (IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.pop (Γ := Γ) k a a_1)) (hs : SupportsStmt (Γ := Γ) S (Stmt.pop (Γ := Γ) k a a_1)),
    SupportsStmt (Γ := Γ) S q₁
pop₁ :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ)
    (IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S a_1) (h : q₁ = Stmt.pop (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1),
    SupportsStmt (Γ := Γ) S q₁
⊢ SupportsStmt (Γ := Γ) S q₁

Tactic:
induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

Premises used: Finset.mem_singleton, Turing.TM2.SupportsStmt, 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