-- Mathlib/Computability/PostTuringMachine.lean
theorem stepAux_write (q : Stmt Bool (Λ' Γ Λ σ) σ) (v : σ) (a b : Γ) (L R : ListBlank Γ) :
    stepAux (write (enc a).toList q) v (trTape' enc0 L (ListBlank.cons b R)) =
      stepAux q v (trTape' enc0 (ListBlank.cons a L) R)

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
⊢ stepAux (write (enc a).toList q) v (trTape' enc0 L (ListBlank.cons b R)) =
    stepAux q v (trTape' enc0 (ListBlank.cons a L) R)

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

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

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

Tactic:
rw [List.reverseAux, ← IH (a :: l₁) l₂' e]

Result:
case cons.cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : l₂'.length = l₂.length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append (a :: l₁) L') (ListBlank.append l₂' R'))

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

Tactic:
simp [stepAux, ListBlank.append, write]

Result:
no goals

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
⊢ ∀ {L' R' : ListBlank Bool} (l₁ l₂ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
intro L' R' l₁ l₂ l₂' e

Result:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ l₂ l₂' : List Bool
e : l₂'.length = l₂.length
⊢ stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
    stepAux q 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
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
⊢ stepAux (write (enc a).toList q) v
      (Tape.mk' (L.flatMap (fun x => (enc x).toList.reverse) ⋯)
        (ListBlank.append (enc b).toList (R.flatMap (fun x => (enc x).toList) ⋯))) =
    stepAux q 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 ∀ {L' R'} (l₁ l₂ l₂' : List Bool) (_ : l₂'.length = l₂.length),
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
    stepAux q v (Tape.mk' (L'.append (List.reverseAux l₂ l₁)) R') by
  exact this [] _ _ ((enc b).2.trans (enc a).2.symm)

Result:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
⊢ ∀ {L' R' : ListBlank Bool} (l₁ l₂ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Proof state:
case nil.refl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ : List Bool
e : [].length = [].length
⊢ stepAux (write [] q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux q v (Tape.mk' (ListBlank.append ([].reverseAux l₁) L') R')

Tactic:
rfl

Result:
no goals

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

Tactic:
rcases l₂' with - | ⟨b, l₂'⟩ <;>
  simp only [List.length_nil, List.length_cons, Nat.succ_inj', reduceCtorEq] at e

Result:
case cons.cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : l₂'.length = l₂.length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')