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 Λ
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)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q))
have simp : ∀ (a : Γ' K Γ) (v : σ), go (Γ := Γ) k s q ∈ trSupp (Γ := Γ) M S
Tactic: simp only [trNormal_run, TM1.SupportsStmt]
-- 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
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)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have refine_1 : ∀ (l : Λ' K Γ Λ σ) (h : l ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q)),
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
Tactic: refine ⟨by simp only [trNormal_run, TM1.SupportsStmt]; intros; exact hgo, fun l 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
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)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q)
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
have h₁ : l ∈ {go (Γ := Γ) k s q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
Tactic: rw [trStmts₁_run] at h
Cleared hypotheses: 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
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)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : l ∈ {go (Γ := Γ) k s q, ret (Γ := Γ) q} ∪ trStmts₁ (Γ := Γ) q
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
have h₁ : (l = go (Γ := Γ) k s q ∨ l = ret (Γ := Γ) q) ∨ l ∈ trStmts₁ (Γ := Γ) q
Tactic: simp only [Finset.mem_union, Finset.mem_insert, Finset.mem_singleton]
        at h
Cleared hypotheses: 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
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)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : (l = go (Γ := Γ) k s q ∨ l = ret (Γ := Γ) q) ∨ l ∈ trStmts₁ (Γ := Γ) q
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
have refine_1 : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k s q))
Tactic: rcases h with (⟨rfl | rfl⟩ | 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 Λ
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)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : (l = go (Γ := Γ) k s q ∨ l = ret (Γ := Γ) q) ∨ l ∈ trStmts₁ (Γ := Γ) q
refine_1 : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k s q))
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
have refine_1₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (ret (Γ := Γ) q))
Tactic: rcases h with (⟨rfl | rfl⟩ | 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 Λ
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)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : (l = go (Γ := Γ) k s q ∨ l = ret (Γ := Γ) q) ∨ l ∈ trStmts₁ (Γ := Γ) q
refine_1 : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k s q))
refine_1₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (ret (Γ := Γ) q))
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
have refine_1₂ : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
Tactic: rcases h with (⟨rfl | rfl⟩ | h)
Cleared hypotheses: 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
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)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k s q))
have refine_1 : ∀ (a : σ → Γ k)
  (sub :
    ∀ (x : Λ' K Γ Λ σ),
      (x = go (Γ := Γ) k (StAct.push (Γ := Γ) a) q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q →
        x ∈ trSupp (Γ := Γ) M S)
  (hgo : go (Γ := Γ) k (StAct.push (Γ := Γ) a) q ∈ trSupp (Γ := Γ) M S),
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k (StAct.push (Γ := Γ) a) q))
Tactic: cases s
Cleared hypotheses: s, sub, hgo
-- 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
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)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
refine_1 :
  ∀ (a : σ → Γ k)
    (sub :
      ∀ (x : Λ' K Γ Λ σ),
        (x = go (Γ := Γ) k (StAct.push (Γ := Γ) a) q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q →
          x ∈ trSupp (Γ := Γ) M S)
    (hgo : go (Γ := Γ) k (StAct.push (Γ := Γ) a) q ∈ trSupp (Γ := Γ) M S),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k (StAct.push (Γ := Γ) a) q))
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k s q))
have refine_1₁ : ∀ (a : σ → Option (Γ k) → σ)
  (sub :
    ∀ (x : Λ' K Γ Λ σ),
      (x = go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q →
        x ∈ trSupp (Γ := Γ) M S)
  (hgo : go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q ∈ trSupp (Γ := Γ) M S),
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q))
Tactic: cases s
Cleared hypotheses: s, sub, hgo
-- 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
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)
IH₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
refine_1 :
  ∀ (a : σ → Γ k)
    (sub :
      ∀ (x : Λ' K Γ Λ σ),
        (x = go (Γ := Γ) k (StAct.push (Γ := Γ) a) q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q →
          x ∈ trSupp (Γ := Γ) M S)
    (hgo : go (Γ := Γ) k (StAct.push (Γ := Γ) a) q ∈ trSupp (Γ := Γ) M S),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k (StAct.push (Γ := Γ) a) q))
refine_1₁ :
  ∀ (a : σ → Option (Γ k) → σ)
    (sub :
      ∀ (x : Λ' K Γ Λ σ),
        (x = go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q →
          x ∈ trSupp (Γ := Γ) M S)
    (hgo : go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q ∈ trSupp (Γ := Γ) M S),
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k (StAct.peek (Γ := Γ) a) q))
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k s q))
have refine_1₂ : ∀ (a : σ → Option (Γ k) → σ)
  (sub :
    ∀ (x : Λ' K Γ Λ σ),
      (x = go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q ∨ x = ret (Γ := Γ) q) ∨ x ∈ trStmts₁ (Γ := Γ) q →
        x ∈ trSupp (Γ := Γ) M S)
  (hgo : go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q ∈ trSupp (Γ := Γ) M S),
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M (go (Γ := Γ) k (StAct.pop (Γ := Γ) a) q))
Tactic: cases s
Cleared hypotheses: s, sub, hgo
-- 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
a : σ → σ
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 (TM2.Stmt.load (Γ := Γ) a q)
sub : ∀ 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')
have refine_2 : ∀ (sub : ∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S),
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: unfold TM2to1.trStmts₁ 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
p : σ → Bool
q₁ 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')
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 (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ 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')
have sub₁ : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S
Tactic: unfold TM2to1.trStmts₁ 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
p : σ → Bool
q₁ 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')
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 (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) 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')
have IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
Tactic: obtain ⟨IH₁₁, IH₁₂⟩ := IH₁ ss'.1 fun x hx ↦ sub x <| Finset.mem_union_left _ 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
p : σ → Bool
q₁ 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')
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 (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
⊢ 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')
have IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: obtain ⟨IH₁₁, IH₁₂⟩ := IH₁ ss'.1 fun x hx ↦ sub x <| Finset.mem_union_left _ 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
p : σ → Bool
q₁ 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')
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 (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ 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')
have IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
Tactic: obtain ⟨IH₂₁, IH₂₂⟩ := IH₂ ss'.2 fun x hx ↦ sub x <| Finset.mem_union_right _ 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
p : σ → Bool
q₁ 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')
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 (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
⊢ 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')
have IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: obtain ⟨IH₂₁, IH₂₂⟩ := IH₂ ss'.2 fun x hx ↦ sub x <| Finset.mem_union_right _ hx