awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
push₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ insert (Stmt.push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (Stmt.push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
rcases h₁₂ with (rfl | h₁₂)

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k : K
a : σ → Γ k
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (push (Γ := Γ) k a q)
IH : ∀ (h₁₂ : push (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
unfold stmts₁ at h₀₁

Premises used: Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k : K
a : σ → Γ k
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : push (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₀₁ : q₀ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k : K
a : σ → Γ k
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : push (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₀₁ : q₀ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
Finset.mem_insert_of_mem (IH h₁₂)

Premises used: Set.Mem, setOf, Finset.mem_insert_of_mem
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
exact Finset.mem_insert_of_mem (IH h₁₂)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ = peek (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] at h₁₂

Premises used: Finset.mem_singleton, Finset.mem_insert, Finset.mem_union
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
peek₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ insert (Stmt.peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (Stmt.peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
rcases h₁₂ with (rfl | h₁₂)

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
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:
unfold stmts₁ at h₀₁

Premises used: Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : peek (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₀₁ : q₀ ∈ insert (peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : peek (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₀₁ : q₀ ∈ insert (peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
Finset.mem_insert_of_mem (IH h₁₂)

Premises used: Set.Mem, setOf, Finset.mem_insert_of_mem
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (peek (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
exact Finset.mem_insert_of_mem (IH h₁₂)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ = pop (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] at h₁₂

Premises used: Finset.mem_singleton, Finset.mem_insert, Finset.mem_union
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
pop₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ insert (Stmt.pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (Stmt.pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
rcases h₁₂ with (rfl | h₁₂)

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
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:
unfold stmts₁ at h₀₁

Premises used: Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : pop (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₀₁ : q₀ ∈ insert (pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k : K
a : σ → Option (Γ k) → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : pop (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₀₁ : q₀ ∈ insert (pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
Finset.mem_insert_of_mem (IH h₁₂)

Premises used: Set.Mem, setOf, Finset.mem_insert_of_mem
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (pop (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)

Tactic:
exact Finset.mem_insert_of_mem (IH h₁₂)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₂

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₁₂)

Premises used: Finset.mem_singleton, Turing.TM2.Stmt.branch, Finset.mem_insert, Turing.TM2.Stmt.load, Turing.TM2.Stmt.goto, Finset.mem_union, Turing.TM2.Stmt.halt, Turing.TM2.stmts₁, rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₂
intro₁ intro₂ :
  ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q₂) ⦃q₀ : Stmt Γ Λ σ⦄ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₂
⊢ q₁ ∈ stmts₁ (Γ := Γ) q₂ → stmts₁ (Γ := Γ) 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₁₂)

Premises used: Finset.mem_singleton, Turing.TM2.Stmt.branch, Finset.mem_insert, Turing.TM2.Stmt.load, Turing.TM2.Stmt.goto, Finset.mem_union, Turing.TM2.Stmt.halt, Turing.TM2.stmts₁, rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₂)
⊢ 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

Premises used: Finset.mem_singleton, Turing.TM2.SupportsStmt, Finset.mem_insert, Finset.mem_union, Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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
branch₂ : ∀ (h : q₁_1 ∈ stmts₁ (Γ := Γ) q₂), SupportsStmt (Γ := Γ) S q₁_1
⊢ SupportsStmt (Γ := Γ) S q₁_1

Tactic:
rcases h with (rfl | h | h)

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt (Γ := Γ) S q₁ ∧ SupportsStmt (Γ := Γ) S q₂
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:
hs

Premises used: Turing.TM2.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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 ∈ stmts₁ (Γ := Γ) q₁
⊢ SupportsStmt (Γ := Γ) S q₁_1

Tactic:
IH₁ h hs.1

Premises used: And.left
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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 ∈ stmts₁ (Γ := Γ) q₂
⊢ SupportsStmt (Γ := Γ) S q₁_1

Tactic:
IH₂ h hs.2

Premises used: And.right
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt (Γ := Γ) S q₁ ∧ SupportsStmt (Γ := Γ) S q₂
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:
exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
⊢ q₁ = goto (Γ := Γ) l

Tactic:
simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs

Premises used: Finset.mem_singleton, Turing.TM2.SupportsStmt, Finset.mem_insert, Finset.mem_union, Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ = Stmt.goto (Γ := Γ) l
goto : SupportsStmt (Γ := Γ) S (Stmt.goto (Γ := Γ) l)
⊢ SupportsStmt (Γ := Γ) S q₁

Tactic:
subst h
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
l : σ → Λ
hs : ∀ (v : σ), l v ∈ S
⊢ SupportsStmt (Γ := Γ) S (goto (Γ := Γ) l)

Tactic:
hs

Premises used: Turing.TM2.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
l : σ → Λ
hs : ∀ (v : σ), l v ∈ S
⊢ SupportsStmt (Γ := Γ) S (goto (Γ := Γ) l)

Tactic:
exact hs
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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 (Γ := Γ))
⊢ q₁ = halt (Γ := Γ)

Tactic:
simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs

Premises used: Finset.mem_singleton, Turing.TM2.SupportsStmt, Finset.mem_insert, Finset.mem_union, Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
hs : True
h : q₁ = Stmt.halt (Γ := Γ)
halt : SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (Stmt.halt (Γ := Γ))
⊢ SupportsStmt (Γ := Γ) S q₁

Tactic:
subst h
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
hs : True
⊢ SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (halt (Γ := Γ))

Tactic:
trivial
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
⊢ 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

Premises used: Finset.mem_singleton, Turing.TM2.SupportsStmt, Finset.mem_insert, Finset.mem_union, Turing.TM2.stmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
load₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
⊢ SupportsStmt (Γ := Γ) S q₁

Tactic:
rcases h with (rfl | h)

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
a : σ → σ
a_1 : Stmt Γ Λ σ
hs : SupportsStmt (Γ := Γ) S a_1
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:
hs

Premises used: Turing.TM2.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
a : σ → σ
a_1 : Stmt Γ Λ σ
hs : SupportsStmt (Γ := Γ) S a_1
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:
exact hs
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ ∈ stmts₁ (Γ := Γ) a_1
⊢ SupportsStmt (Γ := Γ) S q₁

Tactic:
IH h hs
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ ∈ stmts₁ (Γ := Γ) a_1
⊢ SupportsStmt (Γ := Γ) S q₁

Tactic:
exact IH h hs
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
load₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
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)
load₃ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
⊢ SupportsStmt (Γ := Γ) S q₁

Tactic:
rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
⊢ 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

Premises used: Finset.mem_singleton, Turing.TM2.SupportsStmt, Finset.mem_insert, Finset.mem_union, Turing.TM2.stmts₁