-- Mathlib/Computability/TuringMachine.lean
theorem tr_respects_aux {q v T k} {S : ∀ k, List (Γ k)}
    (hT : ∀ k, ListBlank.map (proj k) T = ListBlank.mk ((S k).map some).reverse)
    (o : StAct K Γ σ k)
    (IH : ∀ {v : σ} {S : ∀ k : K, List (Γ k)} {T : ListBlank (∀ k, Option (Γ k))},
      (∀ k, ListBlank.map (proj k) T = ListBlank.mk ((S k).map some).reverse) →
      ∃ b, TrCfg (TM2.stepAux q v S) b ∧
        Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b) :
    ∃ b, TrCfg (TM2.stepAux (stRun o q) v S) b ∧ Reaches (TM1.step (tr M))
      (TM1.stepAux (trNormal (stRun o q)) v (Tape.mk' ∅ (addBottom T))) b

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b
⊢ ∃ b,
    TrCfg (TM2.stepAux (stRun o q) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (stRun o q)) v (Tape.mk' ∅ (addBottom T))) b

Tactic:
simp only [trNormal_run, step_run]

Result:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b
⊢ ∃ b,
    TrCfg (TM2.stepAux q (stVar v (S k) o) (update S k (stWrite v (S k) o))) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (goto fun x x => go k o q) v (Tape.mk' ∅ (addBottom T))) b

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b
⊢ ∃ b,
    TrCfg (TM2.stepAux q (stVar v (S k) o) (update S k (stWrite v (S k) o))) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (goto fun x x => go k o q) v (Tape.mk' ∅ (addBottom T))) b

Tactic:
have hgo := tr_respects_aux₁ M o q v (hT k) _ le_rfl

Result:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b
hgo :
  Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom T) }
    { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom T)) }
⊢ ∃ b,
    TrCfg (TM2.stepAux q (stVar v (S k) o) (update S k (stWrite v (S k) o))) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (goto fun x x => go k o q) v (Tape.mk' ∅ (addBottom T))) b

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 Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b
hgo :
  Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom T) }
    { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom T)) }
T' : ListBlank ((k : K) → Option (Γ k))
hT' :
  ∀ (k_1 : K),
    ListBlank.map (proj k_1) T' = ListBlank.mk (List.map some (update S k (stWrite ?m.137053 (S k) o) k_1)).reverse
hrun :
  TM1.stepAux (trStAct ?m.137052 o) ?m.137053 ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom T))) =
    TM1.stepAux ?m.137052 (stVar ?m.137053 (S k) o)
      ((Tape.move Dir.right)^[(update S k (stWrite ?m.137053 (S k) o) k).length] (Tape.mk' ∅ (addBottom T')))
this :
  Reaches₁ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom T) }
    (TM1.stepAux (tr M (go k o q)) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom T))))
⊢ ∃ b,
    TrCfg (TM2.stepAux q (stVar v (S k) o) (update S k (stWrite v (S k) o))) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (goto fun x x => go k o q) v (Tape.mk' ∅ (addBottom T))) b

Tactic:
rw [tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_snd,
  stk_nth_val _ (hT k), List.getElem?_eq_none (le_of_eq (List.length_reverse _)),
  Option.isNone, cond, hrun, TM1.stepAux] at this

Result:
case intro.intro
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b
hgo :
  Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom T) }
    { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom T)) }
T' : ListBlank ((k : K) → Option (Γ k))
hT' :
  ∀ (k_1 : K), ListBlank.map (proj k_1) T' = ListBlank.mk (List.map some (update S k (stWrite v (S k) o) k_1)).reverse
hrun :
  TM1.stepAux (trStAct (goto fun x x => ret q) o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom T))) =
    TM1.stepAux (goto fun x x => ret q) (stVar v (S k) o)
      ((Tape.move Dir.right)^[(update S k (stWrite v (S k) o) k).length] (Tape.mk' ∅ (addBottom T')))
this :
  Reaches₁ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom T) }
    { l := some (ret q), var := stVar v (S k) o,
      Tape := (Tape.move Dir.right)^[(update S k (stWrite v (S k) o) k).length] (Tape.mk' ∅ (addBottom T')) }
⊢ ∃ b,
    TrCfg (TM2.stepAux q (stVar v (S k) o) (update S k (stWrite v (S k) o))) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (goto fun x x => go k o q) v (Tape.mk' ∅ (addBottom T))) b