-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
N : TM2.Stmt Γ Λ σ
run :
  ∀ (k : K) (s : StAct K Γ σ k) (q : TM2.Stmt Γ Λ σ)
    (IH :
      ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
        (hT :
          ∀ (k : K),
            ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
        ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
          TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) q v S) b ∧
            Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) q) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
              b)
    {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
    (hT :
      ∀ (k : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
    ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) s q) v S) b ∧
        Reaches (TM1.step (tr (Γ := Γ) M))
          (TM1.stepAux (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) N v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) N) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
have load : ∀ (a : σ → σ) (q : TM2.Stmt Γ Λ σ)
  (IH :
    ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
      (hT :
        ∀ (k : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
      ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
        TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) q v S) b ∧
          Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) q) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
            b)
  {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
  (hT :
    ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
  ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q) v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
Tactic: induction N using stmtStRec generalizing v S L hT with
  | run k s q IH => exact tr_respects_aux M hT s @IH
  | load a _ IH => exact IH _ hT
  | branch p q₁ q₂ IH₁ IH₂ =>
    unfold TM2.stepAux trNormal TM1.stepAux
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/12129): additional beta reduction needed
    beta_reduce
    cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]
  | goto => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
  | halt => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
Cleared hypotheses: v, S, L, hT, N