-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
q : Stmt Γ Λ σ
hs : SupportsStmt S q
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
move :
  ∀ (d : Dir) (q : Stmt Γ Λ σ)
    (IH :
      ∀ (hs : SupportsStmt S q) (hw : ∀ q' ∈ writes q, q' ∈ trSupp M S),
        SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q'))
    (hs : SupportsStmt S (Stmt.move d q)) (hw : ∀ q' ∈ writes (Stmt.move d q), q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
      ∀ q' ∈ writes (Stmt.move d q), SupportsStmt (trSupp M S) (tr enc dec M q')
write :
  ∀ (f : Γ → σ → Γ) (q : Stmt Γ Λ σ)
    (IH :
      ∀ (hs : SupportsStmt S q) (hw : ∀ q' ∈ writes q, q' ∈ trSupp M S),
        SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q'))
    (hs : SupportsStmt S (Stmt.write f q)) (hw : ∀ q' ∈ writes (Stmt.write f q), q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec (Stmt.write f q)) ∧
      ∀ q' ∈ writes (Stmt.write f q), SupportsStmt (trSupp M S) (tr enc dec M q')
load :
  ∀ (a : Γ → σ → σ) (q : Stmt Γ Λ σ)
    (IH :
      ∀ (hs : SupportsStmt S q) (hw : ∀ q' ∈ writes q, q' ∈ trSupp M S),
        SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q'))
    (hs : SupportsStmt S (Stmt.load a q)) (hw : ∀ q' ∈ writes (Stmt.load a q), q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec (Stmt.load a q)) ∧
      ∀ q' ∈ writes (Stmt.load a q), SupportsStmt (trSupp M S) (tr enc dec M q')
branch :
  ∀ (p : Γ → σ → Bool) (q₁ q₂ : Stmt Γ Λ σ)
    (IH₁ :
      ∀ (hs : SupportsStmt S q₁) (hw : ∀ q' ∈ writes q₁, q' ∈ trSupp M S),
        SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q'))
    (IH₂ :
      ∀ (hs : SupportsStmt S q₂) (hw : ∀ q' ∈ writes q₂, q' ∈ trSupp M S),
        SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q'))
    (hs : SupportsStmt S (Stmt.branch p q₁ q₂)) (hw : ∀ q' ∈ writes (Stmt.branch p q₁ q₂), q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
      ∀ q' ∈ writes (Stmt.branch p q₁ q₂), SupportsStmt (trSupp M S) (tr enc dec M q')
goto :
  ∀ (l : Γ → σ → Λ) (hs : SupportsStmt S (Stmt.goto l)) (hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l)) ∧
      ∀ q' ∈ writes (Stmt.goto l), SupportsStmt (trSupp M S) (tr enc dec M q')
halt :
  ∀ (hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt)
    (hw : ∀ (q' : Λ' Γ Λ σ), Membership.mem (γ := Finset (Λ' Γ Λ σ)) (writes Stmt.halt) q' → q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec Stmt.halt) ∧
      ∀ (q' : Λ' Γ Λ σ),
        Membership.mem (γ := Finset (Λ' Γ Λ σ)) (writes Stmt.halt) q' → SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
induction q with
    | move d q IH =>
      unfold writes at hw ⊢
      replace IH := IH hs hw; refine ⟨?_, IH.2⟩
      cases d <;> simp only [trNormal, supportsStmt_move, IH]
    | write f q IH =>
      unfold writes at hw ⊢
      simp only [Finset.mem_image, Finset.mem_union, Finset.mem_univ, true_and]
        at hw ⊢
      replace IH := IH hs fun q hq ↦ hw q (Or.inr hq)
      refine ⟨supportsStmt_read _ fun a _ s ↦ hw _ (Or.inl ⟨_, rfl⟩), fun q' hq ↦ ?_⟩
      rcases hq with (⟨a, q₂, rfl⟩ | hq)
      · simp only [tr, supportsStmt_write, supportsStmt_move, IH.1]
      · exact IH.2 _ hq
    | load a q IH =>
      unfold writes at hw ⊢
      replace IH := IH hs hw
      exact ⟨supportsStmt_read _ fun _ ↦ IH.1, IH.2⟩
    | branch p q₁ q₂ IH₁ IH₂ =>
      unfold writes at hw ⊢
      simp only [Finset.mem_union] at hw ⊢
      replace IH₁ := IH₁ hs.1 fun q hq ↦ hw q (Or.inl hq)
      replace IH₂ := IH₂ hs.2 fun q hq ↦ hw q (Or.inr hq)
      exact ⟨supportsStmt_read _ fun _ ↦ ⟨IH₁.1, IH₂.1⟩, fun q ↦ Or.rec (IH₁.2 _) (IH₂.2 _)⟩
    | goto l =>
      simp only [writes, Finset.notMem_empty]; refine ⟨?_, fun _ ↦ False.elim⟩
      refine supportsStmt_read _ fun a _ s ↦ ?_
      exact Finset.mem_biUnion.2 ⟨_, hs _ _, Finset.mem_insert_self _ _⟩
    | halt =>
      simp only [writes, Finset.notMem_empty]; refine ⟨?_, fun _ ↦ False.elim⟩
      simp only [SupportsStmt, trNormal]

Premises used: Finset.mem_univ, Turing.TM1to1.tr, Finset.mem_image, Turing.TM1to1.writes, Turing.TM1to1.trNormal, Turing.TM1to1.move, Finset.notMem_empty, Turing.TM1to1.write, Turing.TM1to1.supportsStmt_write, Finset.mem_union, Turing.TM1to1.supportsStmt_move, Turing.TM1.SupportsStmt, rfl, true_and