awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
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 : Cont'
⊢ Λ'.ret k ∈ trStmts₁ (Λ'.ret k)

Tactic:
apply Finset.mem_singleton_self

Premises used: Finset.mem_singleton_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ Λ'.ret k ∈ trStmts₁ (Λ'.ret k)

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:
c : Code
k : Cont'
zero' : trStmts₁ (trNormal Code.zero' k) ⊆ trStmts₁ (trNormal Code.zero' k)
succ : trStmts₁ (trNormal Code.succ k) ⊆ trStmts₁ (trNormal Code.succ k)
tail : trStmts₁ (trNormal Code.tail k) ⊆ trStmts₁ (trNormal Code.tail k)
cons : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.cons a_1) k) ⊆ codeSupp' (a.cons a_1) k
comp : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.comp a_1) k) ⊆ codeSupp' (a.comp a_1) k
case : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.case a_1) k) ⊆ codeSupp' (a.case a_1) k
fix : ∀ (a : Code), trStmts₁ (trNormal a.fix k) ⊆ codeSupp' a.fix k
⊢ trStmts₁ (trNormal c k) ⊆ codeSupp' c k

Tactic:
cases c
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ trStmts₁ (trNormal Code.zero' k) ⊆ trStmts₁ (trNormal Code.zero' k)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ trStmts₁ (trNormal Code.zero' k) ⊆ trStmts₁ (trNormal Code.zero' k)

Tactic:
first | rfl | exact Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ trStmts₁ (trNormal Code.succ k) ⊆ trStmts₁ (trNormal Code.succ k)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ trStmts₁ (trNormal Code.succ k) ⊆ trStmts₁ (trNormal Code.succ k)

Tactic:
first | rfl | exact Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ trStmts₁ (trNormal Code.tail k) ⊆ trStmts₁ (trNormal Code.tail k)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ trStmts₁ (trNormal Code.tail k) ⊆ trStmts₁ (trNormal Code.tail k)

Tactic:
first | rfl | exact Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a a_1 : Code
⊢ trStmts₁ (trNormal (a.cons a_1) k) ⊆ codeSupp' (a.cons a_1) k

Tactic:
Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a a_1 : Code
⊢ trStmts₁ (trNormal (a.cons a_1) k) ⊆ codeSupp' (a.cons a_1) k

Tactic:
exact Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a a_1 : Code
⊢ trStmts₁ (trNormal (a.cons a_1) k) ⊆ codeSupp' (a.cons a_1) k

Tactic:
first | rfl | exact Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a a_1 : Code
⊢ trStmts₁ (trNormal (a.comp a_1) k) ⊆ codeSupp' (a.comp a_1) k

Tactic:
Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a a_1 : Code
⊢ trStmts₁ (trNormal (a.comp a_1) k) ⊆ codeSupp' (a.comp a_1) k

Tactic:
exact Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a a_1 : Code
⊢ trStmts₁ (trNormal (a.comp a_1) k) ⊆ codeSupp' (a.comp a_1) k

Tactic:
first | rfl | exact Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a a_1 : Code
⊢ trStmts₁ (trNormal (a.case a_1) k) ⊆ codeSupp' (a.case a_1) k

Tactic:
Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a a_1 : Code
⊢ trStmts₁ (trNormal (a.case a_1) k) ⊆ codeSupp' (a.case a_1) k

Tactic:
exact Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a a_1 : Code
⊢ trStmts₁ (trNormal (a.case a_1) k) ⊆ codeSupp' (a.case a_1) k

Tactic:
first | rfl | exact Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a : Code
⊢ trStmts₁ (trNormal a.fix k) ⊆ codeSupp' a.fix k

Tactic:
Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a : Code
⊢ trStmts₁ (trNormal a.fix k) ⊆ codeSupp' a.fix k

Tactic:
exact Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
a : Code
⊢ trStmts₁ (trNormal a.fix k) ⊆ codeSupp' a.fix k

Tactic:
first | rfl | exact Finset.union_subset_left (fun _ a ↦ a)

Premises used: Finset.union_subset_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
k : Cont'
⊢ trStmts₁ (trNormal c k) ⊆ codeSupp c k

