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
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
⊢ 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]
-- 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
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
⊢ 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 =
  (Option.map some (getElem? (valid := fun (as : List (Γ k)) (i : ℕ) ↦ i < as.length) L.reverse i)).getD default
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)
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 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)
Tactic: simp only [Function.update_of_ne 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)
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')
        (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
have 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
Tactic: cases L.reverse[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 : ℕ
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
⊢ 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
have 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
Tactic: cases L.reverse[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)
⊢ 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))) }
have 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)))
Tactic: congr
-- 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)
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)))
⊢ 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))) }
have 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' := sorry : 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)))
Tactic: congr
-- 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)
⊢ 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)))
have 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)) [])))
Tactic: cases L.reverse
-- 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)
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)) [])))
⊢ 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)))
have 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))))
Tactic: cases L.reverse
-- 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)
⊢ 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)))
have 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))) []))
  (List.map (PointedMap.f { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) })
    (List.tail (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) [])))
Tactic: cases L.reverse
-- 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)
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))) []))
    (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)) [])))
⊢ 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)))
have e_Tape₁ : ∀ (head : Γ k) (tail : List (Γ k)),
  Eq (α := List (Γ' K Γ))
    (List.tail
      (List.map (fun (a : Γ k) ↦ (false, update (β := fun (k : K) ↦ Option (Γ k)) (fun (x : K) ↦ none) k (some a)))
        (head :: tail)))
    (List.map (PointedMap.f { f := Prod.mk false, map_pt' := sorry : PointedMap ((k : K) → Option (Γ k)) (Γ' K Γ) })
      (List.tail
        (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) (head :: tail))))
Tactic: cases L.reverse
-- 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)
head : Γ k
tail : List (Γ k)
⊢ Eq (α := List (Γ' K Γ))
    (List.tail
      (List.map (fun (a : Γ k) ↦ (false, update (β := fun (k : K) ↦ Option (Γ k)) (fun (x : K) ↦ none) k (some a)))
        (head :: tail)))
    (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)) (head :: tail))))
