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
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)
push₁ : ∀ (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 Λ
k : K
a : σ → Γ k
a_1 : Stmt Γ Λ σ
hs : SupportsStmt (Γ := Γ) S a_1
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:
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 Λ
k : K
a : σ → Γ k
a_1 : Stmt Γ Λ σ
hs : SupportsStmt (Γ := Γ) S a_1
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:
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 Γ Λ σ
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₁ ∈ 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 Γ Λ σ
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₁ ∈ 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 Γ Λ σ
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)
push₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
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)
push₃ : ∀ (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 : σ → 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)
⊢ 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

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 Γ Λ σ
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)
peek₁ : ∀ (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 Λ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
hs : SupportsStmt (Γ := Γ) S a_1
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:
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 Λ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
hs : SupportsStmt (Γ := Γ) S a_1
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:
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 Γ Λ σ
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₁ ∈ 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 Γ Λ σ
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₁ ∈ 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 Γ Λ σ
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)
peek₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
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)
peek₃ : ∀ (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 : σ → 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)
⊢ 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

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 Γ Λ σ
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)
pop₁ : ∀ (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 Λ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
hs : SupportsStmt (Γ := Γ) S a_1
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:
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 Λ
k : K
a : σ → Option (Γ k) → σ
a_1 : Stmt Γ Λ σ
hs : SupportsStmt (Γ := Γ) S a_1
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:
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 Γ Λ σ
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)
pop₁ : ∀ (h : q₁ ∈ stmts₁ (Γ := Γ) a_1), SupportsStmt (Γ := Γ) S q₁
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)
pop₃ : ∀ (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₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ (Γ := Γ) q₂
hs : SupportsStmt (Γ := Γ) S 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]

Premises used: Finset.mem_singleton, Turing.TM2.SupportsStmt, 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
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ (Γ := Γ) q₂
simp : ∀ x ∈ S, q₂ ∈ stmts₁ (Γ := Γ) (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (Γ := Γ) (M a)
⊢ some q₂ ∈ stmts (Γ := Γ) M S → some q₁ ∈ stmts (Γ := Γ) M S

Tactic:
simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
    forall_eq', exists_imp, and_imp]

Premises used: and_imp, Option.some.injEq, forall_eq', exists_imp, Turing.TM2.stmts, Finset.mem_biUnion, Option.mem_def, Finset.mem_insertNone
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₂
⊢ ∀ x ∈ S, q₂ ∈ stmts₁ (Γ := Γ) (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (Γ := Γ) (M a)

Tactic:
fun l ls h₂ ↦ ⟨_, ls, stmts₁_trans h₂ h₁⟩

Premises used: Turing.TM2.stmts₁_trans, And.intro, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₂
⊢ ∀ x ∈ S, q₂ ∈ stmts₁ (Γ := Γ) (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (Γ := Γ) (M a)

Tactic:
exact fun l ls h₂ ↦ ⟨_, ls, stmts₁_trans h₂ h₁⟩
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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
simp : ∀ x ∈ S, q ∈ stmts₁ (Γ := Γ) (M x) → SupportsStmt (Γ := Γ) S q
⊢ some q ∈ stmts (Γ := Γ) M S → 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]

Premises used: and_imp, Option.some.injEq, forall_eq', exists_imp, Turing.TM2.stmts, Finset.mem_biUnion, Option.mem_def, Finset.mem_insertNone
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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
⊢ ∀ x ∈ S, q ∈ stmts₁ (Γ := Γ) (M x) → SupportsStmt (Γ := Γ) S q

Tactic:
fun l ls h ↦ stmts₁_supportsStmt_mono h (ss.2 _ ls)

Premises used: Turing.TM2.stmts₁_supportsStmt_mono, And.right
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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
⊢ ∀ x ∈ S, q ∈ stmts₁ (Γ := Γ) (M x) → SupportsStmt (Γ := Γ) S q

Tactic:
exact fun l ls h ↦ stmts₁_supportsStmt_mono h (ss.2 _ ls)

Premises used: Turing.TM2.stmts₁_supportsStmt_mono, And.right
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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 (Γ := Γ))
⊢ SupportsStmt (Γ := Γ) S (M l₁)

Tactic:
replace h₂ := ss.2 _ (Finset.some_mem_insertNone.1 h₂)
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁)
⊢ stepAux (Γ := Γ) (M l₁) v T = c'

Tactic:
simp only [step, Option.mem_def, Option.some.injEq] at h₁

Premises used: Option.some.injEq, Turing.TM2.step, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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'
subst :
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (M l₁) v T).l (Γ := Γ))
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (c'.l (Γ := Γ))

Tactic:
subst c'
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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)
h₂ : SupportsStmt (Γ := Γ) S (M l₁)
revert :
  ∀ (h₂ : SupportsStmt (Γ := Γ) S (M l₁)),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) (M l₁) v T).l (Γ := Γ))
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((stepAux (Γ := Γ) (M l₁) v T).l (Γ := Γ))

Tactic:
revert h₂
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₁' v T).l (Γ := Γ))
IH₂ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (Stmt.branch (Γ := Γ) p q₁' q₂')
branch :
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((bif false then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
branch₁ :
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((bif true then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((bif p v then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))

Tactic:
cases p v
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₁' v T).l (Γ := Γ))
IH₂ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (branch (Γ := Γ) p q₁' q₂')
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((bif false then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))

Tactic:
IH₂ _ _ hs.2

Premises used: cond, Set.Mem, setOf, And.right
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₁' v T).l (Γ := Γ))
IH₂ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (branch (Γ := Γ) p q₁' q₂')
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((bif false then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))

Tactic:
exact IH₂ _ _ 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
inst : Inhabited Λ
inst_1 : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports (Γ := Γ) M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₁' v T).l (Γ := Γ))
IH₂ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (branch (Γ := Γ) p q₁' q₂')
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((bif true then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))

Tactic:
IH₁ _ _ hs.1

Premises used: cond, Set.Mem, setOf, And.left
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
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₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₁' v T).l (Γ := Γ))
IH₂ :
  ∀ (v : σ) (T : (k : K) → List (Γ k)) (h₂ : SupportsStmt (Γ := Γ) S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
      ((stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt (Γ := Γ) S (branch (Γ := Γ) p q₁' q₂')
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    ((bif true then stepAux (Γ := Γ) q₁' v T else stepAux (Γ := Γ) q₂' v T).l (Γ := Γ))

Tactic:
exact IH₁ _ _ hs.1

Premises used: And.left