Tactic:
Finset.Subset.trans (codeSupp'_self _ _) (Finset.union_subset_left fun _ a ↦ a)

Premises used: Finset.Subset.trans, Finset.union_subset_left, Turing.PartrecToTM2.codeSupp'_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ codeSupp Code.zero' k = trStmts₁ (trNormal Code.zero' k) ∪ contSupp k

Tactic:
rfl

Premises used: Turing.PartrecToTM2.codeSupp, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ codeSupp Code.succ k = trStmts₁ (trNormal Code.succ k) ∪ contSupp k

Tactic:
rfl

Premises used: Turing.PartrecToTM2.codeSupp, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ codeSupp Code.tail k = trStmts₁ (trNormal Code.tail k) ∪ contSupp k

Tactic:
rfl

Premises used: Turing.PartrecToTM2.codeSupp, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f fs : Code
k : Cont'
⊢ codeSupp (f.cons fs) k = trStmts₁ (trNormal (f.cons fs) k) ∪ codeSupp f (Cont'.cons₁ fs k)

Tactic:
simp [codeSupp, codeSupp', contSupp, Finset.union_assoc]

Premises used: Finset.union_assoc, Turing.PartrecToTM2.contSupp, Turing.PartrecToTM2.codeSupp, Turing.PartrecToTM2.codeSupp'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
k : Cont'
simp :
  trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
⊢ codeSupp (f.comp g) k = trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k)

Tactic:
simp only [codeSupp, codeSupp', trNormal, Finset.union_assoc, contSupp]

Premises used: Finset.union_assoc, Turing.PartrecToTM2.contSupp, Turing.PartrecToTM2.codeSupp, Turing.PartrecToTM2.trNormal, Turing.PartrecToTM2.codeSupp'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
k : Cont'
rw :
  trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k ∪ contSupp k)) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
rw₁ rw₂ :
  trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k)) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
⊢ trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))

Tactic:
rw [← Finset.union_assoc _ _ (contSupp k),
    Finset.union_eq_right.2 (codeSupp'_self _ _)]

Premises used: Iff.mpr, Finset.union_assoc, Turing.PartrecToTM2.codeSupp'_self, Turing.PartrecToTM2.contSupp, Finset.union_eq_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
k : Cont'
⊢ codeSupp (f.case g) k = trStmts₁ (trNormal (f.case g) k) ∪ (codeSupp f k ∪ codeSupp g k)

Tactic:
simp [codeSupp, codeSupp', Finset.union_assoc, Finset.union_left_comm]

Premises used: Finset.union_assoc, Finset.union_left_comm, Turing.PartrecToTM2.codeSupp, Turing.PartrecToTM2.codeSupp'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont'
⊢ codeSupp f.fix k = trStmts₁ (trNormal f.fix k) ∪ codeSupp f (Cont'.fix f k)

Tactic:
simp [codeSupp, codeSupp', contSupp, Finset.union_assoc, Finset.union_left_comm,
    Finset.union_left_idem]

Premises used: Finset.union_assoc, Finset.union_left_idem, Turing.PartrecToTM2.contSupp, Finset.union_left_comm, Turing.PartrecToTM2.codeSupp, Turing.PartrecToTM2.codeSupp'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
k : Cont'
⊢ contSupp (Cont'.cons₁ fs k) =
    trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
      codeSupp fs k.cons₂

Tactic:
simp [codeSupp, contSupp]

Premises used: Turing.PartrecToTM2.contSupp, Turing.PartrecToTM2.codeSupp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ contSupp k.cons₂ = trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k

Tactic:
rfl

Premises used: Turing.PartrecToTM2.contSupp, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont'
⊢ contSupp (Cont'.comp f k) = codeSupp f k

Tactic:
rfl

Premises used: Turing.PartrecToTM2.contSupp, Turing.PartrecToTM2.codeSupp, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont'
⊢ contSupp (Cont'.fix f k) = codeSupp f (Cont'.fix f k)

Tactic:
simp +contextual [codeSupp, codeSupp', contSupp, Finset.union_assoc,
    Finset.subset_iff, -Finset.singleton_union, -Finset.union_singleton]

Premises used: Finset.union_assoc, Finset.singleton_union, Turing.PartrecToTM2.contSupp, Finset.subset_iff, Turing.PartrecToTM2.codeSupp, Finset.union_singleton, Turing.PartrecToTM2.codeSupp'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
⊢ contSupp Cont'.halt = ∅

Tactic:
rfl

Premises used: Turing.PartrecToTM2.contSupp, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
K S : Finset Λ'
q : Λ'
⊢ Supports (insert q K) S ↔ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr q) ∧ Supports K S

Tactic:
simp [Supports]

Premises used: Turing.PartrecToTM2.Supports
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
q : Λ'
⊢ Supports {q} S ↔ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr q)

Tactic:
simp [Supports]

Premises used: Turing.PartrecToTM2.Supports
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
K₁ K₂ S : Finset Λ'
⊢ Supports (K₁ ∪ K₂) S ↔ Supports K₁ S ∧ Supports K₂ S

Tactic:
simp [Supports, or_imp, forall_and]

Premises used: or_imp, Turing.PartrecToTM2.Supports, forall_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
K : Option Γ' → Finset Λ'
S : Finset Λ'
⊢ Supports (Finset.biUnion Finset.univ K) S ↔ ∀ (a : Option Γ'), Supports (K a) S

Tactic:
simpa [Supports] using forall_comm

Premises used: forall_comm, Turing.PartrecToTM2.Supports
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x : Option Γ'
pos : x = some Γ'.consₗ → Λ'.Supports S (id (unrev q))
neg : ¬x = some Γ'.consₗ → Λ'.Supports S (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) k (unrev q))
⊢ Λ'.Supports S ((if x = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) k) (unrev q))

Tactic:
split_ifs
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x : Option Γ'
h : x = some Γ'.consₗ
⊢ Λ'.Supports S (id (unrev q))

Tactic:
H

Premises used: Turing.PartrecToTM2.Λ'.Supports, Turing.PartrecToTM2.unrev
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x : Option Γ'
h : x = some Γ'.consₗ
⊢ Λ'.Supports S (id (unrev q))

Tactic:
exact H
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x : Option Γ'
h : ¬x = some Γ'.consₗ
⊢ Λ'.Supports S (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) k (unrev q))

Tactic:
H

Premises used: Turing.PartrecToTM2.Λ'.Supports, Turing.PartrecToTM2.unrev
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x : Option Γ'
h : ¬x = some Γ'.consₗ
⊢ Λ'.Supports S (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) k (unrev q))

Tactic:
exact H
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
⊢ ∀ {q : Λ'}, q ∈ trStmts₁ q

Tactic:
have W := fun {q} => trStmts₁_self q
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
H₁ : contSupp Cont'.halt ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret Cont'.halt))

Tactic:
trivial
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : contSupp (Cont'.cons₁ a a_1) ⊆ S
⊢ trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal a a_1.cons₂)))) ⊆
      S ∧
    codeSupp a a_1.cons₂ ⊆ S

