-- Mathlib/Computability/TuringMachine.lean
theorem addBottom_modifyNth (f : (∀ k, Option (Γ k)) → ∀ k, Option (Γ k))
    (L : ListBlank (∀ k, Option (Γ k))) (n : ℕ) :
    (addBottom L).modifyNth (fun a ↦ (a.1, f a.2)) n = addBottom (L.modifyNth f n)

Proof state:
case succ
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.cons (true, L.head)
      (ListBlank.modifyNth (fun a => (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)) =
    ListBlank.cons (true, L.head) (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail))

Tactic:
congr

Result:
case succ.e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.modifyNth (fun a => (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail) =
    ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail)

Proof state:
case succ.e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail) =
    ListBlank.modifyNth (fun a => (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)

Tactic:
apply ListBlank.map_modifyNth

Result:
case succ.e_l.H
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ∀ (x : (k : K) → Option (Γ k)),
    { f := Prod.mk false, map_pt' := ⋯ }.f (f x) =
      (({ f := Prod.mk false, map_pt' := ⋯ }.f x).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x).2)

Proof state:
case succ.e_l.H
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
x✝ : (k : K) → Option (Γ k)
⊢ { f := Prod.mk false, map_pt' := ⋯ }.f (f x✝) =
    (({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).2)

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ ListBlank.modifyNth (fun a => (a.1, f a.2)) n (addBottom L) = addBottom (ListBlank.modifyNth f n L)

Tactic:
cases n <;>
  simp only [addBottom, ListBlank.head_cons, ListBlank.modifyNth, ListBlank.tail_cons]

Result:
case succ
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.cons (true, L.head)
      (ListBlank.modifyNth (fun a => (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)) =
    ListBlank.cons (true, L.head) (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail))

Proof state:
case succ.e_l.H
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ∀ (x : (k : K) → Option (Γ k)),
    { f := Prod.mk false, map_pt' := ⋯ }.f (f x) =
      (({ f := Prod.mk false, map_pt' := ⋯ }.f x).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x).2)

Tactic:
intro

Result:
case succ.e_l.H
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
x✝ : (k : K) → Option (Γ k)
⊢ { f := Prod.mk false, map_pt' := ⋯ }.f (f x✝) =
    (({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).2)

Proof state:
case succ.e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.modifyNth (fun a => (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail) =
    ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail)

Tactic:
symm

Result:
case succ.e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail) =
    ListBlank.modifyNth (fun a => (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)