-- Mathlib/Computability/TMToPartrec.lean
theorem trNormal_supports {S c k} (Hk : codeSupp c k ⊆ S) : (trNormal c k).Supports S

Proof state:
case tail
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.tail k ⊆ S
⊢ contSupp k ⊆ S

Tactic:
exact Finset.union_subset_right Hk

Result:
no goals

Proof state:
case fix
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, 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))

Tactic:
apply IHf

Result:
case fix.Hk
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
k : Cont'
Hk : codeSupp f.fix k ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S

Proof state:
case fix.Hk
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, 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

Result:
no goals

Proof state:
case zero'
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.zero' k ⊆ S
⊢ contSupp k ⊆ S

Tactic:
exact Finset.union_subset_right Hk

Result:
no goals

Proof state:
S : Finset Λ'
c : Code
k : Cont'
Hk : codeSupp c k ⊆ S
⊢ Λ'.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

Result:
no goals

Proof state:
case cons.Hk
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (f.cons fs) k ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S

Tactic:
rw [codeSupp_cons] at Hk

Result:
case cons.Hk
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, 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

Proof state:
case comp.Hk
S : Finset Λ'
f g : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, 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

Result:
no goals

Proof state:
case case
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, 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⟩

Result:
no goals

Proof state:
case cons.Hk
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, 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

Result:
no goals

Proof state:
case comp.Hk
S : Finset Λ'
f g : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : codeSupp (f.comp g) k ⊆ S
⊢ codeSupp g (Cont'.comp f k) ⊆ S

Tactic:
rw [codeSupp_comp] at Hk

Result:
case comp.Hk
S : Finset Λ'
f g : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, 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

Proof state:
case succ
S : Finset Λ'
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))

Tactic:
intro

Result:
case succ
S : Finset Λ'
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))

Proof state:
case case
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, 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)

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

Result:
case case
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, 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)

Proof state:
case succ
S : Finset Λ'
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))

Tactic:
split_ifs <;> exact Finset.union_subset_right Hk

Result:
no goals

Proof state:
case cons
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, 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))

Tactic:
apply IHf

Result:
case cons.Hk
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (f.cons fs) k ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S

Proof state:
case fix.Hk
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
k : Cont'
Hk : codeSupp f.fix k ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S

Tactic:
rw [codeSupp_fix] at Hk

Result:
case fix.Hk
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, 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

Proof state:
case comp
S : Finset Λ'
f g : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, 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))

Tactic:
apply IHg

Result:
case comp.Hk
S : Finset Λ'
f g : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : codeSupp (f.comp g) k ⊆ S
⊢ codeSupp g (Cont'.comp f k) ⊆ S