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
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
branch :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₁_1), q₀ ∈ stmts₁ (Γ := Γ) q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂)
    (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂)), q₀ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂)
branch₁ :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₁_1), q₀ ∈ stmts₁ (Γ := Γ) q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂)
    (h₁₂ : q₁ = Stmt.branch (Γ := Γ) f q₁_1 q₂ ∨ q₁ ∈ stmts₁ (Γ := Γ) q₁_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) q₂),
    q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁_1 q₂) (stmts₁ (Γ := Γ) q₁_1 ∪ stmts₁ (Γ := Γ) q₂)
goto :
  ∀ (l : σ → Λ) (h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) l)) q₁),
    Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) l)) q₀
goto₁ :
  ∀ (l : σ → Λ) (h₁₂ : q₁ = Stmt.goto (Γ := Γ) l), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.goto (Γ := Γ) l} q₀
halt :
  ∀ (h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.halt (Γ := Γ))) q₁),
    Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.halt (Γ := Γ))) q₀
halt₁ : ∀ (h₁₂ : q₁ = Stmt.halt (Γ := Γ)), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.halt (Γ := Γ)} q₀
load :
  ∀ (a : σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
    (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.load (Γ := Γ) a q)), q₀ ∈ stmts₁ (Γ := Γ) (Stmt.load (Γ := Γ) a q)
load₁ :
  ∀ (a : σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
    (h₁₂ : q₁ = Stmt.load (Γ := Γ) a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q),
    q₀ ∈ insert (Stmt.load (Γ := Γ) a q) (stmts₁ (Γ := Γ) q)
push :
  ∀ (k : K) (a : σ → Γ k) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
    (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a q)), q₀ ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a q)
⊢ q₀ ∈ stmts₁ (Γ := Γ) q₂
have push₁ : ∀ (k : K) (a : σ → Γ k) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
  (h₁₂ : q₁ = Stmt.push (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q),
  q₀ ∈ insert (Stmt.push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
Tactic: induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] at h₁₂)
  | branch f q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · exact Finset.mem_insert_of_mem (Finset.mem_union_left _ (IH₁ h₁₂))
    · exact Finset.mem_insert_of_mem (Finset.mem_union_right _ (IH₂ h₁₂))
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | load _ q IH | _ _ _ q IH =>
    rcases h₁₂ with (rfl | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · exact Finset.mem_insert_of_mem (IH h₁₂)
Cleared hypotheses: q₂, 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
q₁ q₂ : Stmt Γ Λ σ
intro : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₂), stmts₁ (Γ := Γ) q₁ ⊆ stmts₁ (Γ := Γ) q₂
⊢ q₁ ∈ stmts₁ (Γ := Γ) q₂ → stmts₁ (Γ := Γ) q₁ ⊆ stmts₁ (Γ := Γ) q₂
have intro₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₂) ⦃q₀ : Stmt Γ Λ σ⦄, q₀ ∈ stmts₁ (Γ := Γ) q₁ → q₀ ∈ stmts₁ (Γ := Γ) q₂
Tactic: classical
  intro h₁₂ q₀ h₀₁
  induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] at h₁₂)
  | branch f q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · exact Finset.mem_insert_of_mem (Finset.mem_union_left _ (IH₁ h₁₂))
    · exact Finset.mem_insert_of_mem (Finset.mem_union_right _ (IH₂ h₁₂))
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | load _ q IH | _ _ _ q IH =>
    rcases h₁₂ with (rfl | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · exact Finset.mem_insert_of_mem (IH 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
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₁) (hs : SupportsStmt (Γ := Γ) S q₁), SupportsStmt (Γ := Γ) S q₁_1
IH₂ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁_1
h : q₁_1 ∈ stmts₁ (Γ := Γ) (branch (Γ := Γ) f q₁ q₂)
hs : SupportsStmt (Γ := Γ) S (branch (Γ := Γ) f q₁ q₂)
⊢ SupportsStmt (Γ := Γ) S q₁_1
have h₁ : q₁_1 = branch (Γ := Γ) f q₁ q₂ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₁ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₂
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
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
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₁) (hs : SupportsStmt (Γ := Γ) S q₁), SupportsStmt (Γ := Γ) S q₁_1
IH₂ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁_1
hs : SupportsStmt (Γ := Γ) S q₁ ∧ SupportsStmt (Γ := Γ) S q₂
h : q₁_1 = branch (Γ := Γ) f q₁ q₂ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₁ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₂
⊢ SupportsStmt (Γ := Γ) S q₁_1
have branch : ∀
  (IH₁ :
    ∀ (h : branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₁) (hs : SupportsStmt (Γ := Γ) S q₁),
      SupportsStmt (Γ := Γ) S (branch (Γ := Γ) f q₁ q₂))
  (IH₂ :
    ∀ (h : branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂),
      SupportsStmt (Γ := Γ) S (branch (Γ := Γ) f q₁ q₂)),
  SupportsStmt (Γ := Γ) S (branch (Γ := Γ) f q₁ q₂)
