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)
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)) [])))
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' := ⋯ : 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))))
⊢ 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)))

Tactic:
cases L.reverse

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)
⊢ 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:
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)
⊢ 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:
try 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)
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:
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)
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:
try 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)
⊢ 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)) [])))

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)
⊢ 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)) [])))

Tactic:
try 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)
head : Γ k
tail : List (Γ k)
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)
⊢ 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))))

Tactic:
simp only [List.map_map, List.tail_cons, List.map]

Premises used: List.map, List.map_map, List.tail_cons
-- 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)
head : Γ k
tail : List (Γ k)
⊢ 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:
rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
⊢ Part.Dom (α := ListBlank (Γ' K Γ)) (TM1.eval (tr (Γ := Γ) M) (trInit (Γ := Γ) k L)) ↔ (TM2.eval (Γ := Γ) M k L).Dom

Tactic:
StateTransition.tr_eval_dom (tr_respects M) (trCfg_init k L)

Premises used: StateTransition.tr_eval_dom, Turing.TM2to1.trCfg_init, Turing.TM2to1.tr_respects
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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
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₂
⊢ ∃ (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₂

Tactic:
obtain ⟨c₁, h₁, rfl⟩ := (Part.mem_map_iff _).1 H₁

Premises used: Iff.mp, Part.mem_map_iff, rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₀
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
⊢ ∃ (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₂

Premises used: Iff.mp, Part.mem_map_iff, rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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
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
⊢ ∃ (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 ⟨_, ⟨L', hT⟩, h₃⟩ := StateTransition.tr_eval (tr_respects M) (trCfg_init k L) h₂

Premises used: StateTransition.tr_eval, Turing.TM2to1.trCfg_init, Turing.TM2to1.tr_respects
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₀
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') }
refl :
  ∀
    (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') })
    (H₁ :
      Membership.mem (γ := Part (ListBlank (Γ' K Γ))) (TM1.eval (tr (Γ := Γ) M) (trInit (Γ := Γ) k L))
        (TM1.Cfg.Tape (Λ := Λ' K Γ Λ σ)
            { l := Option.map (normal (Γ := Γ)) q, var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L') :
              TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }).right₀),
    ∃ (S_1 : (k : K) → List (Γ k)) (L'_1 : ListBlank ((k : K) → Option (Γ k))),
      addBottom (Γ := Γ) L'_1 =
          (TM1.Cfg.Tape (Λ := Λ' K Γ Λ σ)
              { l := Option.map (normal (Γ := Γ)) q, var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L') }).right₀ ∧
        (∀ (k : K),
            ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L'_1 =
              ListBlank.mk (List.map some (S_1 k)).reverse) ∧
          S_1 k = (TM2.Cfg.mk (Γ := Γ) q v S).stk (Γ := Γ) k
⊢ ∃ (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:
cases Part.mem_unique h₁ h₃

Premises used: Part.mem_unique
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
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') }
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') }
H₁ :
  Membership.mem (γ := Part (ListBlank (Γ' K Γ))) (TM1.eval (tr (Γ := Γ) M) (trInit (Γ := Γ) k L))
    (TM1.Cfg.Tape (Λ := Λ' K Γ Λ σ)
        { l := Option.map (normal (Γ := Γ)) q, var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L') :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }).right₀
⊢ addBottom (Γ := Γ) L' =
    (TM1.Cfg.Tape (Λ := Λ' K Γ Λ σ)
        { l := Option.map (normal (Γ := Γ)) q, var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L') }).right₀

Tactic:
simp only [Tape.mk'_right₀]

Premises used: Turing.Tape.mk'_right₀
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
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') }
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') }
H₁ :
  Membership.mem (γ := Part (ListBlank (Γ' K Γ))) (TM1.eval (tr (Γ := Γ) M) (trInit (Γ := Γ) k L))
    (TM1.Cfg.Tape (Λ := Λ' K Γ Λ σ)
        { l := Option.map (normal (Γ := Γ)) q, var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L') :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }).right₀
⊢ ∃ (S_1 : (k : K) → List (Γ k)) (L'_1 : ListBlank ((k : K) → Option (Γ k))),
    addBottom (Γ := Γ) L'_1 =
        (TM1.Cfg.Tape (Λ := Λ' K Γ Λ σ)
            { l := Option.map (normal (Γ := Γ)) q, var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L') }).right₀ ∧
      (∀ (k : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L'_1 =
            ListBlank.mk (List.map some (S_1 k)).reverse) ∧
        S_1 k = (TM2.Cfg.mk (Γ := Γ) q v S).stk (Γ := Γ) k

Tactic:
exact ⟨_, L', by simp only [Tape.mk'_right₀], hT, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
l' : Λ' K Γ Λ σ
h : l' ∈ trSupp (Γ := Γ) M S
this :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt (Γ := Γ) S q →
      (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
rcases :
  ∀ (l : Λ) (lS : l ∈ S) (h : l' ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
rcases Finset.mem_biUnion.1 h with ⟨l, lS, h⟩

Premises used: Iff.mp, Finset.mem_biUnion
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
l' : Λ' K Γ Λ σ
h_1 : l' ∈ trSupp (Γ := Γ) M S
this :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt (Γ := Γ) S q →
      (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ
lS : l ∈ S
h : l' ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (M l)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (M l), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
have :=
        this _ (ss.2 l lS) fun x hx ↦ Finset.mem_biUnion.2 ⟨_, lS, Finset.mem_insert_of_mem hx⟩
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
l' : Λ' K Γ Λ σ
h_1 : l' ∈ trSupp (Γ := Γ) M S
this_1 :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt (Γ := Γ) S q →
      (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ
lS : l ∈ S
h : l' ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))
this :
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (M l)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (M l), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
inl :
  ∀ (h : normal (Γ := Γ) l ∈ trSupp (Γ := Γ) M S)
    (h : normal (Γ := Γ) l ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (normal (Γ := Γ) l))
inr : ∀ (h : l' ∈ trStmts₁ (Γ := Γ) (M l)), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
rcases Finset.mem_insert.1 h with (rfl | h)

Premises used: Finset.mem_insert, Iff.mp, rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
this_1 :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt (Γ := Γ) S q →
      (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ
lS : l ∈ S
this :
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (M l)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (M l), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
h_1 : normal (Γ := Γ) l ∈ trSupp (Γ := Γ) M S
h : normal (Γ := Γ) l ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (normal (Γ := Γ) l))

Tactic:
this.1

Premises used: And.left, Turing.TM2to1.tr
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
this_1 :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt (Γ := Γ) S q →
      (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ
lS : l ∈ S
this :
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (M l)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (M l), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
h_1 : normal (Γ := Γ) l ∈ trSupp (Γ := Γ) M S
h : normal (Γ := Γ) l ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (normal (Γ := Γ) l))

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
l' : Λ' K Γ Λ σ
h_1 : l' ∈ trSupp (Γ := Γ) M S
this_1 :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt (Γ := Γ) S q →
      (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ
lS : l ∈ S
h_2 : l' ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))
this :
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (M l)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (M l), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
h : l' ∈ trStmts₁ (Γ := Γ) (M l)
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
this.2 _ h

Premises used: And.right