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₁
k : K
a : σ → Γ k
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ = Stmt.push (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q
push :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a q))
    (IH : ∀ (h₁₂ : Stmt.push (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q),
    q₀ ∈ insert (Stmt.push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (Stmt.push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
have push₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ insert (Stmt.push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
Tactic: rcases h₁₂ with (rfl | 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
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ ∈ insert (peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
have h₁₃ : q₁ = peek (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] 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
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ = peek (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
have peek : ∀ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (peek (Γ := Γ) k a q))
  (IH : ∀ (h₁₂ : peek (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q),
  q₀ ∈ insert (peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
Tactic: rcases h₁₂ with (rfl | h₁₂)
Cleared hypotheses: q₁, h₀₁, 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
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ = Stmt.peek (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q
peek :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (Stmt.peek (Γ := Γ) k a q))
    (IH : ∀ (h₁₂ : Stmt.peek (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q),
    q₀ ∈ insert (Stmt.peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (Stmt.peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
have peek₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ insert (Stmt.peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
Tactic: rcases h₁₂ with (rfl | 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
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ ∈ insert (pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
have h₁₃ : q₁ = pop (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] 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
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ = pop (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
have pop : ∀ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (pop (Γ := Γ) k a q))
  (IH : ∀ (h₁₂ : pop (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q),
  q₀ ∈ insert (pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
Tactic: rcases h₁₂ with (rfl | h₁₂)
Cleared hypotheses: q₁, h₀₁, 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
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ = Stmt.pop (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q
pop :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (Stmt.pop (Γ := Γ) k a q))
    (IH : ∀ (h₁₂ : Stmt.pop (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q),
    q₀ ∈ insert (Stmt.pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (Stmt.pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
have pop₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ insert (Stmt.pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) 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
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
⊢ q₀ ∈ stmts₁ (Γ := Γ) q₂
have 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₁ (Γ := Γ) (branch (Γ := Γ) f q₁_1 q₂)), q₀ ∈ stmts₁ (Γ := Γ) (branch (Γ := Γ) f q₁_1 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 Γ Λ σ
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₂)
⊢ q₀ ∈ stmts₁ (Γ := Γ) q₂
have 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₂)
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 Γ Λ σ
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₂)
⊢ q₀ ∈ stmts₁ (Γ := Γ) q₂
have goto : ∀ (l : σ → Λ) (h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (goto (Γ := Γ) l)) q₁),
  Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (goto (Γ := Γ) l)) 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 Γ Λ σ
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₀
⊢ q₀ ∈ stmts₁ (Γ := Γ) q₂
have goto₁ : ∀ (l : σ → Λ) (h₁₂ : q₁ = Stmt.goto (Γ := Γ) l), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.goto (Γ := Γ) l} 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 Γ Λ σ
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₀
⊢ q₀ ∈ stmts₁ (Γ := Γ) q₂
have halt : ∀ (h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (halt (Γ := Γ))) q₁),
  Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (halt (Γ := Γ))) 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 Γ Λ σ
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₀
⊢ q₀ ∈ stmts₁ (Γ := Γ) q₂
have halt₁ : ∀ (h₁₂ : q₁ = Stmt.halt (Γ := Γ)), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.halt (Γ := Γ)} 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 Γ Λ σ
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₀
⊢ q₀ ∈ stmts₁ (Γ := Γ) q₂
have load : ∀ (a : σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
  (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) (load (Γ := Γ) a q)), q₀ ∈ stmts₁ (Γ := Γ) (load (Γ := Γ) a 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 Γ Λ σ
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)
⊢ q₀ ∈ stmts₁ (Γ := Γ) q₂
have 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)
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 Γ Λ σ
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)
⊢ q₀ ∈ stmts₁ (Γ := Γ) q₂
have push : ∀ (k : K) (a : σ → Γ k) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q)
  (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) (push (Γ := Γ) k a q)), q₀ ∈ stmts₁ (Γ := Γ) (push (Γ := Γ) k a 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₁₂