awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'} (H : codeSupp g k ⊆ S), Supports (codeSupp' g k) S
k : Cont'
H'_1 : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ⊆ S ∧ trStmts₁ (trNormal f k) ⊆ S ∧ codeSupp' f k ⊆ S
H :
  (trStmts₁ (trNormal (f.comp g) k) ⊆ S ∧
      codeSupp' g (Cont'.comp f k) ⊆ S ∧ trStmts₁ (trNormal f k) ⊆ S ∧ codeSupp' f k ⊆ S) ∧
    contSupp k ⊆ S
⊢ codeSupp' f k ⊆ S ∧ contSupp k ⊆ S

Tactic:
⟨h.2.2, H.2⟩

Premises used: And.right, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'} (H : codeSupp g k ⊆ S), Supports (codeSupp' g k) S
k : Cont'
H'_1 : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ⊆ S ∧ trStmts₁ (trNormal f k) ⊆ S ∧ codeSupp' f k ⊆ S
H :
  (trStmts₁ (trNormal (f.comp g) k) ⊆ S ∧
      codeSupp' g (Cont'.comp f k) ⊆ S ∧ trStmts₁ (trNormal f k) ⊆ S ∧ codeSupp' f k ⊆ S) ∧
    contSupp k ⊆ S
⊢ codeSupp' f k ⊆ S ∧ contSupp k ⊆ S