Tactic:
rw [contSupp_cons₁, Finset.union_subset_iff] at H₁

Premises used: Turing.PartrecToTM2.contSupp_cons₁, Finset.union_subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ :
  trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal a a_1.cons₂)))) ⊆
      S ∧
    codeSupp a a_1.cons₂ ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.cons₁ a a_1)))

Tactic:
fun _ => H₁.1 W

Premises used: Turing.TM2.SupportsStmt, And.left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ :
  trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal a a_1.cons₂)))) ⊆
      S ∧
    codeSupp a a_1.cons₂ ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.cons₁ a a_1)))

Tactic:
exact fun _ => H₁.1 W

Premises used: And.left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Cont'
H₁ : contSupp a.cons₂ ⊆ S
⊢ trStmts₁ (head stack (Λ'.ret a)) ⊆ S ∧ contSupp a ⊆ S

Tactic:
rw [contSupp_cons₂, Finset.union_subset_iff] at H₁

Premises used: Turing.PartrecToTM2.contSupp_cons₂, Finset.union_subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Cont'
H₁ : trStmts₁ (head stack (Λ'.ret a)) ⊆ S ∧ contSupp a ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret a.cons₂))

Tactic:
fun _ => H₁.1 W

Premises used: Turing.TM2.SupportsStmt, And.left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Cont'
H₁ : trStmts₁ (head stack (Λ'.ret a)) ⊆ S ∧ contSupp a ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret a.cons₂))

Tactic:
exact fun _ => H₁.1 W

Premises used: And.left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : contSupp (Cont'.comp a a_1) ⊆ S
⊢ codeSupp a a_1 ⊆ S

Tactic:
rw [contSupp_comp] at H₁

Premises used: Turing.PartrecToTM2.contSupp_comp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a a_1 ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.comp a a_1)))

Tactic:
fun _ => H₁ (codeSupp_self _ _ W)

Premises used: Turing.TM2.SupportsStmt, Turing.PartrecToTM2.codeSupp_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a a_1 ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.comp a a_1)))

Tactic:
exact fun _ => H₁ (codeSupp_self _ _ W)

Premises used: Turing.PartrecToTM2.codeSupp_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : contSupp (Cont'.fix a a_1) ⊆ S
⊢ codeSupp a (Cont'.fix a a_1) ⊆ S

Tactic:
rw [contSupp_fix] at H₁

Premises used: Turing.PartrecToTM2.contSupp_fix
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a (Cont'.fix a a_1) ⊆ S
⊢ ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s), a ∈ s ∪ t

Tactic:
have L := @Finset.mem_union_left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a (Cont'.fix a a_1) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s), a ∈ s ∪ t
⊢ ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t), a ∈ s ∪ t

Tactic:
have R := @Finset.mem_union_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a (Cont'.fix a a_1) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s), a ∈ s ∪ t
R : ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t), a ∈ s ∪ t
s : Option Γ'
fix : (bif false then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S
fix₁ : (bif true then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S
⊢ (bif natEnd (s.getD default) then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S

Tactic:
cases natEnd (s.getD default)

Premises used: Inhabited.default, Option.getD, Turing.PartrecToTM2.natEnd
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a (Cont'.fix a a_1) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s), a ∈ s ∪ t
R : ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t), a ∈ s ∪ t
s : Option Γ'
⊢ (bif false then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S

Tactic:
H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a (Cont'.fix a a_1) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s), a ∈ s ∪ t
R : ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t), a ∈ s ∪ t
s : Option Γ'
⊢ (bif false then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S

Tactic:
refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a (Cont'.fix a a_1) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s), a ∈ s ∪ t
R : ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t), a ∈ s ∪ t
s : Option Γ'
⊢ (bif true then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S

Tactic:
H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)

Premises used: Finset.mem_singleton_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a (Cont'.fix a a_1) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s), a ∈ s ∪ t
R : ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t), a ∈ s ∪ t
s : Option Γ'
⊢ (bif true then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S

Tactic:
exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)

Premises used: Finset.mem_singleton_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
halt : ∀ (H₁ : contSupp Cont'.halt ⊆ S), TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret Cont'.halt))
cons₁ :
  ∀ (a : Code) (a_1 : Cont') (H₁ : contSupp (Cont'.cons₁ a a_1) ⊆ S),
    TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.cons₁ a a_1)))
cons₂ : ∀ (a : Cont') (H₁ : contSupp a.cons₂ ⊆ S), TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret a.cons₂))
comp :
  ∀ (a : Code) (a_1 : Cont') (H₁ : contSupp (Cont'.comp a a_1) ⊆ S),
    TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.comp a a_1)))
