-- Mathlib/Computability/PostTuringMachine.lean
theorem stepAux_read (f : Γ → Stmt Bool (Λ' Γ Λ σ) σ) (v : σ) (L R : ListBlank Γ) :
    stepAux (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R)

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ (bif (ListBlank.cons a (ListBlank.append l₂ R')).head then
      stepAux (readAux l₂.length fun v => f (true ::ᵥ v)) v
        (Tape.move Dir.right (Tape.mk' (ListBlank.append l₁ L') (ListBlank.cons a (ListBlank.append l₂ R'))))
    else
      stepAux (readAux l₂.length fun v => f (false ::ᵥ v)) v
        (Tape.move Dir.right (Tape.mk' (ListBlank.append l₁ L') (ListBlank.cons a (ListBlank.append l₂ R'))))) =
    stepAux (readAux l₂.length fun v => f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))

Tactic:
simp only [ListBlank.head_cons, Tape.move_right_mk', ListBlank.tail_cons]

Result:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ (bif a then
      stepAux (readAux l₂.length fun v => f (true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun v => f (false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))) =
    stepAux (readAux l₂.length fun v => f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))

Proof state:
case intro.intro.nil
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₁ : List Bool
f : List.Vector Bool [].length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux [].length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux (f ⟨[], ⋯⟩) v (Tape.mk' (ListBlank.append ([].reverseAux l₁) L') R')

Tactic:
rfl

Result:
no goals

Proof state:
case intro.intro.cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux (a :: l₂).length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (a :: l₂) R')) =
    stepAux (f ⟨a :: l₂, ⋯⟩) v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
trans
  stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
    (Tape.mk' ((L'.append l₁).cons a) (R'.append l₂))

Result:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux (a :: l₂).length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (a :: l₂) R')) =
    stepAux (readAux l₂.length fun v => f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))

Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux l₂.length fun v => f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R')) =
    stepAux (f ⟨a :: l₂, ⋯⟩) v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Proof state:
case intro.intro
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L (ListBlank.cons a R)) =
      stepAux (f (enc (ListBlank.cons a R).head)) v
        (trTape' enc0 (ListBlank.cons (ListBlank.cons a R).head L) (ListBlank.cons a R).tail)

Tactic:
simp only [ListBlank.head_cons, ListBlank.tail_cons, trTape', ListBlank.cons_flatMap,
  ListBlank.append_assoc]

Result:
case intro.intro
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v
        (Tape.mk' (L.flatMap (fun x => (enc x).toList.reverse) ⋯)
          (ListBlank.append (enc a).toList (R.flatMap (fun x => (enc x).toList) ⋯))) =
      stepAux (f (enc a)) v
        (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun x => (enc x).toList.reverse) ⋯))
          (R.flatMap (fun x => (enc x).toList) ⋯))