awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
    (hT :
      ∀ (k : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
    ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) q₁ v S) b ∧
        Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
IH₂ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
    (hT :
      ∀ (k : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
    ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) q₂ v S) b ∧
        Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
branch :
  ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (bif false then TM2.stepAux (Γ := Γ) q₁ v S else TM2.stepAux (Γ := Γ) q₂ v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (bif false then TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))
        else TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        b
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (bif p v then TM2.stepAux (Γ := Γ) q₁ v S else TM2.stepAux (Γ := Γ) q₂ v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (bif p v then TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))
        else TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        b
have branch₁ : ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
  TrCfg (Γ := Γ) (bif true then TM2.stepAux (Γ := Γ) q₁ v S else TM2.stepAux (Γ := Γ) q₂ v S) b ∧
    Reaches (TM1.step (tr (Γ := Γ) M))
      (bif true then TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))
      else TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
      b
Tactic: cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
N : TM2.Stmt Γ Λ σ
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) N v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) N) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
have run : ∀ (k : K) (s : StAct K Γ σ k) (q : TM2.Stmt Γ Λ σ)
  (IH :
    ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
      (hT :
        ∀ (k : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
      ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
        TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) q v S) b ∧
          Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) q) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
            b)
  {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
  (hT :
    ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
  ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) s q) v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
Tactic: induction N using stmtStRec generalizing v S L hT with
  | run k s q IH => exact tr_respects_aux M hT s @IH
  | load a _ IH => exact IH _ hT
  | branch p q₁ q₂ IH₁ IH₂ =>
    unfold TM2.stepAux trNormal TM1.stepAux
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/12129): additional beta reduction needed
    beta_reduce
    cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]
  | goto => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
  | halt => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
Cleared hypotheses: v, S, L, hT, N
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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) (TM1.init (trInit (Γ := Γ) k L))
have rw : 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: rw [(_ : TM1.init _ = _)]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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)
rw :
  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))) }
⊢ TrCfg.{u_1, u_2, u_3, u_4} (Γ := Γ) (Λ := Λ) (σ := σ) (TM2.init (Γ := Γ) k L) (TM1.init (trInit (Γ := Γ) k L))
have rw₁ : Eq (α := TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ) (TM1.init (trInit (Γ := Γ) 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: rw [(_ : TM1.init _ = _)]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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))) }
have 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')))
Tactic: refine ⟨ListBlank.mk (L.reverse.map fun a ↦ update default k (some a)), fun k' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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')))
have 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'))
Tactic: refine ListBlank.ext fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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} (α := 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'))
have 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
Tactic: rw [ListBlank.map_mk, ListBlank.nth_mk, List.getI_eq_getElem?_getD, List.map_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (hypothesis)
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 : ℕ
⊢ (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
have 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'))
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
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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'))
⊢ (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
have 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)
Tactic: rw [this, List.getElem?_map, proj, PointedMap.mk_val]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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'))
⊢ 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)
have 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)
Tactic: by_cases h : k' = k
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h : k' = k
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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
⊢ 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)
have 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)
Tactic: subst k'
Cleared hypotheses: k', this, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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))
⊢ 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)
have 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
Tactic: simp only [Function.update_self]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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))
⊢ 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
have 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
Tactic: rw [ListBlank.nth_mk, List.getI_eq_getElem?_getD, ← List.map_reverse, List.getElem?_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
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
⊢ 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
have 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
Tactic: rw [ListBlank.nth_mk, List.getI_eq_getElem?_getD, ← List.map_reverse, List.getElem?_map]