-- Mathlib/Computability/TuringMachine.lean
theorem tr_supports {S} (ss : TM2.Supports M S) : TM1.Supports (tr M) (trSupp M S) :=
  ⟨Finset.mem_biUnion.2 ⟨_, ss.1, Finset.mem_insert.2 <| Or.inl rfl⟩, fun l' h ↦ by
    suffices ∀ (q) (_ : TM2.SupportsStmt S q) (_ : ∀ x ∈ trStmts₁ q, x ∈ trSupp M S),
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
        ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l') by
      rcases Finset.mem_biUnion.1 h with ⟨l, lS, h⟩
      have :=
        this _ (ss.2 l lS) fun x hx ↦ Finset.mem_biUnion.2 ⟨_, lS, Finset.mem_insert_of_mem hx⟩
      rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ h]
    clear h l'
    refine stmtStRec ?_ ?_ ?_ ?_ ?_
    · intro _ s _ IH ss' sub -- stack op
      rw [TM2to1.supports_run] at ss'
      simp only [TM2to1.trStmts₁_run, Finset.mem_union, Finset.mem_insert, Finset.mem_singleton]
        at sub
      have hgo := sub _ (Or.inl <| Or.inl rfl)
      have hret := sub _ (Or.inl <| Or.inr rfl)
      obtain ⟨IH₁, IH₂⟩ := IH ss' fun x hx ↦ sub x <| Or.inr hx
      refine ⟨by simp only [trNormal_run, TM1.SupportsStmt]; intros; exact hgo, fun l h ↦ ?_⟩
      rw [trStmts₁_run] at h
      simp only [TM2to1.trStmts₁_run, Finset.mem_union, Finset.mem_insert, Finset.mem_singleton]
        at h
      rcases h with (⟨rfl | rfl⟩ | h)
      · cases s
        · exact ⟨fun _ _ ↦ hret, fun _ _ ↦ hgo⟩
        · exact ⟨fun _ _ ↦ hret, fun _ _ ↦ hgo⟩
        · exact ⟨⟨fun _ _ ↦ hret, fun _ _ ↦ hret⟩, fun _ _ ↦ hgo⟩
      · unfold TM1.SupportsStmt TM2to1.tr
        exact ⟨IH₁, fun _ _ ↦ hret⟩
      · exact IH₂ _ h
    · intro _ _ IH ss' sub -- load
      unfold TM2to1.trStmts₁ at sub ⊢
      exact IH ss' sub
    · intro _ _ _ IH₁ IH₂ ss' sub -- branch
      unfold TM2to1.trStmts₁ at sub
      obtain ⟨IH₁₁, IH₁₂⟩ := IH₁ ss'.1 fun x hx ↦ sub x <| Finset.mem_union_left _ hx
      obtain ⟨IH₂₁, IH₂₂⟩ := IH₂ ss'.2 fun x hx ↦ sub x <| Finset.mem_union_right _ hx
      refine ⟨⟨IH₁₁, IH₂₁⟩, fun l h ↦ ?_⟩
      rw [trStmts₁] at h
      rcases Finset.mem_union.1 h with (h | h) <;> [exact IH₁₂ _ h; exact IH₂₂ _ h]
    · intro _ ss' _ -- goto
      simp only [trStmts₁, Finset.not_mem_empty]; refine ⟨?_, fun _ ↦ False.elim⟩
      exact fun _ v ↦ Finset.mem_biUnion.2 ⟨_, ss' v, Finset.mem_insert_self _ _⟩
    · intro _ _ -- halt
      simp only [trStmts₁, Finset.not_mem_empty]
      exact ⟨trivial, fun _ ↦ False.elim⟩⟩

Proof state:
case refine_1.intro.inl.inl.push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
q✝ : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt S q✝ →
    (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : σ → Γ k✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ (StAct.push a✝) q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ (StAct.push a✝) q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ (StAct.push a✝) q✝))

Tactic:
exact ⟨fun _ _ ↦ hret, fun _ _ ↦ hgo⟩

Result:
no goals

Proof state:
case refine_1.intro.inl.inl.peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
q✝ : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt S q✝ →
    (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : σ → Option (Γ k✝) → σ
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ (StAct.peek a✝) q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ (StAct.peek a✝) q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ (StAct.peek a✝) q✝))

Tactic:
exact ⟨fun _ _ ↦ hret, fun _ _ ↦ hgo⟩

Result:
no goals

Proof state:
case refine_5
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ TM2.SupportsStmt S TM2.Stmt.halt →
    (∀ x ∈ trStmts₁ TM2.Stmt.halt, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
        ∀ l' ∈ trStmts₁ TM2.Stmt.halt, TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
intro _ _

Result:
case refine_5
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
x✝¹ : TM2.SupportsStmt S TM2.Stmt.halt
x✝ : ∀ x ∈ trStmts₁ TM2.Stmt.halt, x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
    ∀ l' ∈ trStmts₁ TM2.Stmt.halt, TM1.SupportsStmt (trSupp M S) (tr M l')

Proof state:
case refine_5
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
x✝¹ : TM2.SupportsStmt S TM2.Stmt.halt
x✝ : ∀ x ∈ trStmts₁ TM2.Stmt.halt, x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
exact ⟨trivial, fun _ ↦ False.elim⟩

Result:
no goals

Proof state:
case refine_4
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ x ∈ trStmts₁ (TM2.Stmt.goto l✝), x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝)) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
refine ⟨?_, fun _ ↦ False.elim⟩

Result:
case refine_4
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ x ∈ trStmts₁ (TM2.Stmt.goto l✝), x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝))

Proof state:
case intro.intro
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
l' : Λ' K Γ Λ σ
h✝ : l' ∈ trSupp M S
this✝ :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt S q →
      (∀ x ∈ trStmts₁ q, x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧ ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ
lS : l ∈ S
h : l' ∈ insert (normal l) (trStmts₁ (M l))
this : TM1.SupportsStmt (trSupp M S) (trNormal (M l)) ∧ ∀ l' ∈ trStmts₁ (M l), TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ h]

Result:
no goals