awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k s q)
HS₁ : trStmts₁ (Λ'.push k s q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.push k s q)) S

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : trStmts₁ (Λ'.read q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.read q)) S

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : trStmts₁ q.succ ⊆ S
⊢ Supports (trStmts₁ q.succ) S

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : trStmts₁ (q₁.pred q₂) ⊆ S
⊢ Supports (trStmts₁ (q₁.pred q₂)) S

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : Cont'
H₁ : Λ'.Supports S (Λ'.ret k)
HS₁ : trStmts₁ (Λ'.ret k) ⊆ S
⊢ Supports (trStmts₁ (Λ'.ret k)) S

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : trStmts₁ (q₁.pred q₂) ⊆ S
pred :
  ∀ (HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S),
    Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
⊢ Supports (trStmts₁ (q₁.pred q₂)) S

Tactic:
simp [trStmts₁, -Finset.singleton_subset_iff] at HS₁ ⊢

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.singleton_subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p k₁ k₂ q)
HS₁ : insert (Λ'.move p k₁ k₂ q) (trStmts₁ q) ⊆ S
⊢ Λ'.move p k₁ k₂ q ∈ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p k₁ k₂ q)
HS₁ : insert (Λ'.move p k₁ k₂ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.move p k₁ k₂ q ∈ S
⊢ trStmts₁ q ⊆ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p k₁ k₂ q)
HS₁ : insert (Λ'.move p k₁ k₂ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.move p k₁ k₂ q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ q ∈ S

Tactic:
have h₃ := h₂ W
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p k₁ k₂ q)
HS₁ : insert (Λ'.move p k₁ k₂ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.move p k₁ k₂ q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ q ∈ S

Tactic:
first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p k q)
HS₁ : insert (Λ'.clear p k q) (trStmts₁ q) ⊆ S
⊢ Λ'.clear p k q ∈ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p k q)
HS₁ : insert (Λ'.clear p k q) (trStmts₁ q) ⊆ S
h₁ : Λ'.clear p k q ∈ S
⊢ trStmts₁ q ⊆ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p k q)
HS₁ : insert (Λ'.clear p k q) (trStmts₁ q) ⊆ S
h₁ : Λ'.clear p k q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ q ∈ S

Tactic:
have h₃ := h₂ W
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p k q)
HS₁ : insert (Λ'.clear p k q) (trStmts₁ q) ⊆ S
h₁ : Λ'.clear p k q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ q ∈ S

Tactic:
first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
⊢ q.copy ∈ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
h₁ : q.copy ∈ S
⊢ trStmts₁ q ⊆ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
h₁ : q.copy ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ q ∈ S

Tactic:
have h₃ := h₂ W
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
h₁ : q.copy ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ q ∈ S

Tactic:
first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k s q)
HS₁ : insert (Λ'.push k s q) (trStmts₁ q) ⊆ S
⊢ Λ'.push k s q ∈ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k s q)
HS₁ : insert (Λ'.push k s q) (trStmts₁ q) ⊆ S
h₁ : Λ'.push k s q ∈ S
⊢ trStmts₁ q ⊆ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k s q)
HS₁ : insert (Λ'.push k s q) (trStmts₁ q) ⊆ S
h₁ : Λ'.push k s q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ q ∈ S

Tactic:
have h₃ := h₂ W
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k s q)
HS₁ : insert (Λ'.push k s q) (trStmts₁ q) ⊆ S
h₁ : Λ'.push k s q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ q ∈ S

Tactic:
first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
⊢ Λ'.read q ∈ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
⊢ (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
⊢ ∀ ⦃x : Λ'⦄ (x_1 : Option Γ') (h : x ∈ trStmts₁ (q x_1)), x ∈ S

Tactic:
simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
⊢ ∀ ⦃x : Λ'⦄ (x_1 : Option Γ') (h : x ∈ trStmts₁ (q x_1)), x ∈ S

Tactic:
try simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
⊢ ∀ ⦃x : Λ'⦄ (x_1 : Option Γ') (h : x ∈ trStmts₁ (q x_1)), x ∈ S

Tactic:
first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
⊢ q.succ ∈ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
⊢ insert (unrev q) (trStmts₁ q) ⊆ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : insert (unrev q) (trStmts₁ q) ⊆ S
⊢ unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S

Tactic:
simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : insert (unrev q) (trStmts₁ q) ⊆ S
⊢ unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S

Tactic:
try simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : insert (unrev q) (trStmts₁ q) ⊆ S
⊢ unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S

Tactic:
first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
⊢ q₁.pred q₂ ∈ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
⊢ insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂) ⊆ S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂) ⊆ S
⊢ unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S

Tactic:
simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂) ⊆ S
⊢ unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S

Tactic:
try simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂) ⊆ S
⊢ unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S

Tactic:
first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

Premises used: Finset.subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : Cont'
H₁ : Λ'.Supports S (Λ'.ret k)
HS₁ : {Λ'.ret k} ⊆ S
⊢ Supports {Λ'.ret k} S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Premises used: Finset.insert_subset_iff, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p k₁ k₂ q)
HS₁ : insert (Λ'.move p k₁ k₂ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.move p k₁ k₂ q ∈ S
h₂ : trStmts₁ q ⊆ S
h₃ : q ∈ S
⊢ Supports (insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)) S

Tactic:
supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩

Premises used: Iff.mpr, And.intro, Turing.PartrecToTM2.supports_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p k₁ k₂ q)
HS₁ : insert (Λ'.move p k₁ k₂ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.move p k₁ k₂ q ∈ S
h₂ : trStmts₁ q ⊆ S
h₃ : q ∈ S
⊢ Supports (insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)) S

Tactic:
exact supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p k q)
HS₁ : insert (Λ'.clear p k q) (trStmts₁ q) ⊆ S
h₁ : Λ'.clear p k q ∈ S
h₂ : trStmts₁ q ⊆ S
h₃ : q ∈ S
⊢ Supports (insert (Λ'.clear p k q) (trStmts₁ q)) S

Tactic:
supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩

Premises used: Iff.mpr, And.intro, Turing.PartrecToTM2.supports_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p k q)
HS₁ : insert (Λ'.clear p k q) (trStmts₁ q) ⊆ S
h₁ : Λ'.clear p k q ∈ S
h₂ : trStmts₁ q ⊆ S
h₃ : q ∈ S
⊢ Supports (insert (Λ'.clear p k q) (trStmts₁ q)) S

Tactic:
exact supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
h₁ : q.copy ∈ S
h₂ : trStmts₁ q ⊆ S
h₃ : q ∈ S
⊢ Supports (insert q.copy (trStmts₁ q)) S

Tactic:
supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₃⟩, q_ih H₁ h₂⟩

Premises used: Iff.mpr, And.intro, Turing.PartrecToTM2.supports_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
h₁ : q.copy ∈ S
h₂ : trStmts₁ q ⊆ S
h₃ : q ∈ S
⊢ Supports (insert q.copy (trStmts₁ q)) S

Tactic:
exact supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₃⟩, q_ih H₁ h₂⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k s q)
HS₁ : insert (Λ'.push k s q) (trStmts₁ q) ⊆ S
h₁ : Λ'.push k s q ∈ S
h₂ : trStmts₁ q ⊆ S
h₃ : q ∈ S
⊢ Supports (insert (Λ'.push k s q) (trStmts₁ q)) S

Tactic:
supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₃⟩, q_ih H₁ h₂⟩

Premises used: Iff.mpr, And.intro, Turing.PartrecToTM2.supports_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k s q)
HS₁ : insert (Λ'.push k s q) (trStmts₁ q) ⊆ S
h₁ : Λ'.push k s q ∈ S
h₂ : trStmts₁ q ⊆ S
h₃ : q ∈ S
⊢ Supports (insert (Λ'.push k s q) (trStmts₁ q)) S

Tactic:
exact supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₃⟩, q_ih H₁ h₂⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : ∀ ⦃x : Λ'⦄ (x_1 : Option Γ') (h : x ∈ trStmts₁ (q x_1)), x ∈ S
⊢ Supports (insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))) S

Tactic:
supports_insert.2 ⟨fun _ => h₂ _ W, ?_⟩

Premises used: Iff.mpr, And.intro, Turing.PartrecToTM2.supports_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : ∀ ⦃x : Λ'⦄ (x_1 : Option Γ') (h : x ∈ trStmts₁ (q x_1)), x ∈ S
read : Supports (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) S
⊢ Supports (insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))) S

Tactic:
refine supports_insert.2 ⟨fun _ => h₂ _ W, ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : ∀ ⦃x : Λ'⦄ (x_1 : Option Γ') (h : x ∈ trStmts₁ (q x_1)), x ∈ S
⊢ Supports (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) S

Tactic:
supports_biUnion.2 fun _ => q_ih _ (H₁ _) fun _ h => h₂ _ h

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_biUnion
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : ∀ ⦃x : Λ'⦄ (x_1 : Option Γ') (h : x ∈ trStmts₁ (q x_1)), x ∈ S
⊢ Supports (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) S

Tactic:
exact supports_biUnion.2 fun _ => q_ih _ (H₁ _) fun _ h => h₂ _ h

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_biUnion