have e_Tape : Eq (α := List (Γ' K Γ))
  (List.map (fun (a : Γ k) ↦ (false, update (β := fun (k : K) ↦ Option (Γ k)) (fun (x : K) ↦ none) k (some a))) tail)
  (List.map (Prod.mk false ∘ fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) tail)
Tactic: simp only [List.map_map, List.tail_cons, List.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
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
L₁ : ListBlank (Γ' K Γ)
L₂ : List (Γ k)
H₁ : Membership.mem (γ := Part (ListBlank (Γ' K Γ))) (TM1.eval (tr (Γ := Γ) M) (trInit (Γ := Γ) k L)) L₁
H₂ : L₂ ∈ TM2.eval (Γ := Γ) M k L
⊢ ∃ (S : (k : K) → List (Γ k)) (L' : ListBlank ((k : K) → Option (Γ k))),
    addBottom (Γ := Γ) L' = L₁ ∧
      (∀ (k : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
        S k = L₂
have obtain : ∀ (c₁ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ)
  (h₁ :
    Membership.mem (γ := Part (TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ))
      (eval (TM1.step (tr (Γ := Γ) M)) (TM1.init (trInit (Γ := Γ) k L))) c₁)
  (H₁ :
    Membership.mem (γ := Part (ListBlank (Γ' K Γ))) (TM1.eval (tr (Γ := Γ) M) (trInit (Γ := Γ) k L)) c₁.Tape.right₀),
  ∃ (S : (k : K) → List (Γ k)) (L' : ListBlank ((k : K) → Option (Γ k))),
    addBottom (Γ := Γ) L' = c₁.Tape.right₀ ∧
      (∀ (k : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
        S k = L₂
Tactic: obtain ⟨c₁, h₁, rfl⟩ := (Part.mem_map_iff _).1 H₁
Cleared hypotheses: L₁, 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
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L L₂ : List (Γ k)
H₂ : L₂ ∈ TM2.eval (Γ := Γ) M k L
c₁ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h₁ :
  Membership.mem (γ := Part (TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ))
    (eval (TM1.step (tr (Γ := Γ) M)) (TM1.init (trInit (Γ := Γ) k L))) c₁
H₁ : Membership.mem (γ := Part (ListBlank (Γ' K Γ))) (TM1.eval (tr (Γ := Γ) M) (trInit (Γ := Γ) k L)) c₁.Tape.right₀
⊢ ∃ (S : (k : K) → List (Γ k)) (L' : ListBlank ((k : K) → Option (Γ k))),
    addBottom (Γ := Γ) L' = c₁.Tape.right₀ ∧
      (∀ (k : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
        S k = L₂
have obtain : ∀ (c₂ : TM2.Cfg Γ Λ σ) (h₂ : c₂ ∈ eval (TM2.step (Γ := Γ) M) (TM2.init (Γ := Γ) k L))
  (H₂ : c₂.stk (Γ := Γ) k ∈ TM2.eval (Γ := Γ) M k L),
  ∃ (S : (k : K) → List (Γ k)) (L' : ListBlank ((k : K) → Option (Γ k))),
    addBottom (Γ := Γ) L' = c₁.Tape.right₀ ∧
      (∀ (k : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
        S k = c₂.stk (Γ := Γ) k
Tactic: obtain ⟨c₂, h₂, rfl⟩ := (Part.mem_map_iff _).1 H₂
Cleared hypotheses: L₂, 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
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
c₁ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h₁ :
  Membership.mem (γ := Part (TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ))
    (eval (TM1.step (tr (Γ := Γ) M)) (TM1.init (trInit (Γ := Γ) k L))) c₁
H₁ : Membership.mem (γ := Part (ListBlank (Γ' K Γ))) (TM1.eval (tr (Γ := Γ) M) (trInit (Γ := Γ) k L)) c₁.Tape.right₀
c₂ : TM2.Cfg Γ Λ σ
h₂ : c₂ ∈ eval (TM2.step (Γ := Γ) M) (TM2.init (Γ := Γ) k L)
H₂ : c₂.stk (Γ := Γ) k ∈ TM2.eval (Γ := Γ) M k L
⊢ ∃ (S : (k : K) → List (Γ k)) (L' : ListBlank ((k : K) → Option (Γ k))),
    addBottom (Γ := Γ) L' = c₁.Tape.right₀ ∧
      (∀ (k : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
        S k = c₂.stk (Γ := Γ) k
have obtain : ∀ {q : Option Λ} {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)
  (h₂ : TM2.Cfg.mk (Γ := Γ) q v S ∈ eval (TM2.step (Γ := Γ) M) (TM2.init (Γ := Γ) k L))
  (H₂ : (TM2.Cfg.mk (Γ := Γ) q v S).stk (Γ := Γ) k ∈ TM2.eval (Γ := Γ) M k L)
  (h₃ :
    Membership.mem (γ := Part (TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ))
      (eval (TM1.step (tr (Γ := Γ) M)) (TM1.init (trInit (Γ := Γ) k L)))
      { l := Option.map (normal (Γ := Γ)) q, var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L') }),
  ∃ (S_1 : (k : K) → List (Γ k)) (L' : ListBlank ((k : K) → Option (Γ k))),
    addBottom (Γ := Γ) L' = c₁.Tape.right₀ ∧
      (∀ (k : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L' = ListBlank.mk (List.map some (S_1 k)).reverse) ∧
        S_1 k = (TM2.Cfg.mk (Γ := Γ) q v S).stk (Γ := Γ) k
Tactic: obtain ⟨_, ⟨L', hT⟩, h₃⟩ := StateTransition.tr_eval (tr_respects M) (trCfg_init k L) h₂
Cleared hypotheses: c₂, h₂, H₂