awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (write a q) (stmts₁ q)

Tactic:
grind
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ insert (load a q) (stmts₁ q)
⊢ q₁ = load a q ∨ q₁ ∈ stmts₁ q

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

Premises used: Finset.mem_singleton, Finset.mem_insert, Finset.mem_union
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ = Stmt.load a q ∨ q₁ ∈ stmts₁ q
load :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Stmt.load a q)) (IH : ∀ (h₁₂ : Stmt.load a q ∈ stmts₁ q), q₀ ∈ stmts₁ q),
    q₀ ∈ insert (Stmt.load a q) (stmts₁ q)
load₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ insert (Stmt.load a q) (stmts₁ q)
⊢ q₀ ∈ insert (Stmt.load a q) (stmts₁ q)

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

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

Tactic:
h₀₁

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
a : Γ → σ → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (load a q)
IH : ∀ (h₁₂ : load a q ∈ stmts₁ q), q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a q) (stmts₁ q)

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a q) (stmts₁ q)

Tactic:
grind
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
branch :
  ∀ (p : Γ → σ → 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 p q₁_1 q₂)),
    q₀ ∈ stmts₁ (Stmt.branch p q₁_1 q₂)
branch₁ :
  ∀ (p : Γ → σ → 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 p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    q₀ ∈ insert (Stmt.branch p q₁_1 q₂) (stmts₁ q₁_1 ∪ stmts₁ q₂)
goto : ∀ (l : Γ → σ → Λ) (h₁₂ : q₁ ∈ stmts₁ (Stmt.goto l)), q₀ ∈ stmts₁ (Stmt.goto l)
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₀
move :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (Stmt.move a q)),
    q₀ ∈ stmts₁ (Stmt.move a q)
move₁ :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q),
    q₀ ∈ insert (Stmt.move a q) (stmts₁ q)
write :
  ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (Stmt.write a q)),
    q₀ ∈ stmts₁ (Stmt.write a q)
write₁ :
  ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q)
    (h₁₂ : q₁ = Stmt.write a q ∨ q₁ ∈ stmts₁ q), q₀ ∈ insert (Stmt.write a q) (stmts₁ 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₂

Tactic:
induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)
  | branch p q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · grind
    · grind
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | _ _ q IH =>
    rcases h₁₂ with rfl | h₁₂
    · exact h₀₁
    · grind

Premises used: Finset.mem_singleton, Finset.mem_insert, Turing.TM1.stmts₁, Turing.TM1.Stmt.halt, Finset.mem_union, Turing.TM1.Stmt.goto, Turing.TM1.Stmt.branch, rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
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_union, Finset.mem_singleton] at h₁₂)
  | branch p q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · grind
    · grind
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | _ _ q IH =>
    rcases h₁₂ with rfl | h₁₂
    · exact h₀₁
    · grind