Tactic:
exact ⟨h.2.2, H.2⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'} (H : codeSupp g k ⊆ S), Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.comp g) k ⊆ S
H'_1 : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S
h_1 : codeSupp' f k ⊆ S
⊢ Supports (codeSupp' f k) S

Tactic:
IHf (Finset.union_subset_right H')

Premises used: Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'} (H : codeSupp g k ⊆ S), Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.comp g) k ⊆ S
H'_1 : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S
h_1 : codeSupp' f k ⊆ S
⊢ Supports (codeSupp' f k) S

Tactic:
exact IHf (Finset.union_subset_right H')

Premises used: Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'} (H : codeSupp g k ⊆ S), Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.case g) k ⊆ S
⊢ codeSupp (f.case g) k ⊆ S

Tactic:
have H' := H
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'} (H : codeSupp g k ⊆ S), Supports (codeSupp' g k) S
k : Cont'
H H' : codeSupp (f.case g) k ⊆ S
⊢ trStmts₁ (trNormal (f.case g) k) ⊆ S ∧ codeSupp f k ⊆ S ∧ codeSupp g k ⊆ S

Tactic:
simp only [codeSupp_case, Finset.union_subset_iff] at H'

Premises used: Turing.PartrecToTM2.codeSupp_case, Finset.union_subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'} (H : codeSupp g k ⊆ S), Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.case g) k ⊆ S
H' : trStmts₁ (trNormal (f.case g) k) ⊆ S ∧ codeSupp f k ⊆ S ∧ codeSupp g k ⊆ S
⊢ Supports (codeSupp' (f.case g) k) S

Tactic:
trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun _ => ?_

Premises used: Finset.union_subset_left, Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports', Turing.PartrecToTM2.codeSupp'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'} (H : codeSupp g k ⊆ S), Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.case g) k ⊆ S
H' : trStmts₁ (trNormal (f.case g) k) ⊆ S ∧ codeSupp f k ⊆ S ∧ codeSupp g k ⊆ S
case : codeSupp' f k ∪ codeSupp' g k ⊆ S → Supports (codeSupp' f k ∪ codeSupp' g k) S
⊢ Supports (codeSupp' (f.case g) k) S

Tactic:
refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun _ => ?_

Premises used: Finset.union_subset_left, Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'} (H : codeSupp g k ⊆ S), Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.case g) k ⊆ S
H' : trStmts₁ (trNormal (f.case g) k) ⊆ S ∧ codeSupp f k ⊆ S ∧ codeSupp g k ⊆ S
h : codeSupp' f k ∪ codeSupp' g k ⊆ S
⊢ Supports (codeSupp' f k ∪ codeSupp' g k) S

Tactic:
supports_union.2 ⟨IHf H'.2.1, IHg H'.2.2⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, And.right, And.left, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'} (H : codeSupp g k ⊆ S), Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.case g) k ⊆ S
H' : trStmts₁ (trNormal (f.case g) k) ⊆ S ∧ codeSupp f k ⊆ S ∧ codeSupp g k ⊆ S
h : codeSupp' f k ∪ codeSupp' g k ⊆ S
⊢ Supports (codeSupp' f k ∪ codeSupp' g k) S

Tactic:
exact supports_union.2 ⟨IHf H'.2.1, IHg H'.2.2⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, And.right, And.left, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
⊢ codeSupp f.fix k ⊆ S

Tactic:
have H' := H
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H H' : codeSupp f.fix k ⊆ S
⊢ trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S

Tactic:
simp only [codeSupp_fix, Finset.union_subset_iff] at H'

Premises used: Turing.PartrecToTM2.codeSupp_fix, Finset.union_subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
⊢ Supports (codeSupp' f.fix k) S

Tactic:
trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_

Premises used: Finset.union_subset_left, Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports', Turing.PartrecToTM2.codeSupp'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
fix :
  ∀ (h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S),
    Supports (codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}))
      S
⊢ Supports (codeSupp' f.fix k) S

Tactic:
refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_

Premises used: Finset.union_subset_left, Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
⊢ Supports (codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k})) S

Tactic:
supports_union.2 ⟨IHf H'.2, ?_⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, And.right, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
fix : Supports (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) S
⊢ Supports (codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k})) S

Tactic:
refine supports_union.2 ⟨IHf H'.2, ?_⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, And.right, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
⊢ Supports (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) S

Tactic:
trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_

Premises used: Turing.PartrecToTM2.trNormal_supports, Finset.union_subset_right, Turing.PartrecToTM2.trStmts₁_supports'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
fix : codeSupp f (Cont'.fix f k) ⊆ S
fix₁ : {Λ'.ret k} ⊆ S → Supports {Λ'.ret k} S
⊢ Supports (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) S

Tactic:
refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_

Premises used: Turing.PartrecToTM2.trNormal_supports, Finset.union_subset_right, Turing.PartrecToTM2.trStmts₁_supports'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
fix :
  ∀
    (h :
      codeSupp' f (Cont'.fix f k) ⊆ S ∧
        (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
          {Λ'.ret k} ⊆ S)
    (H :
      (trStmts₁ (trNormal f.fix k) ⊆ S ∧
          codeSupp' f (Cont'.fix f k) ⊆ S ∧
            (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
              {Λ'.ret k} ⊆ S) ∧
        contSupp k ⊆ S),
    codeSupp' f (Cont'.fix f k) ⊆ S ∧
      (trStmts₁ (trNormal f.fix k) ⊆ S ∧
          codeSupp' f (Cont'.fix f k) ⊆ S ∧
            (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
              {Λ'.ret k} ⊆ S) ∧
        contSupp k ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S

Tactic:
simp only [codeSupp', codeSupp, Finset.union_subset_iff, contSupp, trStmts₁,
        Finset.insert_subset_iff] at h H ⊢

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.insert_subset_iff, Turing.PartrecToTM2.contSupp, Turing.PartrecToTM2.codeSupp, Finset.union_subset_iff, Turing.PartrecToTM2.codeSupp'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h :
  codeSupp' f (Cont'.fix f k) ⊆ S ∧
    (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧ {Λ'.ret k} ⊆ S
H :
  (trStmts₁ (trNormal f.fix k) ⊆ S ∧
      codeSupp' f (Cont'.fix f k) ⊆ S ∧
        (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
          {Λ'.ret k} ⊆ S) ∧
    contSupp k ⊆ S
⊢ codeSupp' f (Cont'.fix f k) ⊆ S ∧
    (trStmts₁ (trNormal f.fix k) ⊆ S ∧
        codeSupp' f (Cont'.fix f k) ⊆ S ∧
          (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
            {Λ'.ret k} ⊆ S) ∧
      contSupp k ⊆ S

Tactic:
⟨h.1, ⟨H.1.1, h⟩, H.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h :
  codeSupp' f (Cont'.fix f k) ⊆ S ∧
    (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧ {Λ'.ret k} ⊆ S
H :
  (trStmts₁ (trNormal f.fix k) ⊆ S ∧
      codeSupp' f (Cont'.fix f k) ⊆ S ∧
        (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
          {Λ'.ret k} ⊆ S) ∧
    contSupp k ⊆ S
⊢ codeSupp' f (Cont'.fix f k) ⊆ S ∧
    (trStmts₁ (trNormal f.fix k) ⊆ S ∧
        codeSupp' f (Cont'.fix f k) ⊆ S ∧
          (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
            {Λ'.ret k} ⊆ S) ∧
      contSupp k ⊆ S

Tactic:
exact ⟨h.1, ⟨H.1.1, h⟩, H.2⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
h_1 : {Λ'.ret k} ⊆ S
⊢ Supports {Λ'.ret k} S

Tactic:
supports_singleton.2 (ret_supports <| Finset.union_subset_right H)

Premises used: Iff.mpr, Turing.PartrecToTM2.ret_supports, Turing.PartrecToTM2.supports_singleton, Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
h_1 : {Λ'.ret k} ⊆ S
⊢ Supports {Λ'.ret k} S

Tactic:
exact supports_singleton.2 (ret_supports <| Finset.union_subset_right H)

Premises used: Iff.mpr, Turing.PartrecToTM2.ret_supports, Turing.PartrecToTM2.supports_singleton, Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
H : codeSupp Code.zero' k ⊆ S
⊢ Supports (codeSupp' Code.zero' k) S

Tactic:
trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H)

Premises used: Turing.PartrecToTM2.codeSupp_self, Finset.Subset.trans, Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports, Turing.PartrecToTM2.codeSupp'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
H : codeSupp Code.zero' k ⊆ S
⊢ Supports (codeSupp' Code.zero' k) S

Tactic:
exact trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H)

Premises used: Turing.PartrecToTM2.codeSupp_self, Finset.Subset.trans, Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
H : codeSupp Code.succ k ⊆ S
⊢ Supports (codeSupp' Code.succ k) S

Tactic:
trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H)

Premises used: Turing.PartrecToTM2.codeSupp_self, Finset.Subset.trans, Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports, Turing.PartrecToTM2.codeSupp'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
H : codeSupp Code.succ k ⊆ S
⊢ Supports (codeSupp' Code.succ k) S

Tactic:
exact trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H)

Premises used: Turing.PartrecToTM2.codeSupp_self, Finset.Subset.trans, Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
H : codeSupp Code.tail k ⊆ S
⊢ Supports (codeSupp' Code.tail k) S

Tactic:
trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H)

Premises used: Turing.PartrecToTM2.codeSupp_self, Finset.Subset.trans, Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports, Turing.PartrecToTM2.codeSupp'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
H : codeSupp Code.tail k ⊆ S
⊢ Supports (codeSupp' Code.tail k) S

Tactic:
exact trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H)

Premises used: Turing.PartrecToTM2.codeSupp_self, Finset.Subset.trans, Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
H : contSupp Cont'.halt ⊆ S
⊢ Supports (contSupp Cont'.halt) S

Tactic:
simp [contSupp_halt, Supports]

Premises used: Turing.PartrecToTM2.contSupp_halt, Turing.PartrecToTM2.Supports
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
⊢ contSupp (Cont'.cons₁ f k) ⊆ S

Tactic:
have H₁ := H
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H H₁ : contSupp (Cont'.cons₁ f k) ⊆ S
⊢ trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S

Tactic:
rw [contSupp_cons₁] at H₁

Premises used: Turing.PartrecToTM2.contSupp_cons₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
⊢ codeSupp f k.cons₂ ⊆ S

Tactic:
have H₂ := Finset.union_subset_right H₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
H₂ : codeSupp f k.cons₂ ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S

Tactic:
trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => ?_

Premises used: Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports', Turing.PartrecToTM2.contSupp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
H₂ : codeSupp f k.cons₂ ⊆ S
cons₁ :
  ∀ (h : codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S),
    Supports (codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k)) S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S

Tactic:
refine trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => ?_

Premises used: Turing.PartrecToTM2.trNormal_supports, Turing.PartrecToTM2.trStmts₁_supports'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
H₂ : codeSupp f k.cons₂ ⊆ S
h : codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
⊢ Supports (codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k)) S

Tactic:
supports_union.2 ⟨codeSupp'_supports H₂, ?_⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, Turing.PartrecToTM2.codeSupp'_supports, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
H₂ : codeSupp f k.cons₂ ⊆ S
h : codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
cons₁ : Supports (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) S
⊢ Supports (codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k)) S

Tactic:
refine supports_union.2 ⟨codeSupp'_supports H₂, ?_⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, Turing.PartrecToTM2.codeSupp'_supports, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
H₂ : codeSupp f k.cons₂ ⊆ S
h : codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
⊢ codeSupp' f k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S ∧ contSupp k ⊆ S

Tactic:
simp only [codeSupp, contSupp_cons₂, Finset.union_subset_iff] at H₂

Premises used: Turing.PartrecToTM2.contSupp_cons₂, Turing.PartrecToTM2.codeSupp, Finset.union_subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
h : codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
H₂ : codeSupp' f k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S ∧ contSupp k ⊆ S
⊢ Supports (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) S

Tactic:
trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH

Premises used: Finset.union_subset_right, Turing.PartrecToTM2.trStmts₁_supports', Turing.PartrecToTM2.head_supports, And.right