-- 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
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L R : ListBlank Γ
⊢ ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L R) =
      stepAux (f (enc R.head)) v (trTape' enc0 (ListBlank.cons R.head L) R.tail)

Tactic:
obtain ⟨a, R, rfl⟩ := R.exists_cons

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 (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)

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 Γ
⊢ ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (L' R' : ListBlank Bool) (l₁ l₂ : List Bool)
    (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
clear f L a R

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
v : σ
⊢ ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (L' R' : ListBlank Bool) (l₁ l₂ : List Bool)
    (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) 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
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' (?m.119027 i) (?m.119028 i) σ) σ) (L' R' : ListBlank Bool)
    (l₁ l₂ : List Bool) (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
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) ⋯))

Tactic:
exact this n f (L.flatMap (fun x => (enc x).1.reverse) _)
  (R.flatMap (fun x => (enc x).1) _) [] _ (enc a).2

Result:
no goals

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
v : σ
i : ℕ
f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ
L' R' : ListBlank Bool
l₁ l₂ : List Bool
h✝ : l₂.length = i
⊢ stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
    stepAux (f ⟨l₂, h✝⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
subst i

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
v : σ
L' R' : ListBlank Bool
l₁ 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')

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
        (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) ⋯))

Tactic:
suffices ∀ i f L' R' l₁ l₂ h,
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
    stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R') by
  intro f
  exact this n f (L.flatMap (fun x => (enc x).1.reverse) _)
    (R.flatMap (fun x => (enc x).1) _) [] _ (enc a).2

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 Γ
⊢ ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (L' R' : ListBlank Bool) (l₁ l₂ : List Bool)
    (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) 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 (Λ' Γ Λ σ) σ
⊢ stepAux (f (a ::ᵥ ⟨l₂, ⋯⟩)) v (Tape.mk' (ListBlank.append (l₂.reverseAux (a :: l₁)) L') R') =
    stepAux (f ⟨a :: l₂, ⋯⟩) v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
rfl

Result:
no goals