fix :
  ∀ (a : Code) (a_1 : Cont') (H₁ : contSupp (Cont'.fix a a_1) ⊆ S),
    TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.fix a a_1)))
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret k))

Tactic:
cases k with
  | halt => trivial
  | cons₁ => rw [contSupp_cons₁, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | cons₂ => rw [contSupp_cons₂, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | comp => rw [contSupp_comp] at H₁; exact fun _ => H₁ (codeSupp_self _ _ W)
  | fix =>
    rw [contSupp_fix] at H₁
    have L := @Finset.mem_union_left; have R := @Finset.mem_union_right
    intro s; dsimp only; cases natEnd (s.getD default)
    · refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)
    · exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)

Premises used: Turing.PartrecToTM2.contSupp_comp, Turing.PartrecToTM2.halt, Turing.PartrecToTM2.contSupp_cons₂, Turing.PartrecToTM2.contSupp_fix, Turing.PartrecToTM2.contSupp_cons₁, Finset.union_subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
q : Λ'
H₁ : Λ'.Supports S q
HS₁ : trStmts₁ q ⊆ S
⊢ ∀ {q : Λ'}, q ∈ trStmts₁ q

Tactic:
have W := fun {q} => trStmts₁_self q
-- 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₁ : trStmts₁ (Λ'.move p k₁ k₂ q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.move p k₁ k₂ q)) S

Tactic:
_
-- 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₁ : trStmts₁ (Λ'.clear p k q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.clear p k 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.copy
HS₁ : trStmts₁ q.copy ⊆ S
⊢ Supports (trStmts₁ q.copy) S

Tactic:
_