awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.copy (trStmts₁ q)

Tactic:
exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.copy (trStmts₁ q)

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
copy : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.copy (trStmts₁ q)
⊢ q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.trans, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.subset_insert, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
push : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.push k s q) (trStmts₁ q)
⊢ q' ∈ trStmts₁ (Λ'.push k s q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k s q)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.push k s q) (trStmts₁ q)

Tactic:
fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Turing.PartrecToTM2.Λ'.push, Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.push k s q) (trStmts₁ q)

Tactic:
exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.push k s q) (trStmts₁ q)

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
push : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.push k s q) (trStmts₁ q)
⊢ q' ∈ trStmts₁ (Λ'.push k s q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k s q)

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.trans, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.subset_insert, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
read :
  Membership.mem (γ := Finset Λ') (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) q' →
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))
⊢ q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
h : ?_mvar.152830
⊢ trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))

Tactic:
Finset.Subset.trans

Premises used: Finset.Subset.trans
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
h : ?_mvar.152830
⊢ ?_mvar.152834 ⊆ ?_mvar.152835

Tactic:
q_ih
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
read :
  Membership.mem (γ := Finset Λ') (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) q' →
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))
⊢ q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.trans, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.subset_insert, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
succ :
  (q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧
    (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))
⊢ q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
succ :
  (q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧
    (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))
⊢ q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.trans, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.subset_insert, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
pred :
  (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
      (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))
⊢ q' ∈ trStmts₁ (q₁.pred q₂) → trStmts₁ q' ⊆ trStmts₁ (q₁.pred q₂)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
pred :
  (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
      (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))
⊢ q' ∈ trStmts₁ (q₁.pred q₂) → trStmts₁ q' ⊆ trStmts₁ (q₁.pred q₂)

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
k : Cont'
⊢ q' ∈ trStmts₁ (Λ'.ret k) → trStmts₁ q' ⊆ trStmts₁ (Λ'.ret k)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
k : Cont'
⊢ q' ∈ trStmts₁ (Λ'.ret k) → trStmts₁ q' ⊆ trStmts₁ (Λ'.ret k)

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
read :
  ∀ (x : Option Γ') (h : q' ∈ trStmts₁ (q x)),
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))
⊢ Membership.mem (γ := Finset Λ') (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) q' →
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))

Tactic:
simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, forall_exists_index]

Premises used: Finset.mem_univ, forall_exists_index, Finset.mem_biUnion, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
s : Option Γ'
h : q' ∈ trStmts₁ (q s)
x : Λ'
h' : x ∈ trStmts₁ q'
read : x = Λ'.read q ∨ ∃ (a : Option Γ'), x ∈ trStmts₁ (q a)
⊢ Membership.mem (γ := Finset Λ') (insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)))
    x

Tactic:
simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, Finset.mem_insert]

Premises used: Finset.mem_univ, Finset.mem_insert, Finset.mem_biUnion, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
s : Option Γ'
h : q' ∈ trStmts₁ (q s)
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = Λ'.read q ∨ ∃ (a : Option Γ'), x ∈ trStmts₁ (q a)

Tactic:
Or.inr ⟨_, q_ih s h h'⟩

Premises used: Exists.intro, Or.inr
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
s : Option Γ'
h : q' ∈ trStmts₁ (q s)
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = Λ'.read q ∨ ∃ (a : Option Γ'), x ∈ trStmts₁ (q a)

Tactic:
exact Or.inr ⟨_, q_ih s h h'⟩

Premises used: Or.inr
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
succ : q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))
succ₁ : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))
⊢ (q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧
    (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))

Tactic:
constructor
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : unrev q ∈ trStmts₁ q → trStmts₁ (unrev q) ⊆ trStmts₁ q
⊢ trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))

Tactic:
apply Finset.subset_insert

Premises used: Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
h : q' ∈ trStmts₁ q
x : Λ'
h' : x ∈ trStmts₁ q'
succ : x = q.succ ∨ x = unrev q ∨ x ∈ trStmts₁ q
⊢ x ∈ insert q.succ (insert (unrev q) (trStmts₁ q))

Tactic:
simp only [Finset.mem_insert]

Premises used: Finset.mem_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
h : q' ∈ trStmts₁ q
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = q.succ ∨ x = unrev q ∨ x ∈ trStmts₁ q

