-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
c : Code
k : Cont'
Hk : codeSupp c k ⊆ S
zero' : ∀ {k : Cont'} (Hk : codeSupp Code.zero' k ⊆ S), Λ'.Supports S (trNormal Code.zero' k)
zero'₁ : ∀ {k : Cont'} (Hk : codeSupp Code.zero' k ⊆ S), contSupp k ⊆ S
succ : ∀ {k : Cont'} (Hk : codeSupp Code.succ k ⊆ S), Λ'.Supports S (trNormal Code.succ k)
succ₁ :
  ∀ {k : Cont'} (Hk : codeSupp Code.succ k ⊆ S) (s : Option Γ'),
    Λ'.Supports S
      ((if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main) (unrev (Λ'.ret k).succ))
tail : ∀ {k : Cont'} (Hk : codeSupp Code.tail k ⊆ S), Λ'.Supports S (trNormal Code.tail k)
tail₁ : ∀ {k : Cont'} (Hk : codeSupp Code.tail k ⊆ S), contSupp k ⊆ S
cons :
  ∀ (f fs : Code) (IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)),
    (∀ {k : Cont'} (Hk : codeSupp fs k ⊆ S), Λ'.Supports S (trNormal fs k)) →
      ∀ {k : Cont'} (Hk : codeSupp (f.cons fs) k ⊆ S), Λ'.Supports S (trNormal (f.cons fs) k)
cons₁ :
  ∀ (f fs : Code) (IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)),
    (∀ {k : Cont'} (Hk : codeSupp fs k ⊆ S), Λ'.Supports S (trNormal fs k)) →
      ∀ {k : Cont'} (Hk : codeSupp (f.cons fs) k ⊆ S), Λ'.Supports S (trNormal f (Cont'.cons₁ fs k))
comp :
  ∀ (f g : Code),
    (∀ {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), Λ'.Supports S (trNormal (f.comp g) k)
comp₁ :
  ∀ (f g : Code),
    (∀ {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), Λ'.Supports S (trNormal g (Cont'.comp f k))
case :
  ∀ (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), Λ'.Supports S (trNormal (f.case g) k)
case₁ :
  ∀ (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), Λ'.Supports S (trNormal f k) ∧ Λ'.Supports S (trNormal g k)
fix :
  ∀ (f : Code) (IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)) {k : Cont'}
    (Hk : codeSupp f.fix k ⊆ S), Λ'.Supports S (trNormal f.fix k)
fix₁ :
  ∀ (f : Code) (IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)) {k : Cont'}
    (Hk : codeSupp f.fix k ⊆ S), Λ'.Supports S (trNormal f (Cont'.fix f k))
⊢ Λ'.Supports S (trNormal c k)

Tactic:
induction c generalizing k with simp [Λ'.Supports, head]
  | zero' => exact Finset.union_subset_right Hk
  | succ => intro; split_ifs <;> exact Finset.union_subset_right Hk
  | tail => exact Finset.union_subset_right Hk
  | cons f fs IHf _ =>
    apply IHf
    rw [codeSupp_cons] at Hk
    exact Finset.union_subset_right Hk
  | comp f g _ IHg => apply IHg; rw [codeSupp_comp] at Hk; exact Finset.union_subset_right Hk
  | case f g IHf IHg =>
    simp only [codeSupp_case, Finset.union_subset_iff] at Hk
    exact ⟨IHf Hk.2.1, IHg Hk.2.2⟩
  | fix f IHf => apply IHf; rw [codeSupp_fix] at Hk; exact Finset.union_subset_right Hk

Premises used: Turing.PartrecToTM2.Λ'.Supports, Finset.union_subset_right, Turing.PartrecToTM2.codeSupp_fix, Turing.PartrecToTM2.codeSupp_case, Turing.PartrecToTM2.head, Turing.PartrecToTM2.codeSupp_cons, Finset.union_subset_iff, Turing.PartrecToTM2.codeSupp_comp