awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
⊢ TrCfg.{u_1, u_2, u_3, u_4} (Γ := Γ) (Λ := Λ) (σ := σ) (TM2.init (Γ := Γ) k L)
    { l := Option.map (normal (Γ := Γ)) (some default), var := default,
      Tape :=
        Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.mk
              (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse))) }

Tactic:
⟨ListBlank.mk (L.reverse.map fun a ↦ update default k (some a)), fun k' ↦ ?_⟩

Premises used: Turing.ListBlank.mk, Inhabited.default, Function.update, List.map, Option.some, List.reverse, Turing.TM2.init, Turing.TM2to1.TrCfg.mk
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
refine :
  ∀ (k' : K),
    Eq.{u_2 + 1} (α := ListBlank (Option (Γ k')))
      (ListBlank.map (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
          (ListBlank.mk
            (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse)) :
        ListBlank (Option (Γ k')))
      (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k'))) :
        ListBlank (Option (Γ k')))
⊢ TrCfg.{u_1, u_2, u_3, u_4} (Γ := Γ) (Λ := Λ) (σ := σ) (TM2.init (Γ := Γ) k L)
    { l := Option.map (normal (Γ := Γ)) (some default), var := default,
      Tape :=
        Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.mk
              (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse))) }

Tactic:
refine ⟨ListBlank.mk (L.reverse.map fun a ↦ update default k (some a)), fun k' ↦ ?_⟩
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
k' : K
⊢ Eq.{u_2 + 1} (α := ListBlank (Option (Γ k')))
    (ListBlank.map (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
        (ListBlank.mk
          (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse)) :
      ListBlank (Option (Γ k')))
    (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k'))) :
      ListBlank (Option (Γ k')))

Tactic:
ListBlank.ext fun i ↦ ?_

Premises used: Turing.ListBlank.ext
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
k' : K
refine :
  ∀ (i : ℕ),
    Eq.{u_2 + 1} (α := Option (Γ k'))
      (ListBlank.nth
          (ListBlank.map (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
            (ListBlank.mk
              (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse)))
          i :
        Option (Γ k'))
      (ListBlank.nth
          (ListBlank.mk
            (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k'))))
          i :
        Option (Γ k'))
⊢ Eq.{u_2 + 1} (α := ListBlank (Option (Γ k')))
    (ListBlank.map (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
        (ListBlank.mk
          (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse)) :
      ListBlank (Option (Γ k')))
    (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k'))) :
      ListBlank (Option (Γ k')))

Tactic:
refine ListBlank.ext fun i ↦ ?_

Premises used: Turing.ListBlank.ext
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
rw :
  (getElem? (coll := List (Option (Γ k'))) (valid := fun (as : List (Option (Γ k'))) (i : ℕ) ↦ i < as.length)
          (List.map
              (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k'))
                fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a))
              L.reverse :
            List (Option (Γ k')))
          i).getD
      default =
    ListBlank.nth
      (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k')))) i
⊢ Eq.{u_2 + 1} (α := Option (Γ k'))
    (ListBlank.nth
        (ListBlank.map (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
          (ListBlank.mk
            (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse)))
        i :
      Option (Γ k'))
    (ListBlank.nth
        (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k'))))
        i :
      Option (Γ k'))

Tactic:
rw [ListBlank.map_mk, ListBlank.nth_mk, List.getI_eq_getElem?_getD, List.map_map]

Premises used: Turing.ListBlank.map_mk, List.map_map, List.getI_eq_getElem?_getD, Turing.ListBlank.nth_mk
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
⊢ Eq.{u_2 + 1} (α := Γ k → Option (Γ k'))
    (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k'))
        fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) :
      Γ k → Option (Γ k'))
    fun (a : Γ k) ↦
    (PointedMap.f (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
        (update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) :
      Option (Γ k'))

Tactic:
have : ((proj k').f ∘ fun a => update (β := fun k => Option (Γ k)) default k (some a))
      = fun a => (proj k').f (update (β := fun k => Option (Γ k)) default k (some a)) := rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this :
  Eq.{u_2 + 1} (α := Γ k → Option (Γ k'))
    (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k'))
        fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) :
      Γ k → Option (Γ k'))
    fun (a : Γ k) ↦
    (PointedMap.f (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
        (update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) :
      Option (Γ k'))
rw :
  Eq (α := Option (Γ k'))
    (Option.getD
      (Option.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) k')
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default)
    (ListBlank.nth
      (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k'))))
      i)
⊢ (getElem? (coll := List (Option (Γ k'))) (valid := fun (as : List (Option (Γ k'))) (i : ℕ) ↦ i < as.length)
          (List.map
              (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k'))
                fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a))
              L.reverse :
            List (Option (Γ k')))
          i).getD
      default =
    ListBlank.nth
      (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k')))) i

Tactic:
rw [this, List.getElem?_map, proj, PointedMap.mk_val]

Premises used: Turing.proj, List.getElem?_map, Turing.PointedMap.mk_val
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this :
  Eq.{u_2 + 1} (α := Γ k → Option (Γ k'))
    (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k'))
        fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) :
      Γ k → Option (Γ k'))
    fun (a : Γ k) ↦
    (PointedMap.f (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
        (update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) :
      Option (Γ k'))
pos :
  ∀ (h : k' = k),
    Eq (α := Option (Γ k'))
      (Option.getD
        (Option.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) k')
          (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
        default)
      (ListBlank.nth
        (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k'))))
        i)
neg :
  ∀ (h : ¬k' = k),
    Eq (α := Option (Γ k'))
      (Option.getD
        (Option.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) k')
          (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
        default)
      (ListBlank.nth
        (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k'))))
        i)
⊢ Eq (α := Option (Γ k'))
    (Option.getD
      (Option.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) k')
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default)
    (ListBlank.nth
      (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k'))))
      i)

Tactic:
by_cases h : k' = k
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this :
  Eq.{u_2 + 1} (α := Γ k → Option (Γ k'))
    (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k'))
        fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) :
      Γ k → Option (Γ k'))
    fun (a : Γ k) ↦
    (PointedMap.f (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
        (update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) :
      Option (Γ k'))
h : k' = k
pos :
  ∀
    (this :
      Eq.{u_2 + 1} (α := Γ k → Option (Γ k))
        (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k))
            fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) :
          Γ k → Option (Γ k))
        fun (a : Γ k) ↦
        (PointedMap.f (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k)
            (update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) :
          Option (Γ k))),
    Eq (α := Option (Γ k))
      (Option.getD
        (Option.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) k)
          (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
        default)
      (ListBlank.nth
        (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k))))
        i)
⊢ Eq (α := Option (Γ k'))
    (Option.getD
      (Option.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) k')
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default)
    (ListBlank.nth
      (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k'))))
      i)

Tactic:
subst k'
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
i : ℕ
this :
  Eq.{u_2 + 1} (α := Γ k → Option (Γ k))
    (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k))
        fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) :
      Γ k → Option (Γ k))
    fun (a : Γ k) ↦
    (PointedMap.f (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k)
        (update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) :
      Option (Γ k))
pos :
  Option.getD
      (Option.map (fun (a : Γ k) ↦ some a)
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default =
    ListBlank.nth (ListBlank.mk (List.map some L).reverse) i
⊢ Eq (α := Option (Γ k))
    (Option.getD
      (Option.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) k)
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default)
    (ListBlank.nth
      (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k)))) i)

Tactic:
simp only [Function.update_self]

Premises used: Function.update_self
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
i : ℕ
this :
  Eq.{u_2 + 1} (α := Γ k → Option (Γ k))
    (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k))
        fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) :
      Γ k → Option (Γ k))
    fun (a : Γ k) ↦
    (PointedMap.f (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k)
        (update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) :
      Option (Γ k))
pos :
  Option.getD
      (Option.map (fun (a : Γ k) ↦ some a)
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default =
    (List.map some L).reverse.getI i
pos₁ :
  Option.getD
      (Option.map (fun (a : Γ k) ↦ some a)
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default =
    (getElem? (valid := fun (as : List (Option (Γ k))) (i : ℕ) ↦ i < as.length) (List.map some L).reverse i).getD
      default
pos₂ :
  Option.getD
      (Option.map (fun (a : Γ k) ↦ some a)
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default =
    (getElem? (valid := fun (as : List (Option (Γ k))) (i : ℕ) ↦ i < as.length) (List.map some L.reverse) i).getD
      default
pos₃ pos₄ :
  Option.getD
      (Option.map (fun (a : Γ k) ↦ some a)
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default =
    (Option.map some (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i)).getD default
⊢ Option.getD
      (Option.map (fun (a : Γ k) ↦ some a)
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default =
    ListBlank.nth (ListBlank.mk (List.map some L).reverse) i

Tactic:
rw [ListBlank.nth_mk, List.getI_eq_getElem?_getD, ← List.map_reverse, List.getElem?_map]

Premises used: List.getElem?_map, List.getI_eq_getElem?_getD, List.map_reverse, Turing.ListBlank.nth_mk
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this :
  Eq.{u_2 + 1} (α := Γ k → Option (Γ k'))
    (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k'))
        fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) :
      Γ k → Option (Γ k'))
    fun (a : Γ k) ↦
    (PointedMap.f (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
        (update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) :
      Option (Γ k'))
h : ¬k' = k
neg :
  Eq (α := Option (Γ k'))
    (Option.getD
      (Option.map (fun (a : Γ k) ↦ default k')
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default)
    (ListBlank.nth (ListBlank.mk (List.reverse (List.map some []))) i)
⊢ Eq (α := Option (Γ k'))
    (Option.getD
      (Option.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) k')
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default)
    (ListBlank.nth
      (ListBlank.mk (List.reverse (List.map some (update (β := fun (k : K) ↦ List (Γ k)) (fun (x : K) ↦ []) k L k'))))
      i)

Tactic:
simp only [Function.update_of_ne h]

Premises used: Function.update_of_ne
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this :
  Eq.{u_2 + 1} (α := Γ k → Option (Γ k'))
    (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k'))
        fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) :
      Γ k → Option (Γ k'))
    fun (a : Γ k) ↦
    (PointedMap.f (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
        (update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) :
      Option (Γ k'))
h : ¬k' = k
neg :
  Option.getD (Option.map (fun (a : Γ k) ↦ default k') none) default =
    (getElem? (valid := fun (as : List (Option (Γ k'))) (i : ℕ) ↦ i < as.length) [] i).getD default
neg₁ :
  ∀ (val : Γ k),
    Option.getD (Option.map (fun (a : Γ k) ↦ default k') (some val)) default =
      (getElem? (valid := fun (as : List (Option (Γ k'))) (i : ℕ) ↦ i < as.length) [] i).getD default
⊢ Option.getD
      (Option.map (fun (a : Γ k) ↦ default k')
        (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i))
      default =
    (getElem? (valid := fun (as : List (Option (Γ k'))) (i : ℕ) ↦ i < as.length) [] i).getD default

Tactic:
cases L.reverse[i]?

Premises used: List.reverse
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this :
  Eq.{u_2 + 1} (α := Γ k → Option (Γ k'))
    (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k'))
        fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) :
      Γ k → Option (Γ k'))
    fun (a : Γ k) ↦
    (PointedMap.f (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
        (update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) :
      Option (Γ k'))
h : ¬k' = k
⊢ Option.getD (Option.map (fun (a : Γ k) ↦ default k') none) default =
    (getElem? (valid := fun (as : List (Option (Γ k'))) (i : ℕ) ↦ i < as.length) [] i).getD default

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this :
  Eq.{u_2 + 1} (α := Γ k → Option (Γ k'))
    (Function.comp (β := (i : K) → Option (Γ i)) (PointedMap.f (proj (Γ := fun (k : K) ↦ Option (Γ k)) k'))
        fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a) :
      Γ k → Option (Γ k'))
    fun (a : Γ k) ↦
    (PointedMap.f (Γ := (i : K) → Option (Γ i)) (proj (Γ := fun (k : K) ↦ Option (Γ k)) k')
        (update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) :
      Option (Γ k'))
h : ¬k' = k
val : Γ k
⊢ Option.getD (Option.map (fun (a : Γ k) ↦ default k') (some val)) default =
    (getElem? (valid := fun (as : List (Option (Γ k'))) (i : ℕ) ↦ i < as.length) [] i).getD default

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
e_Tape :
  Eq (α := (k : K) → Option (Γ k))
    (List.headI
        (List.map (fun (a : Γ k) ↦ (false, update (β := fun (k : K) ↦ Option (Γ k)) (fun (x : K) ↦ none) k (some a)))
          L.reverse)).2
    (ListBlank.head
      (ListBlank.mk (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse)))
e_Tape₁ :
  Eq (α := List (Γ' K Γ))
    (List.tail
      (List.map (fun (a : Γ k) ↦ (false, update (β := fun (k : K) ↦ Option (Γ k)) (fun (x : K) ↦ none) k (some a)))
        L.reverse))
    (List.map (PointedMap.f { f := Prod.mk false, map_pt' := ⋯ : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) })
      (List.tail (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse)))
⊢ Eq (α := TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ)
    { l := some default, var := default,
      Tape :=
        Tape.mk₁
          ((true,
              (List.headI
                  (List.map
                    (fun (a : Γ k) ↦ (false, update (β := fun (k : K) ↦ Option (Γ k)) (fun (x : K) ↦ none) k (some a)))
                    L.reverse)).2) ::
            List.tail
              (List.map
                (fun (a : Γ k) ↦ (false, update (β := fun (k : K) ↦ Option (Γ k)) (fun (x : K) ↦ none) k (some a)))
                L.reverse)) }
    { l := Option.map (normal (Γ := Γ)) (some default), var := default,
      Tape :=
        Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.mk
              (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse))) }

Tactic:
congr
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
e_Tape :
  Eq (α := (k : K) → Option (Γ k))
    (List.headI
        (List.map (fun (a : Γ k) ↦ (false, update (β := fun (k : K) ↦ Option (Γ k)) (fun (x : K) ↦ none) k (some a)))
          [])).2
    (ListBlank.head
      (ListBlank.mk (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) [])))
e_Tape₁ :
  ∀ (head : Γ k) (tail : List (Γ k)),
    Eq (α := (k : K) → Option (Γ k))
      (List.headI
          (List.map (fun (a : Γ k) ↦ (false, update (β := fun (k : K) ↦ Option (Γ k)) (fun (x : K) ↦ none) k (some a)))
            (head :: tail))).2
      (ListBlank.head
        (ListBlank.mk
          (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) (head :: tail))))
⊢ Eq (α := (k : K) → Option (Γ k))
    (List.headI
        (List.map (fun (a : Γ k) ↦ (false, update (β := fun (k : K) ↦ Option (Γ k)) (fun (x : K) ↦ none) k (some a)))
          L.reverse)).2
    (ListBlank.head
      (ListBlank.mk (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse)))

Tactic:
cases L.reverse

Premises used: List.reverse