-- Mathlib/Computability/PostTuringMachine.lean
theorem stepAux_move (d : Dir) (q : Stmt Bool (Λ' Γ Λ σ) σ) (v : σ) (T : Tape Bool) :
    stepAux (move n d q) v T = stepAux q v ((Tape.move d)^[n] T)

Proof state:
case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v (((Tape.move d)^[i] ∘ Tape.move d) T)

Tactic:
simp only [stepAux, Function.comp_apply]

Result:
case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d)^[i] q) v (Tape.move d T) = stepAux q v ((Tape.move d)^[i] (Tape.move d T))

Proof state:
case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d)^[i + 1] q) v T = stepAux q v ((Tape.move d)^[i + 1] T)

Tactic:
rw [iterate_succ', iterate_succ]

Result:
case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v (((Tape.move d)^[i] ∘ Tape.move d) T)

Proof state:
case zero
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
⊢ stepAux ((Stmt.move d)^[0] q) v T = stepAux q v ((Tape.move d)^[0] T)

Tactic:
rfl

Result:
no goals

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
⊢ ∀ (i : ℕ), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)

Tactic:
intro i

Result:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
i : ℕ
⊢ stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)

Proof state:
case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d)^[i] q) v (Tape.move d T) = stepAux q v ((Tape.move d)^[i] (Tape.move d T))

Tactic:
rw [IH]

Result:
no goals

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
⊢ stepAux (move n d q) v T = stepAux q v ((Tape.move d)^[n] T)

Tactic:
suffices ∀ i, stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T) from this n

Result:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
⊢ ∀ (i : ℕ), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
i : ℕ
⊢ stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)

Tactic:
induction' i with i IH generalizing T

Result:
case zero
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
⊢ stepAux ((Stmt.move d)^[0] q) v T = stepAux q v ((Tape.move d)^[0] T)

case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d)^[i + 1] q) v T = stepAux q v ((Tape.move d)^[i + 1] T)