-- Mathlib/Computability/PostTuringMachine.lean
theorem trTape'_move_left (L R : ListBlank Γ) :
    (Tape.move Dir.left)^[n] (trTape' enc0 L R) = trTape' enc0 L.tail (R.cons L.head)

Proof state:
case intro.intro
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
⊢ (Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons a L) R) =
    trTape' enc0 (ListBlank.cons a L).tail (ListBlank.cons (ListBlank.cons a L).head R)

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

Result:
case intro.intro
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
⊢ (Tape.move Dir.left)^[n]
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun x => (enc x).toList.reverse) ⋯))
        (R.flatMap (fun x => (enc x).toList) ⋯)) =
    Tape.mk' (L.flatMap (fun x => (enc x).toList.reverse) ⋯)
      (ListBlank.append (enc a).toList (R.flatMap (fun x => (enc x).toList) ⋯))

Proof state:
case h.e'_2.h.e'_4
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
b : Bool
l₁ : List Bool
IH :
  ∀ {l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
        Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
l₂ : List Bool
e : (enc a).toList = (b :: l₁).reverseAux l₂
⊢ Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L'✝) (ListBlank.append l₂ R'✝)) =
    Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append (b :: l₂) R'✝)

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

Result:
no goals

Proof state:
case intro.intro.cons
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
b : Bool
l₁ : List Bool
IH :
  ∀ {l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
        Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
l₂ : List Bool
e : (enc a).toList = (b :: l₁).reverseAux l₂
⊢ (Tape.move Dir.left)^[l₁.length]
      (Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L'✝) (ListBlank.append l₂ R'✝))) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Tactic:
convert IH e

Result:
case h.e'_2.h.e'_4
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
b : Bool
l₁ : List Bool
IH :
  ∀ {l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
        Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
l₂ : List Bool
e : (enc a).toList = (b :: l₁).reverseAux l₂
⊢ Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L'✝) (ListBlank.append l₂ R'✝)) =
    Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append (b :: l₂) R'✝)

Proof state:
case intro.intro.nil
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
l₂ : List Bool
e : (enc a).toList = [].reverseAux l₂
⊢ (Tape.move Dir.left)^[[].length] (Tape.mk' (ListBlank.append [] L'✝) (ListBlank.append l₂ R'✝)) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Tactic:
cases e

Result:
case intro.intro.nil.refl
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
⊢ (Tape.move Dir.left)^[[].length] (Tape.mk' (ListBlank.append [] L'✝) (ListBlank.append (enc a).1 R'✝)) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Proof state:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
⊢ (Tape.move Dir.left)^[n] (trTape' enc0 L R) = trTape' enc0 L.tail (ListBlank.cons L.head R)

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

Result:
case intro.intro
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
⊢ (Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons a L) R) =
    trTape' enc0 (ListBlank.cons a L).tail (ListBlank.cons (ListBlank.cons a L).head R)

Proof state:
case intro.intro.nil.refl
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
⊢ (Tape.move Dir.left)^[[].length] (Tape.mk' (ListBlank.append [] L'✝) (ListBlank.append (enc a).1 R'✝)) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Tactic:
rfl

Result:
no goals

Proof state:
case intro.intro
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
⊢ (Tape.move Dir.left)^[n]
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun x => (enc x).toList.reverse) ⋯))
        (R.flatMap (fun x => (enc x).toList) ⋯)) =
    Tape.mk' (L.flatMap (fun x => (enc x).toList.reverse) ⋯)
      (ListBlank.append (enc a).toList (R.flatMap (fun x => (enc x).toList) ⋯))

Tactic:
suffices ∀ {L' R' l₁ l₂} (_ : Vector.toList (enc a) = List.reverseAux l₁ l₂),
    (Tape.move Dir.left)^[l₁.length]
    (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
    Tape.mk' L' (ListBlank.append (Vector.toList (enc a)) R') by
  simpa only [List.length_reverse, Vector.toList_length] using this (List.reverse_reverse _).symm

Result:
case intro.intro
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
⊢ ∀ {L' R' : ListBlank Bool} {l₁ l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
        Tape.mk' L' (ListBlank.append (enc a).toList R')

Proof state:
case intro.intro.cons
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
b : Bool
l₁ : List Bool
IH :
  ∀ {l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
        Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
l₂ : List Bool
e : (enc a).toList = (b :: l₁).reverseAux l₂
⊢ (Tape.move Dir.left)^[(b :: l₁).length] (Tape.mk' (ListBlank.append (b :: l₁) L'✝) (ListBlank.append l₂ R'✝)) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Tactic:
simp only [List.length, List.cons_append, iterate_succ_apply]

Result:
case intro.intro.cons
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
b : Bool
l₁ : List Bool
IH :
  ∀ {l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
        Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
l₂ : List Bool
e : (enc a).toList = (b :: l₁).reverseAux l₂
⊢ (Tape.move Dir.left)^[l₁.length]
      (Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L'✝) (ListBlank.append l₂ R'✝))) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)