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 Γ Λ σ
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') }
⊢ ∃ (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
have 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
Tactic: cases Part.mem_unique h₁ h₃
Cleared hypotheses: c₁, h₁, 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 Λ
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')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have rcases : ∀ (l : Λ) (lS : l ∈ S) (h : l' ∈ insert (normal (Γ := Γ) l) (trStmts₁ (Γ := Γ) (M l))),
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: rcases Finset.mem_biUnion.1 h with ⟨l, lS, h⟩
-- 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 Γ Λ σ
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) (tr (Γ := Γ) M l')
have this₁ : 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⟩
-- 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 Λ
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')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have 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))
Tactic: rcases Finset.mem_insert.1 h with (rfl | h)
Cleared hypotheses: l', h_1, 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 Λ
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))
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have inr : ∀ (h : l' ∈ trStmts₁ (Γ := Γ) (M l)), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: rcases Finset.mem_insert.1 h with (rfl | 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 Λ
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')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have 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))
Tactic: rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ h]
Cleared hypotheses: l', h_1, 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 Λ
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))
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have inr : ∀ (h : l' ∈ trStmts₁ (Γ := Γ) (M l)), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ 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 Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
l' : Λ' K Γ Λ σ
h : l' ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have suffices : ∀ (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')
Tactic: suffices ∀ (q) (_ : 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') by
      rcases Finset.mem_biUnion.1 h with ⟨l, lS, h⟩
      have :=
        this _ (ss.2 l lS) fun x hx ↦ Finset.mem_biUnion.2 ⟨_, lS, Finset.mem_insert_of_mem hx⟩
      rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ 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 Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
⊢ ∀ (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')
have refine_1 : ∀ (k : K) (s : StAct K Γ σ k) (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')) →
    TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q) →
      (∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: refine stmtStRec ?_ ?_ ?_ ?_ ?_
-- 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 Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
refine_1 :
  ∀ (k : K) (s : StAct K Γ σ k) (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')) →
      TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q) →
        (∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ ∀ (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')
have refine_2 : ∀ (a : σ → σ) (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')) →
    TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.load (Γ := Γ) a q) →
      (∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q), x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q),
            TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: refine stmtStRec ?_ ?_ ?_ ?_ ?_
-- 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 Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
refine_1 :
  ∀ (k : K) (s : StAct K Γ σ k) (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')) →
      TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q) →
        (∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
refine_2 :
  ∀ (a : σ → σ) (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')) →
      TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.load (Γ := Γ) a q) →
        (∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q), x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q),
              TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ ∀ (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')
have refine_3 : ∀ (p : σ → Bool) (q₁ 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')) →
    (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')) →
      TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.branch (Γ := Γ) p q₁ q₂) →
        (∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂), x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂),
              TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: refine stmtStRec ?_ ?_ ?_ ?_ ?_
-- 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 Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  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')
ss' : TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have ss'₁ : TM2.SupportsStmt (Γ := Γ) S q
Tactic: rw [TM2to1.supports_run] at ss'
Cleared hypotheses: ss', sub
-- 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 Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  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')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub : ∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have sub₁ : ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
Tactic: simp only [TM2to1.trStmts₁_run, Finset.mem_union, Finset.mem_insert, Finset.mem_singleton]
        at sub
Cleared hypotheses: sub
-- 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 Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  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')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
Tactic: have hgo := sub _ (Or.inl <| Or.inl rfl)
-- 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 Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  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')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
Tactic: have hret := sub _ (Or.inl <| Or.inr rfl)
-- 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 Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  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')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
Tactic: obtain ⟨IH₁, IH₂⟩ := IH ss' fun x hx ↦ sub x <| Or.inr hx
-- 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 Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
IH :
  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')
ss' : TM2.SupportsStmt (Γ := Γ) S q
sub :
  ∀ (x : Λ' K Γ Λ σ), (x = go (Γ := Γ) k s q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q → x ∈ trSupp (Γ := Γ) M S
hgo : go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
hret : ret (Γ := Γ) q ∈ trSupp (Γ := Γ) M S
IH₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q)
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: obtain ⟨IH₁, IH₂⟩ := IH ss' fun x hx ↦ sub x <| Or.inr hx