-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
v : σ
L : ListBlank Γ
q : Stmt Γ Λ σ
R : ListBlank Γ
some :
  ∀ (d : Dir) (q : Stmt Γ Λ σ)
    (IH :
      ∀ (v : σ) (L R : ListBlank Γ),
        Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
          (trCfg enc enc0 (stepAux q v (Tape.mk' L R))))
    (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move d q)) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux (Stmt.move d q) v (Tape.mk' L R)))
some₁ :
  ∀ (f : Γ → σ → Γ) (q : Stmt Γ Λ σ)
    (IH :
      ∀ (v : σ) (L R : ListBlank Γ),
        Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
          (trCfg enc enc0 (stepAux q v (Tape.mk' L R))))
    (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.write f q)) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux (Stmt.write f q) v (Tape.mk' L R)))
some₂ :
  ∀ (a : Γ → σ → σ) (q : Stmt Γ Λ σ)
    (IH :
      ∀ (v : σ) (L R : ListBlank Γ),
        Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
          (trCfg enc enc0 (stepAux q v (Tape.mk' L R))))
    (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.load a q)) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux (Stmt.load a q) v (Tape.mk' L R)))
some₃ :
  ∀ (p : Γ → σ → Bool) (q₁ q₂ : Stmt Γ Λ σ)
    (IH₁ :
      ∀ (v : σ) (L R : ListBlank Γ),
        Reaches (step (tr enc dec M)) (stepAux (trNormal dec q₁) v (trTape' enc0 L R))
          (trCfg enc enc0 (stepAux q₁ v (Tape.mk' L R))))
    (IH₂ :
      ∀ (v : σ) (L R : ListBlank Γ),
        Reaches (step (tr enc dec M)) (stepAux (trNormal dec q₂) v (trTape' enc0 L R))
          (trCfg enc enc0 (stepAux q₂ v (Tape.mk' L R))))
    (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.branch p q₁ q₂)) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux (Stmt.branch p q₁ q₂) v (Tape.mk' L R)))
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
have some₄ : ∀ (l : Γ → σ → Λ) (v : σ) (L R : ListBlank Γ),
  Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.goto l)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.goto l) v (Tape.mk' L R)))
Tactic: induction q generalizing v L R with
    | move d q IH =>
      cases d <;>
          simp only [trNormal, stepAux_move, stepAux,
            Tape.move_left_mk',
            trTape'_move_left enc0, trTape'_move_right enc0] <;>
        apply IH
    | write f q IH =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux]
      refine ReflTransGen.head rfl ?_
      obtain ⟨a, R, rfl⟩ := R.exists_cons
      rw [tr, Tape.mk'_head, stepAux_write, ListBlank.head_cons, stepAux_move,
        trTape'_move_left enc0]
      simpa using IH ..
    | load a q IH =>
      simp only [trNormal, stepAux_read dec enc0 encdec]
      apply IH
    | branch p q₁ q₂ IH₁ IH₂ =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, Tape.mk'_head]
      grind
    | goto l =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, trCfg, trTape_mk']
      apply ReflTransGen.refl
    | halt =>
      simp only [trNormal, stepAux, trCfg,
        trTape_mk']
      apply ReflTransGen.refl
Cleared hypotheses: v, L, q, R