awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S

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

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

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

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

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

Tactic:
exact supports_insert.2 ⟨⟨fun _ => h₂.2 _ W, fun _ => h₂.1⟩, q_ih H₁ h₂.2⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S

Tactic:
supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₂.2 _ (Or.inl W),
                          fun _ => h₂.1, fun _ => h₂.1⟩, ?_⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, Turing.PartrecToTM2.supports_insert, Or.inl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
pred : Supports (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S

Tactic:
refine -- pred
      supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₂.2 _ (Or.inl W),
                          fun _ => h₂.1, fun _ => h₂.1⟩, ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) S

Tactic:
supports_insert.2 ⟨⟨fun _ => h₂.2 _ (Or.inr W), fun _ => h₂.1⟩, ?_⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, Turing.PartrecToTM2.supports_insert, Or.inr
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
pred : Supports (trStmts₁ q₁ ∪ trStmts₁ q₂) S
⊢ Supports (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) S

Tactic:
refine supports_insert.2 ⟨⟨fun _ => h₂.2 _ (Or.inr W), fun _ => h₂.1⟩, ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (trStmts₁ q₁ ∪ trStmts₁ q₂) S

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

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

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

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

Tactic:
q₁_ih H₁.1 fun _ h => h₂.2 _ (Or.inl h)

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

Tactic:
exact q₁_ih H₁.1 fun _ h => h₂.2 _ (Or.inl h)

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

Tactic:
q₂_ih H₁.2 fun _ h => h₂.2 _ (Or.inr h)

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

Tactic:
exact q₂_ih H₁.2 fun _ h => h₂.2 _ (Or.inr h)

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

Tactic:
supports_singleton.2 (ret_supports H₁)

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

Tactic:
exact supports_singleton.2 (ret_supports H₁)

Premises used: Iff.mpr, Turing.PartrecToTM2.ret_supports, Turing.PartrecToTM2.supports_singleton
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
q : Λ'
K : Finset Λ'
H₁ : Λ'.Supports S q
H₂ : trStmts₁ q ∪ K ⊆ S
H₃ : K ⊆ S → Supports K S
⊢ trStmts₁ q ⊆ S ∧ K ⊆ S

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

Premises used: Finset.union_subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
q : Λ'
K : Finset Λ'
H₁ : Λ'.Supports S q
H₃ : K ⊆ S → Supports K S
H₂ : trStmts₁ q ⊆ S ∧ K ⊆ S
⊢ Supports (trStmts₁ q ∪ K) S

Tactic:
supports_union.2 ⟨trStmts₁_supports H₁ H₂.1, H₃ H₂.2⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, Turing.PartrecToTM2.trStmts₁_supports, And.right, And.left, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
q : Λ'
K : Finset Λ'
H₁ : Λ'.Supports S q
H₃ : K ⊆ S → Supports K S
H₂ : trStmts₁ q ⊆ S ∧ K ⊆ S
⊢ Supports (trStmts₁ q ∪ K) S

Tactic:
exact supports_union.2 ⟨trStmts₁_supports H₁ H₂.1, H₃ H₂.2⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, Turing.PartrecToTM2.trStmts₁_supports, And.right, And.left, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.zero' k ⊆ S
⊢ contSupp k ⊆ S

Tactic:
Finset.union_subset_right Hk

Premises used: Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.zero' k ⊆ S
⊢ contSupp k ⊆ S

Tactic:
exact Finset.union_subset_right Hk

Premises used: Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
s : Option Γ'
pos : s = some Γ'.consₗ → Λ'.Supports S (id (unrev (Λ'.ret k).succ))
neg : ¬s = some Γ'.consₗ → Λ'.Supports S (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main (unrev (Λ'.ret k).succ))
⊢ Λ'.Supports S
    ((if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main) (unrev (Λ'.ret k).succ))

Tactic:
split_ifs
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
s : Option Γ'
h : s = some Γ'.consₗ
⊢ Λ'.Supports S (id (unrev (Λ'.ret k).succ))

Tactic:
Finset.union_subset_right Hk

Premises used: Turing.PartrecToTM2.Λ'.Supports, Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
s : Option Γ'
h : s = some Γ'.consₗ
⊢ Λ'.Supports S (id (unrev (Λ'.ret k).succ))

Tactic:
exact Finset.union_subset_right Hk

Premises used: Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
s : Option Γ'
h : ¬s = some Γ'.consₗ
⊢ Λ'.Supports S (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main (unrev (Λ'.ret k).succ))

Tactic:
Finset.union_subset_right Hk

Premises used: Turing.PartrecToTM2.Λ'.Supports, Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
s : Option Γ'
h : ¬s = some Γ'.consₗ
⊢ Λ'.Supports S (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main (unrev (Λ'.ret k).succ))