Tactic: rcases h with (rfl | h | h)
Cleared hypotheses: q₁_1, IH₁, IH₂, 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
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₁) (hs : SupportsStmt (Γ := Γ) S q₁), SupportsStmt (Γ := Γ) S q₁_1
IH₂ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁_1
hs : SupportsStmt (Γ := Γ) S q₁ ∧ SupportsStmt (Γ := Γ) S q₂
h : q₁_1 = Stmt.branch (Γ := Γ) f q₁ q₂ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₁ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₂
branch :
  ∀
    (IH₁ :
      ∀ (h : Stmt.branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₁) (hs : SupportsStmt (Γ := Γ) S q₁),
        SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁ q₂))
    (IH₂ :
      ∀ (h : Stmt.branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂),
        SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁ q₂)),
    SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁ q₂)
⊢ SupportsStmt (Γ := Γ) S q₁_1
have branch₁ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₁), SupportsStmt (Γ := Γ) S q₁_1
Tactic: rcases h with (rfl | h | 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
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₁) (hs : SupportsStmt (Γ := Γ) S q₁), SupportsStmt (Γ := Γ) S q₁_1
IH₂ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁_1
hs : SupportsStmt (Γ := Γ) S q₁ ∧ SupportsStmt (Γ := Γ) S q₂
h : q₁_1 = Stmt.branch (Γ := Γ) f q₁ q₂ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₁ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₂
branch :
  ∀
    (IH₁ :
      ∀ (h : Stmt.branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₁) (hs : SupportsStmt (Γ := Γ) S q₁),
        SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁ q₂))
    (IH₂ :
      ∀ (h : Stmt.branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂),
        SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁ q₂)),
    SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁ q₂)
