awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K),
        ListBlank.map (proj (Γ := fun (i : K) ↦ Option (Γ i)) k) T = 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 (Γ := Γ) T))) b
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ)
        (TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) o)
          (update (β := fun (k : K) ↦ List (Γ k)) S k (stWrite (Γ := Γ) v (S k) o)))
        b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k o q) v (Tape.mk' ∅ (addBottom (Γ := Γ) T))) b
have hgo : Reaches₀ (TM1.step (tr (Γ := Γ) M))
  { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) T) :
    TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
  { l := some (go (Γ := Γ) k o q), var := v,
    Tape := (Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) T)) }
Tactic: have hgo := tr_respects_aux₁ M o q v (hT k) _ le_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
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K),
        ListBlank.map (proj (Γ := fun (i : K) ↦ Option (Γ i)) k) T = 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 (Γ := Γ) T))) b
hgo :
  Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) T) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (go (Γ := Γ) k o q), var := v,
      Tape := (Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) T)) }
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ)
        (TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) o)
          (update (β := fun (k : K) ↦ List (Γ k)) S k (stWrite (Γ := Γ) v (S k) o)))
        b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k o q) v (Tape.mk' ∅ (addBottom (Γ := Γ) T))) b
have obtain : ∀ (T' : ListBlank ((k : K) → Option (Γ k)))
  (hT' :
    ∀ (k_1 : K),
      ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) T' =
        ListBlank.mk
          (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) o) k_1)).reverse)
  (hrun :
    Eq (α := TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ)
      (TM1.stepAux (trStAct (Γ := Γ) (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) o) v
        ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) T))))
      (TM1.stepAux (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) (stVar (Γ := Γ) v (S k) o)
        ((Tape.move Dir.right)^[(update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) o) k).length]
          (Tape.mk' ∅ (addBottom (Γ := Γ) T'))))),
  ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ)
        (TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) o)
          (update (β := fun (k : K) ↦ List (Γ k)) S k (stWrite (Γ := Γ) v (S k) o)))
        b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k o q) v (Tape.mk' ∅ (addBottom (Γ := Γ) T))) b
Tactic: obtain ⟨T', hT', hrun⟩ := tr_respects_aux₂ (Λ := Λ) hT o
-- 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
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K),
        ListBlank.map (proj (Γ := fun (i : K) ↦ Option (Γ i)) k) T = 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 (Γ := Γ) T))) b
hgo :
  Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) T) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (go (Γ := Γ) k o q), var := v,
      Tape := (Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) T)) }
T' : ListBlank ((k : K) → Option (Γ k))
hT' :
  ∀ (k_1 : K),
    ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) T' =
      ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) o) k_1)).reverse
hrun :
  Eq (α := TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ)
    (TM1.stepAux (trStAct (Γ := Γ) (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) o) v
      ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) T))))
    (TM1.stepAux (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) (stVar (Γ := Γ) v (S k) o)
      ((Tape.move Dir.right)^[(update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) o) k).length]
        (Tape.mk' ∅ (addBottom (Γ := Γ) T'))))
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ)
        (TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) o)
          (update (β := fun (k : K) ↦ List (Γ k)) S k (stWrite (Γ := Γ) v (S k) o)))
        b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k o q) v (Tape.mk' ∅ (addBottom (Γ := Γ) T))) b
have this : Reaches₁ (TM1.step (tr (Γ := Γ) M))
  { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) T) :
    TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
  (TM1.stepAux (tr (Γ := Γ) M (go (Γ := Γ) k o q)) v
    ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) T))))
Tactic: have := hgo.tail' 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
M : Λ → TM2.Stmt Γ Λ σ
c₁ : TM2.Cfg Γ Λ σ
c₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h : TrCfg (Γ := Γ) c₁ c₂
⊢ match (motive := Option (TM2.Cfg Γ Λ σ) → Prop) TM2.step (Γ := Γ) M c₁ with
  | some b₁ =>
    ∃ (b₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ), TrCfg (Γ := Γ) b₁ b₂ ∧ Reaches₁ (TM1.step (tr (Γ := Γ) M)) c₂ b₂
  | none => TM1.step (tr (Γ := Γ) M) c₂ = none
have none : ∀ {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),
  match (motive := Option (TM2.Cfg Γ Λ σ) → Prop) TM2.step (Γ := Γ) M (TM2.Cfg.mk (Γ := Γ) none v S) with
  | some b₁ =>
    ∃ (b₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) b₁ b₂ ∧
        Reaches₁ (TM1.step (tr (Γ := Γ) M))
          { l := Option.map (normal (Γ := Γ)) none, var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) } b₂
  | none =>
    TM1.step (tr (Γ := Γ) M)
        { l := Option.map (normal (Γ := Γ)) none, var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } =
      none
Tactic: obtain @⟨- | l, v, S, L, hT⟩ := h
Cleared hypotheses: c₁, c₂, 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 Γ Λ σ
c₁ : TM2.Cfg Γ Λ σ
c₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h : TrCfg (Γ := Γ) c₁ c₂
none :
  ∀ {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),
    match (motive := Option (TM2.Cfg Γ Λ σ) → Prop) TM2.step (Γ := Γ) M (TM2.Cfg.mk (Γ := Γ) Option.none v S) with
    | some b₁ =>
      ∃ (b₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
        TrCfg (Γ := Γ) b₁ b₂ ∧
          Reaches₁ (TM1.step (tr (Γ := Γ) M))
            { l := Option.map (normal (Γ := Γ)) Option.none, var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) } b₂
    | Option.none =>
      TM1.step (tr (Γ := Γ) M)
          { l := Option.map (normal (Γ := Γ)) Option.none, var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
            TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } =
        Option.none
