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
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) <;> [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.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) <;> [exact hs; exact IH 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₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ (Γ := Γ) q₂
hs : SupportsStmt (Γ := Γ) S q₂
⊢ SupportsStmt (Γ := Γ) S q₁
have branch : ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
  (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
  (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
  (h : q₁ ∈ stmts₁ (Γ := Γ) (branch (Γ := Γ) f q₁_1 q₂)) (hs : SupportsStmt (Γ := Γ) S (branch (Γ := Γ) f q₁_1 q₂)),
  SupportsStmt (Γ := Γ) S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- 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₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ (Γ := Γ) q₂
hs : SupportsStmt (Γ := Γ) S q₂
branch :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂))
    (hs : SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁_1 q₂)), SupportsStmt (Γ := Γ) S q₁
⊢ SupportsStmt (Γ := Γ) S q₁
have branch₁ : ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
  (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
  (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
  (hs : SupportsStmt (Γ := Γ) S q₁_1 ∧ SupportsStmt (Γ := Γ) S q₂)
  (h : q₁ = Stmt.branch (Γ := Γ) f q₁_1 q₂ ∨ q₁ ∈ stmts₁ (Γ := Γ) q₁_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) q₂),
  SupportsStmt (Γ := Γ) S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- 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₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ (Γ := Γ) q₂
hs : SupportsStmt (Γ := Γ) S q₂
branch :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂))
    (hs : SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁_1 q₂)), SupportsStmt (Γ := Γ) S q₁
branch₁ :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S q₁_1 ∧ SupportsStmt (Γ := Γ) S q₂)
    (h : q₁ = Stmt.branch (Γ := Γ) f q₁_1 q₂ ∨ q₁ ∈ stmts₁ (Γ := Γ) q₁_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) q₂),
    SupportsStmt (Γ := Γ) S q₁
⊢ SupportsStmt (Γ := Γ) S q₁
have goto : ∀ (l : σ → Λ) (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (goto (Γ := Γ) l)) q₁)
  (hs : SupportsStmt (Γ := Γ) S (goto (Γ := Γ) l)), SupportsStmt (Γ := Γ) S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- 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₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ (Γ := Γ) q₂
hs : SupportsStmt (Γ := Γ) S q₂
branch :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂))
    (hs : SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁_1 q₂)), SupportsStmt (Γ := Γ) S q₁
branch₁ :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S q₁_1 ∧ SupportsStmt (Γ := Γ) S q₂)
    (h : q₁ = Stmt.branch (Γ := Γ) f q₁_1 q₂ ∨ q₁ ∈ stmts₁ (Γ := Γ) q₁_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) q₂),
    SupportsStmt (Γ := Γ) S q₁
goto :
  ∀ (l : σ → Λ) (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) l)) q₁)
    (hs : SupportsStmt (Γ := Γ) S (Stmt.goto (Γ := Γ) l)), SupportsStmt (Γ := Γ) S q₁
⊢ SupportsStmt (Γ := Γ) S q₁
have goto₁ : ∀ (l : σ → Λ) (hs : ∀ (v : σ), l v ∈ S) (h : q₁ = Stmt.goto (Γ := Γ) l), SupportsStmt (Γ := Γ) S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- 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₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ (Γ := Γ) q₂
hs : SupportsStmt (Γ := Γ) S q₂
branch :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂))
    (hs : SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁_1 q₂)), SupportsStmt (Γ := Γ) S q₁
branch₁ :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S q₁_1 ∧ SupportsStmt (Γ := Γ) S q₂)
    (h : q₁ = Stmt.branch (Γ := Γ) f q₁_1 q₂ ∨ q₁ ∈ stmts₁ (Γ := Γ) q₁_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) q₂),
    SupportsStmt (Γ := Γ) S q₁
goto :
  ∀ (l : σ → Λ) (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) l)) q₁)
    (hs : SupportsStmt (Γ := Γ) S (Stmt.goto (Γ := Γ) l)), SupportsStmt (Γ := Γ) S q₁
goto₁ : ∀ (l : σ → Λ) (hs : ∀ (v : σ), l v ∈ S) (h : q₁ = Stmt.goto (Γ := Γ) l), SupportsStmt (Γ := Γ) S q₁
⊢ SupportsStmt (Γ := Γ) S q₁
have halt : ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (halt (Γ := Γ))) q₁)
  (hs : SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (halt (Γ := Γ))), SupportsStmt (Γ := Γ) S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- 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₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ (Γ := Γ) q₂