Premises used: Finset.mem_singleton, Finset.mem_insert, Turing.TM1.stmts₁, Turing.TM1.Stmt.halt, Finset.mem_union, Turing.TM1.Stmt.goto, Turing.TM1.Stmt.branch, rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
p : Γ → σ → 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 p q₁ q₂)
hs : SupportsStmt S (branch p q₁ q₂)
⊢ q₁_1 = branch p 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, Finset.mem_insert, Turing.TM1.stmts₁, Finset.mem_union, Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
p : Γ → σ → 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 p q₁ q₂ ∨ q₁_1 ∈ stmts₁ q₁ ∨ q₁_1 ∈ stmts₁ q₂
branch :
  ∀ (IH₁ : ∀ (h : Stmt.branch p q₁ q₂ ∈ stmts₁ q₁) (hs : SupportsStmt S q₁), SupportsStmt S (Stmt.branch p q₁ q₂))
    (IH₂ : ∀ (h : Stmt.branch p q₁ q₂ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S (Stmt.branch p q₁ q₂)),
    SupportsStmt S (Stmt.branch p 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.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
IH₁ : ∀ (h : branch p q₁ q₂ ∈ stmts₁ q₁) (hs : SupportsStmt S q₁), SupportsStmt S (branch p q₁ q₂)
IH₂ : ∀ (h : branch p q₁ q₂ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S (branch p q₁ q₂)
⊢ SupportsStmt S (branch p q₁ q₂)

Tactic:
hs

Premises used: Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
p : Γ → σ → 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.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
p : Γ → σ → 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.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
IH₁ : ∀ (h : branch p q₁ q₂ ∈ stmts₁ q₁) (hs : SupportsStmt S q₁), SupportsStmt S (branch p q₁ q₂)
IH₂ : ∀ (h : branch p q₁ q₂ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S (branch p q₁ q₂)
⊢ SupportsStmt S (branch p q₁ q₂)

Tactic:
exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : Γ → σ → Λ
h : q₁ ∈ stmts₁ (goto l)
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, Finset.mem_insert, Turing.TM1.stmts₁, Finset.mem_union, Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : Γ → σ → Λ
hs : ∀ (a : Γ) (v : σ), l a v ∈ S
h : q₁ = Stmt.goto l
goto : SupportsStmt S (Stmt.goto l)
⊢ SupportsStmt S q₁

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

Tactic:
hs

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

Tactic:
exact hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ halt) q₁
hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) 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, Finset.mem_insert, Turing.TM1.stmts₁, Finset.mem_union, Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
hs : True
h : q₁ = Stmt.halt
halt : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt
⊢ SupportsStmt S q₁

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

Tactic:
trivial
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
h : q₁ ∈ stmts₁ (move a q)
hs : SupportsStmt S (move a q)
⊢ q₁ = move a q ∨ q₁ ∈ stmts₁ q

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

Premises used: Finset.mem_singleton, Finset.mem_insert, Turing.TM1.stmts₁, Finset.mem_union, Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q
move :
  ∀ (IH : ∀ (h : Stmt.move a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.move a q)),
    SupportsStmt S (Stmt.move a q)
move₁ : ∀ (h : q₁ ∈ stmts₁ q), SupportsStmt S q₁
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h)

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
a : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S q
IH : ∀ (h : move a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (move a q)
⊢ SupportsStmt S (move a q)

Tactic:
hs

Premises used: Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
a : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S q
IH : ∀ (h : move a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (move a q)
⊢ SupportsStmt S (move a q)

Tactic:
exact hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁

Tactic:
IH h hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁

Tactic:
exact IH h hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q
move :
  ∀ (IH : ∀ (h : Stmt.move a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.move a q)),
    SupportsStmt S (Stmt.move a q)
move₁ : ∀ (h : q₁ ∈ stmts₁ q), SupportsStmt S q₁
move₂ :
  ∀ (IH : ∀ (h : Stmt.move a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.move a q)),
    SupportsStmt S (Stmt.move a q)
move₃ : ∀ (h : q₁ ∈ stmts₁ q), 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.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
h : q₁ ∈ stmts₁ (write a q)
hs : SupportsStmt S (write a q)
⊢ q₁ = write a q ∨ q₁ ∈ stmts₁ q

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

Premises used: Finset.mem_singleton, Finset.mem_insert, Turing.TM1.stmts₁, Finset.mem_union, Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = Stmt.write a q ∨ q₁ ∈ stmts₁ q
write :
  ∀ (IH : ∀ (h : Stmt.write a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.write a q)),
    SupportsStmt S (Stmt.write a q)
write₁ : ∀ (h : q₁ ∈ stmts₁ q), SupportsStmt S q₁
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h)

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S q
IH : ∀ (h : write a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (write a q)
⊢ SupportsStmt S (write a q)

Tactic:
hs

Premises used: Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S q
IH : ∀ (h : write a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (write a q)
⊢ SupportsStmt S (write a q)

Tactic:
exact hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁

Tactic:
IH h hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁

Tactic:
exact IH h hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = Stmt.write a q ∨ q₁ ∈ stmts₁ q
write :
  ∀ (IH : ∀ (h : Stmt.write a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.write a q)),
    SupportsStmt S (Stmt.write a q)
write₁ : ∀ (h : q₁ ∈ stmts₁ q), SupportsStmt S q₁
write₂ :
  ∀ (IH : ∀ (h : Stmt.write a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.write a q)),
    SupportsStmt S (Stmt.write a q)
write₃ : ∀ (h : q₁ ∈ stmts₁ q), 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.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
h : q₁ ∈ stmts₁ (load a q)
hs : SupportsStmt S (load a q)
⊢ q₁ = load a q ∨ q₁ ∈ stmts₁ q

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

Premises used: Finset.mem_singleton, Finset.mem_insert, Turing.TM1.stmts₁, Finset.mem_union, Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = Stmt.load a q ∨ q₁ ∈ stmts₁ q
load :
  ∀ (IH : ∀ (h : Stmt.load a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.load a q)),
    SupportsStmt S (Stmt.load a q)
load₁ : ∀ (h : q₁ ∈ stmts₁ q), SupportsStmt S q₁
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h)

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
a : Γ → σ → σ
q : Stmt Γ Λ σ
hs : SupportsStmt S q
IH : ∀ (h : load a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (load a q)
⊢ SupportsStmt S (load a q)

Tactic:
hs

Premises used: Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
a : Γ → σ → σ
q : Stmt Γ Λ σ
hs : SupportsStmt S q
IH : ∀ (h : load a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (load a q)
⊢ SupportsStmt S (load a q)

Tactic:
exact hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁

Tactic:
IH h hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁

Tactic:
exact IH h hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = Stmt.load a q ∨ q₁ ∈ stmts₁ q
load :
  ∀ (IH : ∀ (h : Stmt.load a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.load a q)),
    SupportsStmt S (Stmt.load a q)
load₁ : ∀ (h : q₁ ∈ stmts₁ q), SupportsStmt S q₁
load₂ :
  ∀ (IH : ∀ (h : Stmt.load a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.load a q)),
    SupportsStmt S (Stmt.load a q)
load₃ : ∀ (h : q₁ ∈ stmts₁ q), 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.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
branch :
  ∀ (p : Γ → σ → 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 p q₁_1 q₂))
    (hs : SupportsStmt S (Stmt.branch p q₁_1 q₂)), SupportsStmt S q₁
branch₁ :
  ∀ (p : Γ → σ → 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 p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    SupportsStmt S q₁
goto : ∀ (l : Γ → σ → Λ) (h : q₁ ∈ stmts₁ (Stmt.goto l)) (hs : SupportsStmt S (Stmt.goto l)), SupportsStmt S q₁
goto₁ : ∀ (l : Γ → σ → Λ) (hs : ∀ (a : Γ) (v : σ), l a 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} (Γ := Γ) (σ := σ) S Stmt.halt), SupportsStmt S q₁
halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt), SupportsStmt S q₁
move :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (h : q₁ ∈ stmts₁ (Stmt.move a q)) (hs : SupportsStmt S (Stmt.move a q)), SupportsStmt S q₁
move₁ :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (hs : SupportsStmt S q) (h : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q), SupportsStmt S q₁
write :
  ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (h : q₁ ∈ stmts₁ (Stmt.write a q)) (hs : SupportsStmt S (Stmt.write a q)), SupportsStmt S q₁
write₁ :
  ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (hs : SupportsStmt S q) (h : q₁ = Stmt.write a q ∨ q₁ ∈ stmts₁ q), SupportsStmt S q₁
load :
  ∀ (a : Γ → σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (h : q₁ ∈ stmts₁ (Stmt.load a q)) (hs : SupportsStmt S (Stmt.load a q)), SupportsStmt S q₁
load₁ :
  ∀ (a : Γ → σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (hs : SupportsStmt S q) (h : q₁ = Stmt.load a q ∨ q₁ ∈ stmts₁ q), 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 p 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
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

Premises used: Finset.mem_singleton, Finset.mem_insert, Turing.TM1.stmts₁, Turing.TM1.Stmt.halt, Finset.mem_union, Turing.TM1.Stmt.goto, Turing.TM1.SupportsStmt, Turing.TM1.Stmt.branch, rfl