branch₁ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₁), SupportsStmt (Γ := Γ) S q₁_1
⊢ SupportsStmt (Γ := Γ) S q₁_1
have branch₂ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₂), SupportsStmt (Γ := Γ) S q₁_1
Tactic: rcases h with (rfl | h | 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : σ → Λ
h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (goto (Γ := Γ) l)) q₁
hs : SupportsStmt (Γ := Γ) S (goto (Γ := Γ) l)
⊢ SupportsStmt (Γ := Γ) S q₁
have h₁ : q₁ = goto (Γ := Γ) l
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
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
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : σ → Λ
hs : ∀ (v : σ), l v ∈ S
h : q₁ = goto (Γ := Γ) l
⊢ SupportsStmt (Γ := Γ) S q₁
have goto : SupportsStmt (Γ := Γ) S (goto (Γ := Γ) l)
Tactic: subst h
Cleared hypotheses: q₁, 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (halt (Γ := Γ))) q₁
hs : SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (halt (Γ := Γ))
⊢ SupportsStmt (Γ := Γ) S q₁
have h₁ : q₁ = halt (Γ := Γ)
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
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
S : Finset Λ
q₁ : Stmt Γ Λ σ
hs : True
h : q₁ = halt (Γ := Γ)
⊢ SupportsStmt (Γ := Γ) S q₁
have halt : SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (halt (Γ := Γ))
Tactic: subst h
Cleared hypotheses: q₁, 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : σ → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
h : q₁ ∈ stmts₁ (Γ := Γ) (load (Γ := Γ) a a_1)
hs : SupportsStmt (Γ := Γ) S (load (Γ := Γ) a a_1)
⊢ SupportsStmt (Γ := Γ) S q₁
have h₁ : q₁ = load (Γ := Γ) a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
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
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : σ → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = load (Γ := Γ) a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
⊢ SupportsStmt (Γ := Γ) S q₁
have load : ∀
  (IH :
    ∀ (h : load (Γ := Γ) a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
      SupportsStmt (Γ := Γ) S (load (Γ := Γ) a a_1)),
  SupportsStmt (Γ := Γ) S (load (Γ := Γ) a a_1)
Tactic: rcases h with (rfl | h)
Cleared hypotheses: q₁, IH, 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : σ → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = Stmt.load (Γ := Γ) a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
load :
  ∀
    (IH :
      ∀ (h : Stmt.load (Γ := Γ) a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
        SupportsStmt (Γ := Γ) S (Stmt.load (Γ := Γ) a a_1)),
    SupportsStmt (Γ := Γ) S (Stmt.load (Γ := Γ) a a_1)
⊢ SupportsStmt (Γ := Γ) S q₁
have load₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
Tactic: rcases h with (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
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : σ → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = load (Γ := Γ) a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
⊢ SupportsStmt (Γ := Γ) S q₁
have load : ∀
  (IH :
    ∀ (h : load (Γ := Γ) a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
      SupportsStmt (Γ := Γ) S (load (Γ := Γ) a a_1)),
  SupportsStmt (Γ := Γ) S (load (Γ := Γ) a a_1)
Tactic: rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₁, IH, 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : σ → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = Stmt.load (Γ := Γ) a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
load :
  ∀
    (IH :
      ∀ (h : Stmt.load (Γ := Γ) a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
        SupportsStmt (Γ := Γ) S (Stmt.load (Γ := Γ) a a_1)),
    SupportsStmt (Γ := Γ) S (Stmt.load (Γ := Γ) a a_1)
⊢ SupportsStmt (Γ := Γ) S q₁
have load₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
Tactic: rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Γ k
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
h : q₁ ∈ stmts₁ (Γ := Γ) (push (Γ := Γ) k a a_1)
hs : SupportsStmt (Γ := Γ) S (push (Γ := Γ) k a a_1)
⊢ SupportsStmt (Γ := Γ) S q₁
have h₁ : q₁ = push (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Γ k
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = push (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
⊢ SupportsStmt (Γ := Γ) S q₁
have push : ∀
  (IH :
    ∀ (h : push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
      SupportsStmt (Γ := Γ) S (push (Γ := Γ) k a a_1)),
  SupportsStmt (Γ := Γ) S (push (Γ := Γ) k a a_1)
Tactic: rcases h with (rfl | h)
Cleared hypotheses: q₁, IH, 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Γ k
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = Stmt.push (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
push :
  ∀
    (IH :
      ∀ (h : Stmt.push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
        SupportsStmt (Γ := Γ) S (Stmt.push (Γ := Γ) k a a_1)),
    SupportsStmt (Γ := Γ) S (Stmt.push (Γ := Γ) k a a_1)
⊢ SupportsStmt (Γ := Γ) S q₁
have push₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
Tactic: rcases h with (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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Γ k
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = push (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
⊢ SupportsStmt (Γ := Γ) S q₁
have push : ∀
  (IH :
    ∀ (h : push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
      SupportsStmt (Γ := Γ) S (push (Γ := Γ) k a a_1)),
  SupportsStmt (Γ := Γ) S (push (Γ := Γ) k a a_1)
Tactic: rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₁, IH, 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Γ k
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = Stmt.push (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
push :
  ∀
    (IH :
      ∀ (h : Stmt.push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
        SupportsStmt (Γ := Γ) S (Stmt.push (Γ := Γ) k a a_1)),
    SupportsStmt (Γ := Γ) S (Stmt.push (Γ := Γ) k a a_1)
⊢ SupportsStmt (Γ := Γ) S q₁
have push₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
Tactic: rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
h : q₁ ∈ stmts₁ (Γ := Γ) (peek (Γ := Γ) k a a_1)
hs : SupportsStmt (Γ := Γ) S (peek (Γ := Γ) k a a_1)
⊢ SupportsStmt (Γ := Γ) S q₁
have h₁ : q₁ = peek (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = peek (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
⊢ SupportsStmt (Γ := Γ) S q₁
have peek : ∀
  (IH :
    ∀ (h : peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
      SupportsStmt (Γ := Γ) S (peek (Γ := Γ) k a a_1)),
  SupportsStmt (Γ := Γ) S (peek (Γ := Γ) k a a_1)
Tactic: rcases h with (rfl | h)
Cleared hypotheses: q₁, IH, 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = Stmt.peek (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
peek :
  ∀
    (IH :
      ∀ (h : Stmt.peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
        SupportsStmt (Γ := Γ) S (Stmt.peek (Γ := Γ) k a a_1)),
    SupportsStmt (Γ := Γ) S (Stmt.peek (Γ := Γ) k a a_1)
⊢ SupportsStmt (Γ := Γ) S q₁
have peek₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
Tactic: rcases h with (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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = peek (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
⊢ SupportsStmt (Γ := Γ) S q₁
have peek : ∀
  (IH :
    ∀ (h : peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
      SupportsStmt (Γ := Γ) S (peek (Γ := Γ) k a a_1)),
  SupportsStmt (Γ := Γ) S (peek (Γ := Γ) k a a_1)
Tactic: rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₁, IH, 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = Stmt.peek (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
peek :
  ∀
    (IH :
      ∀ (h : Stmt.peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
        SupportsStmt (Γ := Γ) S (Stmt.peek (Γ := Γ) k a a_1)),
    SupportsStmt (Γ := Γ) S (Stmt.peek (Γ := Γ) k a a_1)
⊢ SupportsStmt (Γ := Γ) S q₁
have peek₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
Tactic: rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
h : q₁ ∈ stmts₁ (Γ := Γ) (pop (Γ := Γ) k a a_1)
hs : SupportsStmt (Γ := Γ) S (pop (Γ := Γ) k a a_1)
⊢ SupportsStmt (Γ := Γ) S q₁
have h₁ : q₁ = pop (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = pop (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
⊢ SupportsStmt (Γ := Γ) S q₁
have pop : ∀
  (IH :
    ∀ (h : pop (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
      SupportsStmt (Γ := Γ) S (pop (Γ := Γ) k a a_1)),
  SupportsStmt (Γ := Γ) S (pop (Γ := Γ) k a a_1)
Tactic: rcases h with (rfl | h)
Cleared hypotheses: q₁, IH, 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁
hs : SupportsStmt (Γ := Γ) S a_1
h : q₁ = Stmt.pop (Γ := Γ) k a a_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) a_1
pop :
  ∀
    (IH :
      ∀ (h : Stmt.pop (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1),
        SupportsStmt (Γ := Γ) S (Stmt.pop (Γ := Γ) k a a_1)),
    SupportsStmt (Γ := Γ) S (Stmt.pop (Γ := Γ) k a a_1)
⊢ SupportsStmt (Γ := Γ) S q₁
have pop₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
Tactic: rcases h with (rfl | h)
Cleared hypotheses: h