hs : SupportsStmt (Γ := Γ) S q₂
branch :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂))
    (hs : SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁_1 q₂)), SupportsStmt (Γ := Γ) S q₁
branch₁ :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S q₁_1 ∧ SupportsStmt (Γ := Γ) S q₂)
    (h : q₁ = Stmt.branch (Γ := Γ) f q₁_1 q₂ ∨ q₁ ∈ stmts₁ (Γ := Γ) q₁_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) q₂),
    SupportsStmt (Γ := Γ) S q₁
goto :
  ∀ (l : σ → Λ) (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) l)) q₁)
    (hs : SupportsStmt (Γ := Γ) S (Stmt.goto (Γ := Γ) l)), SupportsStmt (Γ := Γ) S q₁
goto₁ : ∀ (l : σ → Λ) (hs : ∀ (v : σ), l v ∈ S) (h : q₁ = Stmt.goto (Γ := Γ) l), SupportsStmt (Γ := Γ) S q₁
halt :
  ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.halt (Γ := Γ))) q₁)
    (hs : SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (Stmt.halt (Γ := Γ))), SupportsStmt (Γ := Γ) S q₁
⊢ SupportsStmt (Γ := Γ) S q₁
have halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt (Γ := Γ)), SupportsStmt (Γ := Γ) S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- 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₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ (Γ := Γ) q₂
hs : SupportsStmt (Γ := Γ) S q₂
branch :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂))
    (hs : SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁_1 q₂)), SupportsStmt (Γ := Γ) S q₁
branch₁ :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S q₁_1 ∧ SupportsStmt (Γ := Γ) S q₂)
    (h : q₁ = Stmt.branch (Γ := Γ) f q₁_1 q₂ ∨ q₁ ∈ stmts₁ (Γ := Γ) q₁_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) q₂),
    SupportsStmt (Γ := Γ) S q₁
goto :
  ∀ (l : σ → Λ) (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) l)) q₁)
    (hs : SupportsStmt (Γ := Γ) S (Stmt.goto (Γ := Γ) l)), SupportsStmt (Γ := Γ) S q₁
goto₁ : ∀ (l : σ → Λ) (hs : ∀ (v : σ), l v ∈ S) (h : q₁ = Stmt.goto (Γ := Γ) l), SupportsStmt (Γ := Γ) S q₁
halt :
  ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.halt (Γ := Γ))) q₁)
    (hs : SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (Stmt.halt (Γ := Γ))), SupportsStmt (Γ := Γ) S q₁
halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt (Γ := Γ)), SupportsStmt (Γ := Γ) S q₁
⊢ SupportsStmt (Γ := Γ) S q₁
have load : ∀ (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₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- 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₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ (Γ := Γ) q₂
hs : SupportsStmt (Γ := Γ) S q₂
branch :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂))
    (hs : SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁_1 q₂)), SupportsStmt (Γ := Γ) S q₁
branch₁ :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S q₁_1 ∧ SupportsStmt (Γ := Γ) S q₂)
    (h : q₁ = Stmt.branch (Γ := Γ) f q₁_1 q₂ ∨ q₁ ∈ stmts₁ (Γ := Γ) q₁_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) q₂),
    SupportsStmt (Γ := Γ) S q₁
goto :
  ∀ (l : σ → Λ) (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) l)) q₁)
    (hs : SupportsStmt (Γ := Γ) S (Stmt.goto (Γ := Γ) l)), SupportsStmt (Γ := Γ) S q₁
goto₁ : ∀ (l : σ → Λ) (hs : ∀ (v : σ), l v ∈ S) (h : q₁ = Stmt.goto (Γ := Γ) l), SupportsStmt (Γ := Γ) S q₁
halt :
  ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.halt (Γ := Γ))) q₁)
    (hs : SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (Stmt.halt (Γ := Γ))), SupportsStmt (Γ := Γ) S q₁
halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt (Γ := Γ)), SupportsStmt (Γ := Γ) S q₁
load :
  ∀ (a : σ → σ) (a_1 : Stmt Γ Λ σ)
    (IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.load (Γ := Γ) a a_1)) (hs : SupportsStmt (Γ := Γ) S (Stmt.load (Γ := Γ) a a_1)),
    SupportsStmt (Γ := Γ) S q₁
⊢ SupportsStmt (Γ := Γ) S q₁
have load₁ : ∀ (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),
  SupportsStmt (Γ := Γ) S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- 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₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ (Γ := Γ) q₂
