-- Mathlib/Computability/PostTuringMachine.lean
theorem tr_supports [Inhabited Λ] {S : Finset Λ} (ss : Supports M S) :
    Supports (tr enc dec M) (trSupp M S) :=
  ⟨Finset.mem_biUnion.2 ⟨_, ss.1, Finset.mem_insert_self _ _⟩, fun q h ↦ by
    suffices ∀ q, SupportsStmt S q → (∀ 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') by
      rcases Finset.mem_biUnion.1 h with ⟨l, hl, h⟩
      have :=
        this _ (ss.2 _ hl) fun q' hq ↦ Finset.mem_biUnion.2 ⟨_, hl, Finset.mem_insert_of_mem hq⟩
      rcases Finset.mem_insert.1 h with (rfl | h)
      exacts [this.1, this.2 _ h]
    intro q hs hw
    induction q with
    | move d q IH =>
      unfold writes at hw ⊢
      replace IH := IH hs hw; refine ⟨?_, IH.2⟩
      cases d <;> simp only [trNormal, iterate, supportsStmt_move, IH]
    | write f q IH =>
      unfold writes at hw ⊢
      simp only [Finset.mem_image, Finset.mem_union, Finset.mem_univ, exists_prop, 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.not_mem_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.not_mem_empty]; refine ⟨?_, fun _ ↦ False.elim⟩
      simp only [SupportsStmt, supportsStmt_move, trNormal]⟩

Proof state:
case goto
Γ : 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✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
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))

Tactic:
refine supportsStmt_read _ fun a _ s ↦ ?_

Result:
case goto
Γ : 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✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
a : Γ
x✝ : Bool
s : σ
⊢ (fun x s => Λ'.normal (l a s)) x✝ s ∈ trSupp M S

Proof state:
case move
Γ : 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✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
IH :
  SupportsStmt S q →
    (∀ 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 q, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
replace IH := IH hs hw

Result:
case move
Γ : 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✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.move d q)
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Proof state:
Γ : 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✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
this :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S q →
      (∀ 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')
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)

Tactic:
rcases Finset.mem_biUnion.1 h with ⟨l, hl, h⟩

Result:
case intro.intro
Γ : 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✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h✝ : q ∈ trSupp M S
this :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S q →
      (∀ 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')
l : Λ
hl : l ∈ S
h : q ∈ insert (Λ'.normal l) (writes (M l))
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)

Proof state:
case write
Γ : 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✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  SupportsStmt S q →
    (∀ 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' ∈ Finset.image (fun a => Λ'.write a q) Finset.univ ∪ writes q, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.write f q)) ∧
    ∀ q' ∈ Finset.image (fun a => Λ'.write a q) Finset.univ ∪ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
simp only [Finset.mem_image, Finset.mem_union, Finset.mem_univ, exists_prop, true_and]
  at hw ⊢

Result:
case write
Γ : 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✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  SupportsStmt S q →
    (∀ 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' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ q' ∈ writes q → q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.write f q)) ∧
    ∀ (q' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ q' ∈ writes q → SupportsStmt (trSupp M S) (tr enc dec M q')