Tactic:
Or.inr (Or.inr <| q_ih h h')

Premises used: Or.inr
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
h : q' ∈ trStmts₁ q
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = q.succ ∨ x = unrev q ∨ x ∈ trStmts₁ q

Tactic:
exact Or.inr (Or.inr <| q_ih h h')

Premises used: Or.inr
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
      (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))

Tactic:
⟨fun h x h' => ?_, fun _ x h' => ?_, fun h x h' => ?_⟩

Premises used: And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
pred :
  ∀ (h : q' ∈ trStmts₁ q₁) (x : Λ') (h' : x ∈ trStmts₁ q'),
    x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
pred₁ :
  q' = unrev q₂ →
    ∀ (x : Λ') (h' : x ∈ trStmts₁ (unrev q₂)), x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
pred₂ :
  ∀ (h : q' ∈ trStmts₁ q₂) (x : Λ') (h' : x ∈ trStmts₁ q'),
    x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
⊢ (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
      (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))

Tactic:
refine ⟨fun h x h' => ?_, fun _ x h' => ?_, fun h x h' => ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₁
x : Λ'
h' : x ∈ trStmts₁ q'
pred : x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
⊢ x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' = unrev q₂
x : Λ'
h' : x ∈ trStmts₁ (unrev q₂)
pred : x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
⊢ x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₂
x : Λ'
h' : x ∈ trStmts₁ q'
pred : x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
⊢ x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₁
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂

Tactic:
Or.inr (Or.inr <| Or.inl <| q₁_ih h h')

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₁
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂

Tactic:
exact Or.inr (Or.inr <| Or.inl <| q₁_ih h h')

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' = unrev q₂
x : Λ'
h' : x ∈ trStmts₁ (unrev q₂)
pred :
  ∀ (h' : x = Λ'.move (fun (x : Γ') ↦ false) rev main q₂),
    x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
pred₁ : ∀ (h' : x ∈ trStmts₁ q₂), x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂

Tactic:
rcases Finset.mem_insert.1 h' with h' | h'

Premises used: Finset.mem_insert, Iff.mp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' = unrev q₂
x : Λ'
h'_1 : x ∈ trStmts₁ (unrev q₂)
h' : x = Λ'.move (fun (x : Γ') ↦ false) rev main q₂
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂

Tactic:
simp [h', unrev]

Premises used: Turing.PartrecToTM2.unrev
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' = unrev q₂
x : Λ'
h'_1 : x ∈ trStmts₁ (unrev q₂)
h' : x ∈ trStmts₁ q₂
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂

Tactic:
simp [h', unrev]

Premises used: Turing.PartrecToTM2.unrev
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₂
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂

Tactic:
Or.inr (Or.inr <| Or.inr <| q₂_ih h h')

Premises used: Or.inr
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₂
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂

Tactic:
exact Or.inr (Or.inr <| Or.inr <| q₂_ih h h')

Premises used: Or.inr
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
move : ∀ (p : Γ' → Bool) (k₁ k₂ : K'), ∀ q ∈ trStmts₁ q, Λ'.move p k₁ k₂ q ∈ trStmts₁ (Λ'.move p k₁ k₂ q)
clear : ∀ (p : Γ' → Bool) (k : K'), ∀ q ∈ trStmts₁ q, Λ'.clear p k q ∈ trStmts₁ (Λ'.clear p k q)
copy : ∀ q ∈ trStmts₁ q, q.copy ∈ trStmts₁ q.copy
push : ∀ (k : K') (s : Option Γ' → Option Γ'), ∀ q ∈ trStmts₁ q, Λ'.push k s q ∈ trStmts₁ (Λ'.push k s q)
read : ∀ (f : Option Γ' → Λ'), (∀ (a : Option Γ'), f a ∈ trStmts₁ (f a)) → Λ'.read f ∈ trStmts₁ (Λ'.read f)
succ : ∀ q ∈ trStmts₁ q, q.succ ∈ trStmts₁ q.succ
pred : ∀ (q₁ q₂ : Λ'), q₁ ∈ trStmts₁ q₁ → q₂ ∈ trStmts₁ q₂ → q₁.pred q₂ ∈ trStmts₁ (q₁.pred q₂)
ret : ∀ (k : Cont'), Λ'.ret k ∈ trStmts₁ (Λ'.ret k)
⊢ q ∈ trStmts₁ q

Tactic:
induction q
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : q ∈ trStmts₁ q
⊢ Λ'.move p k₁ k₂ q ∈ trStmts₁ (Λ'.move p k₁ k₂ q)

Tactic:
apply Finset.mem_insert_self

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : q ∈ trStmts₁ q
⊢ Λ'.move p k₁ k₂ q ∈ trStmts₁ (Λ'.move p k₁ k₂ q)

Tactic:
first | apply Finset.mem_singleton_self | apply Finset.mem_insert_self

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : q ∈ trStmts₁ q
⊢ Λ'.clear p k q ∈ trStmts₁ (Λ'.clear p k q)

Tactic:
apply Finset.mem_insert_self

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : q ∈ trStmts₁ q
⊢ Λ'.clear p k q ∈ trStmts₁ (Λ'.clear p k q)

Tactic:
first | apply Finset.mem_singleton_self | apply Finset.mem_insert_self

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : q ∈ trStmts₁ q
⊢ q.copy ∈ trStmts₁ q.copy

Tactic:
apply Finset.mem_insert_self

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : q ∈ trStmts₁ q
⊢ q.copy ∈ trStmts₁ q.copy

Tactic:
first | apply Finset.mem_singleton_self | apply Finset.mem_insert_self

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : q ∈ trStmts₁ q
⊢ Λ'.push k s q ∈ trStmts₁ (Λ'.push k s q)

Tactic:
apply Finset.mem_insert_self

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : q ∈ trStmts₁ q
⊢ Λ'.push k s q ∈ trStmts₁ (Λ'.push k s q)

Tactic:
first | apply Finset.mem_singleton_self | apply Finset.mem_insert_self

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : ∀ (a : Option Γ'), f a ∈ trStmts₁ (f a)
⊢ Λ'.read f ∈ trStmts₁ (Λ'.read f)

Tactic:
apply Finset.mem_insert_self

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : ∀ (a : Option Γ'), f a ∈ trStmts₁ (f a)
⊢ Λ'.read f ∈ trStmts₁ (Λ'.read f)

Tactic:
first | apply Finset.mem_singleton_self | apply Finset.mem_insert_self

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : q ∈ trStmts₁ q
⊢ q.succ ∈ trStmts₁ q.succ

Tactic:
apply Finset.mem_insert_self

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : q ∈ trStmts₁ q
⊢ q.succ ∈ trStmts₁ q.succ

Tactic:
first | apply Finset.mem_singleton_self | apply Finset.mem_insert_self

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : q₁ ∈ trStmts₁ q₁
q₂_ih : q₂ ∈ trStmts₁ q₂
⊢ q₁.pred q₂ ∈ trStmts₁ (q₁.pred q₂)

Tactic:
apply Finset.mem_insert_self

Premises used: Finset.mem_insert_self