hs : SupportsStmt (Γ := Γ) S q₂
branch :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁_1 q₂))
    (hs : SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) f q₁_1 q₂)), SupportsStmt (Γ := Γ) S q₁
branch₁ :
  ∀ (f : σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₁_1) (hs : SupportsStmt (Γ := Γ) S q₁_1), SupportsStmt (Γ := Γ) S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) q₂) (hs : SupportsStmt (Γ := Γ) S q₂), SupportsStmt (Γ := Γ) S q₁)
    (hs : SupportsStmt (Γ := Γ) S q₁_1 ∧ SupportsStmt (Γ := Γ) S q₂)
    (h : q₁ = Stmt.branch (Γ := Γ) f q₁_1 q₂ ∨ q₁ ∈ stmts₁ (Γ := Γ) q₁_1 ∨ q₁ ∈ stmts₁ (Γ := Γ) q₂),
    SupportsStmt (Γ := Γ) S q₁
goto :
  ∀ (l : σ → Λ) (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) l)) q₁)
    (hs : SupportsStmt (Γ := Γ) S (Stmt.goto (Γ := Γ) l)), SupportsStmt (Γ := Γ) S q₁
goto₁ : ∀ (l : σ → Λ) (hs : ∀ (v : σ), l v ∈ S) (h : q₁ = Stmt.goto (Γ := Γ) l), SupportsStmt (Γ := Γ) S q₁
halt :
  ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.halt (Γ := Γ))) q₁)
    (hs : SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (Stmt.halt (Γ := Γ))), SupportsStmt (Γ := Γ) S q₁
halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt (Γ := Γ)), SupportsStmt (Γ := Γ) S q₁
load :
  ∀ (a : σ → σ) (a_1 : Stmt Γ Λ σ)
    (IH : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1) (hs : SupportsStmt (Γ := Γ) S a_1), SupportsStmt (Γ := Γ) S q₁)
    (h : q₁ ∈ stmts₁ (Γ := Γ) (Stmt.load (Γ := Γ) a a_1)) (hs : SupportsStmt (Γ := Γ) S (Stmt.load (Γ := Γ) a a_1)),
    SupportsStmt (Γ := Γ) S q₁
load₁ :
  ∀ (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),
    SupportsStmt (Γ := Γ) S q₁
⊢ SupportsStmt (Γ := Γ) S q₁
have push : ∀ (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₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- 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
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ (Γ := Γ) q₂
⊢ some q₂ ∈ stmts (Γ := Γ) M S → some q₁ ∈ stmts (Γ := Γ) M S
have simp : ∀ x ∈ S, q₂ ∈ stmts₁ (Γ := Γ) (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (Γ := Γ) (M a)
Tactic: simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
    forall_eq', exists_imp, and_imp]
-- 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 : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports (Γ := Γ) M S
⊢ some q ∈ stmts (Γ := Γ) M S → SupportsStmt (Γ := Γ) S q
have simp : ∀ x ∈ S, q ∈ stmts₁ (Γ := Γ) (M x) → SupportsStmt (Γ := Γ) S q
Tactic: simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
    forall_eq', exists_imp, and_imp]
-- 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 : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
c' : Cfg Γ Λ σ
h₁ : c' ∈ step (Γ := Γ) M (Cfg.mk (Γ := Γ) (some l₁) v T)
h₂ :
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((Cfg.mk (Γ := Γ) (some l₁) v T).l (Γ := Γ))
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (c'.l (Γ := Γ))
have h₃ : SupportsStmt (Γ := Γ) S (M l₁)
Tactic: replace h₂ := ss.2 _ (Finset.some_mem_insertNone.1 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 : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
c' : Cfg Γ Λ σ
h₁ : c' ∈ step (Γ := Γ) M (Cfg.mk (Γ := Γ) (some l₁) v T)
h₂ : SupportsStmt (Γ := Γ) S (M l₁)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (c'.l (Γ := Γ))
have h₃ : stepAux (Γ := Γ) (M l₁) v T = c'
Tactic: simp only [step, Option.mem_def, Option.some.injEq] 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 : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
c' : Cfg Γ Λ σ
h₂ : SupportsStmt (Γ := Γ) S (M l₁)
h₁ : stepAux (Γ := Γ) (M l₁) v T = c'
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (c'.l (Γ := Γ))
have subst : Membership.mem (γ := Finset (Option Λ)) ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
  ((stepAux (Γ := Γ) (M l₁) v T).l (Γ := Γ))
Tactic: subst c'
Cleared hypotheses: c', h₁