Tactic:
exact Finset.union_subset_right Hk

Premises used: Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.tail k ⊆ S
⊢ contSupp k ⊆ S

Tactic:
Finset.union_subset_right Hk

Premises used: Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.tail k ⊆ S
⊢ contSupp k ⊆ S

Tactic:
exact Finset.union_subset_right Hk

Premises used: Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
a_ih : ∀ {k : Cont'} (Hk : codeSupp fs k ⊆ S), Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (f.cons fs) k ⊆ S
cons : Λ'.Supports S (trNormal f (Cont'.cons₁ fs k))
⊢ Λ'.Supports S (trNormal (f.cons fs) k)

Tactic:
simp [Λ'.Supports, head]

Premises used: Turing.PartrecToTM2.Λ'.Supports, Turing.PartrecToTM2.head
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
a_ih : ∀ {k : Cont'} (Hk : codeSupp fs k ⊆ S), Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (f.cons fs) k ⊆ S
cons : codeSupp f (Cont'.cons₁ fs k) ⊆ S
⊢ Λ'.Supports S (trNormal f (Cont'.cons₁ fs k))

Tactic:
apply IHf
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
a_ih : ∀ {k : Cont'} (Hk : codeSupp fs k ⊆ S), Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (f.cons fs) k ⊆ S
⊢ trStmts₁ (trNormal (f.cons fs) k) ∪ codeSupp f (Cont'.cons₁ fs k) ⊆ S

Tactic:
rw [codeSupp_cons] at Hk

Premises used: Turing.PartrecToTM2.codeSupp_cons
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
a_ih : ∀ {k : Cont'} (Hk : codeSupp fs k ⊆ S), Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : trStmts₁ (trNormal (f.cons fs) k) ∪ codeSupp f (Cont'.cons₁ fs k) ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S

Tactic:
Finset.union_subset_right Hk

Premises used: Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
a_ih : ∀ {k : Cont'} (Hk : codeSupp fs k ⊆ S), Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : trStmts₁ (trNormal (f.cons fs) k) ∪ codeSupp f (Cont'.cons₁ fs k) ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S

Tactic:
exact Finset.union_subset_right Hk

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

Tactic:
simp [Λ'.Supports, head]

Premises used: Turing.PartrecToTM2.Λ'.Supports, Turing.PartrecToTM2.head
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
a_ih : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'} (Hk : codeSupp g k ⊆ S), Λ'.Supports S (trNormal g k)
k : Cont'
Hk : codeSupp (f.comp g) k ⊆ S
comp : codeSupp g (Cont'.comp f k) ⊆ S
⊢ Λ'.Supports S (trNormal g (Cont'.comp f k))

Tactic:
apply IHg
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
a_ih : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'} (Hk : codeSupp g k ⊆ S), Λ'.Supports S (trNormal g k)
k : Cont'
Hk : codeSupp (f.comp g) k ⊆ S
⊢ trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S

Tactic:
rw [codeSupp_comp] at Hk

Premises used: Turing.PartrecToTM2.codeSupp_comp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
a_ih : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'} (Hk : codeSupp g k ⊆ S), Λ'.Supports S (trNormal g k)
k : Cont'
Hk : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
⊢ codeSupp g (Cont'.comp f k) ⊆ S

Tactic:
Finset.union_subset_right Hk

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

Tactic:
exact Finset.union_subset_right Hk

Premises used: Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'} (Hk : codeSupp g k ⊆ S), Λ'.Supports S (trNormal g k)
k : Cont'
Hk : 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 Hk

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

Tactic:
⟨IHf Hk.2.1, IHg Hk.2.2⟩

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

Tactic:
exact ⟨IHf Hk.2.1, IHg Hk.2.2⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
k : Cont'
Hk : codeSupp f.fix k ⊆ S
fix : Λ'.Supports S (trNormal f (Cont'.fix f k))
⊢ Λ'.Supports S (trNormal f.fix k)

Tactic:
simp [Λ'.Supports, head]

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

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

Tactic:
rw [codeSupp_fix] at Hk

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

Tactic:
Finset.union_subset_right Hk

Premises used: Finset.union_subset_right
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
k : Cont'
Hk : trStmts₁ (trNormal f.fix k) ∪ codeSupp f (Cont'.fix f k) ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S

Tactic:
exact Finset.union_subset_right Hk

Premises used: Finset.union_subset_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
⊢ codeSupp (f.cons fs) k ⊆ S

Tactic:
have H' := H
-- 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 H' : codeSupp (f.cons fs) k ⊆ S
⊢ trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S

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

Premises used: Turing.PartrecToTM2.codeSupp_cons, 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 : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
⊢ Supports (codeSupp' (f.cons fs) 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 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
cons :
  ∀
    (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
⊢ Supports (codeSupp' (f.cons fs) 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'