⊢ match (motive := Option (TM2.Cfg Γ Λ σ) → Prop) TM2.step (Γ := Γ) M c₁ with
  | some b₁ =>
    ∃ (b₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ), TrCfg (Γ := Γ) b₁ b₂ ∧ Reaches₁ (TM1.step (tr (Γ := Γ) M)) c₂ b₂
  | Option.none => TM1.step (tr (Γ := Γ) M) c₂ = Option.none
have some : ∀ {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 : Λ),
  match (motive := Option (TM2.Cfg Γ Λ σ) → Prop) TM2.step (Γ := Γ) M (TM2.Cfg.mk (Γ := Γ) (some l) v S) with
  | some b₁ =>
    ∃ (b₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) b₁ b₂ ∧
        Reaches₁ (TM1.step (tr (Γ := Γ) M))
          { l := Option.map (normal (Γ := Γ)) (some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) } b₂
  | Option.none =>
    TM1.step (tr (Γ := Γ) M)
        { l := Option.map (normal (Γ := Γ)) (some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } =
      Option.none
Tactic: obtain @⟨- | l, v, S, L, hT⟩ := h
Cleared hypotheses: c₁, c₂, 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 Γ Λ σ
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 : Λ
⊢ match (motive := Option (TM2.Cfg Γ Λ σ) → Prop) TM2.step (Γ := Γ) M (TM2.Cfg.mk (Γ := Γ) (some l) v S) with
  | some b₁ =>
    ∃ (b₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) b₁ b₂ ∧
        Reaches₁ (TM1.step (tr (Γ := Γ) M))
          { l := Option.map (normal (Γ := Γ)) (some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) } b₂
  | none =>
    TM1.step (tr (Γ := Γ) M)
        { l := Option.map (normal (Γ := Γ)) (some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } =
      none
have some : ∀ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ) (c : TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (M l) v S) b)
  (r :
    Reaches (TM1.step (tr (Γ := Γ) M))
      (TM1.stepAux (tr (Γ := Γ) M (normal (Γ := Γ) l)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b),
  match (motive := Option (TM2.Cfg Γ Λ σ) → Prop) TM2.step (Γ := Γ) M (TM2.Cfg.mk (Γ := Γ) (some l) v S) with
  | some b₁ =>
    ∃ (b₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) b₁ b₂ ∧
        Reaches₁ (TM1.step (tr (Γ := Γ) M))
          { l := Option.map (normal (Γ := Γ)) (some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) } b₂
  | none =>
    TM1.step (tr (Γ := Γ) M)
        { l := Option.map (normal (Γ := Γ)) (some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } =
      none
Tactic: rsuffices ⟨b, c, r⟩ : ∃ b, _ ∧ Reaches (TM1.step (tr M)) _ _
-- 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 Option.some (S k)).reverse
l : Λ
some :
  ∀ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ) (c : TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (M l) v S) b)
    (r :
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (tr (Γ := Γ) M (normal (Γ := Γ) l)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b),
    match (motive := Option (TM2.Cfg Γ Λ σ) → Prop) TM2.step (Γ := Γ) M (TM2.Cfg.mk (Γ := Γ) (Option.some l) v S) with
    | Option.some b₁ =>
      ∃ (b₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
        TrCfg (Γ := Γ) b₁ b₂ ∧
          Reaches₁ (TM1.step (tr (Γ := Γ) M))
            { l := Option.map (normal (Γ := Γ)) (Option.some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) }
            b₂
    | none =>
      TM1.step (tr (Γ := Γ) M)
          { l := Option.map (normal (Γ := Γ)) (Option.some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
            TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } =
        none
⊢ match (motive := Option (TM2.Cfg Γ Λ σ) → Prop) TM2.step (Γ := Γ) M (TM2.Cfg.mk (Γ := Γ) (Option.some l) v S) with
  | Option.some b₁ =>
    ∃ (b₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) b₁ b₂ ∧
        Reaches₁ (TM1.step (tr (Γ := Γ) M))
          { l := Option.map (normal (Γ := Γ)) (Option.some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) } b₂
  | none =>
    TM1.step (tr (Γ := Γ) M)
        { l := Option.map (normal (Γ := Γ)) (Option.some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } =
      none
have rsuffices : ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
  TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (M l) v S) b ∧
    Reaches (TM1.step (tr (Γ := Γ) M))
      (TM1.stepAux (tr (Γ := Γ) M (normal (Γ := Γ) l)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
Tactic: rsuffices ⟨b, c, r⟩ : ∃ b, _ ∧ Reaches (TM1.step (tr M)) _ _
-- 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 : Λ
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (M l) v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) (M l)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
have generalize : ∀ (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
Tactic: generalize M l = 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
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
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂) v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (trNormal (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
have branch : ∃ (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 (fun (x : Γ' K Γ) ↦ p) (Tape.mk' ∅ (addBottom (Γ := Γ) L)).head v then
        TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))
      else TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
      b
Tactic: unfold TM2.stepAux trNormal TM1.stepAux
-- 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
⊢ ∃ (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 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
Tactic: cases p v
-- 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
-- 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
⊢ ∃ (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 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
Tactic: cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]