awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
⊢ Supports
    (codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.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 fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
cons :
  Supports
    (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₂ ∪ trStmts₁ (head stack (Λ'.ret k))))
    S
⊢ Supports
    (codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.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 fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
⊢ Supports
    (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₂ ∪ trStmts₁ (head stack (Λ'.ret k))))
    S

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

Premises used: Turing.PartrecToTM2.trNormal_supports, Finset.union_subset_right, Turing.PartrecToTM2.trStmts₁_supports'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
cons :
  ∀
    (h :
      codeSupp' f (Cont'.cons₁ fs k) ⊆ S ∧
        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₂)))) ⊆
            S ∧
          codeSupp' fs k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S)
    (H : codeSupp' (f.cons fs) k ⊆ S ∧ contSupp k ⊆ S),
    codeSupp' fs k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S ∧ contSupp k ⊆ S
⊢ codeSupp fs k.cons₂ ⊆ S

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

Premises used: Turing.PartrecToTM2.contSupp, Turing.PartrecToTM2.codeSupp, Finset.union_subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h :
  codeSupp' f (Cont'.cons₁ fs k) ⊆ S ∧
    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₂)))) ⊆
        S ∧
      codeSupp' fs k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
H : codeSupp' (f.cons fs) k ⊆ S ∧ contSupp k ⊆ S
⊢ codeSupp' fs k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S ∧ contSupp k ⊆ S

Tactic:
⟨h.2.2.1, h.2.2.2, H.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h :
  codeSupp' f (Cont'.cons₁ fs k) ⊆ S ∧
    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₂)))) ⊆
        S ∧
      codeSupp' fs k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
H : codeSupp' (f.cons fs) k ⊆ S ∧ contSupp k ⊆ S
⊢ codeSupp' fs k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S ∧ contSupp k ⊆ S

Tactic:
exact ⟨h.2.2.1, h.2.2.2, H.2⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h_1 :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ Supports (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k))) S

Tactic:
supports_union.2 ⟨IHfs ?_, ?_⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h_1 :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
cons : codeSupp fs k.cons₂ ⊆ S
cons₁ : Supports (trStmts₁ (head stack (Λ'.ret k))) S
⊢ Supports (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k))) S

Tactic:
refine supports_union.2 ⟨IHfs ?_, ?_⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h_1 :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧
    codeSupp' f (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₂) ⊆
      S

Tactic:
rw [codeSupp, contSupp_cons₁] at H'

Premises used: Turing.PartrecToTM2.codeSupp, Turing.PartrecToTM2.contSupp_cons₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h_1 :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
H'₁ :
  trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧
    codeSupp' f (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₂) ⊆
      S
⊢ codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S

Tactic:
rw [codeSupp, contSupp_cons₁] at H'

Premises used: Turing.PartrecToTM2.codeSupp, Turing.PartrecToTM2.contSupp_cons₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h_1 :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
H'₁ :
  trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧
    codeSupp' f (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₂) ⊆
      S
h₁ :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
⊢ codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S

Tactic:
rw [codeSupp, contSupp_cons₁] at H'

Premises used: Turing.PartrecToTM2.codeSupp, Turing.PartrecToTM2.contSupp_cons₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' :
  trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧
    codeSupp' f (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₂) ⊆
      S
h_1 :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ codeSupp fs k.cons₂ ⊆ S

Tactic:
Finset.union_subset_right (Finset.union_subset_right H'.2)

Premises used: Finset.union_subset_right, And.right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' :
  trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧
    codeSupp' f (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₂) ⊆
      S
h_1 :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ codeSupp fs k.cons₂ ⊆ S

Tactic:
exact Finset.union_subset_right (Finset.union_subset_right H'.2)

Premises used: Finset.union_subset_right, And.right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h_1 :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ Supports (trStmts₁ (head stack (Λ'.ret k))) S

Tactic:
trStmts₁_supports (head_supports <| Finset.union_subset_right H)
        (Finset.union_subset_right h)

Premises used: Finset.union_subset_right, Turing.PartrecToTM2.trStmts₁_supports, Turing.PartrecToTM2.head_supports
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'} (H : codeSupp fs k ⊆ S), Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h_1 :
  codeSupp' f (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₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ Supports (trStmts₁ (head stack (Λ'.ret k))) S

Tactic:
exact
      trStmts₁_supports (head_supports <| Finset.union_subset_right H)
        (Finset.union_subset_right 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 : codeSupp (f.comp g) k ⊆ S
⊢ codeSupp (f.comp 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.comp g) k ⊆ S
⊢ trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S

Tactic:
rw [codeSupp_comp] at H'

Premises used: Turing.PartrecToTM2.codeSupp_comp
-- 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' : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
⊢ codeSupp g (Cont'.comp f k) ⊆ S

Tactic:
have H' := Finset.union_subset_right 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 : 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
⊢ Supports (codeSupp' (f.comp g) 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 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
comp :
  ∀ (h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S),
    Supports (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k)) S
⊢ Supports (codeSupp' (f.comp g) 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 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
⊢ Supports (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k)) S

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

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, 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.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
comp : Supports (trStmts₁ (trNormal f k) ∪ codeSupp' f k) S
⊢ Supports (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k)) S

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

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, 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.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
⊢ Supports (trStmts₁ (trNormal f k) ∪ codeSupp' f 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 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
comp : codeSupp f k ⊆ S
comp₁ : codeSupp' f k ⊆ S → Supports (codeSupp' f k) S
⊢ Supports (trStmts₁ (trNormal f k) ∪ codeSupp' f 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 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
comp :
  ∀ (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
⊢ codeSupp f k ⊆ S

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

Premises used: Turing.PartrecToTM2.codeSupp, Finset.union_subset_iff, Turing.PartrecToTM2.codeSupp'