-- Mathlib/Computability/TMToPartrec.lean
theorem contSupp_supports {S k} (H : contSupp k ⊆ S) : Supports (contSupp k) S

Proof state:
S : Finset Λ'
k : Cont'
H : contSupp k ⊆ S
⊢ Supports (contSupp k) S

Tactic:
induction k with
| halt => simp [contSupp_halt, Supports]
| cons₁ f k IH =>
  have H₁ := H; rw [contSupp_cons₁] at H₁; have H₂ := Finset.union_subset_right H₁
  refine trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => ?_
  refine supports_union.2 ⟨codeSupp'_supports H₂, ?_⟩
  simp only [codeSupp, contSupp_cons₂, Finset.union_subset_iff] at H₂
  exact trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH
| cons₂ k IH =>
  have H' := H; rw [contSupp_cons₂] at H'
  exact trStmts₁_supports' (head_supports <| Finset.union_subset_right H') H' IH
| comp f k IH =>
  have H' := H; rw [contSupp_comp] at H'; have H₂ := Finset.union_subset_right H'
  exact supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩
| fix f k IH =>
  rw [contSupp] at H
  exact supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩

Result:
no goals

Proof state:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : 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:
refine trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => ?_

Result:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : 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

Proof state:
case halt
S : Finset Λ'
H : contSupp Cont'.halt ⊆ S
⊢ Supports (contSupp Cont'.halt) S

Tactic:
simp [contSupp_halt, Supports]

Result:
no goals

Proof state:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : 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
⊢ Supports (contSupp (Cont'.cons₁ f k)) S

Tactic:
have H₂ := Finset.union_subset_right H₁

Result:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : 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

Proof state:
case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H' : contSupp (Cont'.comp f k) ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Tactic:
rw [contSupp_comp] at H'

Result:
case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Proof state:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : 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:
exact trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH

Result:
no goals

Proof state:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : 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 (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) S

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

Result:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : 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

Proof state:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S

Tactic:
have H₁ := H

Result:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H₁ : contSupp (Cont'.cons₁ f k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S

Proof state:
case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Tactic:
have H' := H

Result:
case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H' : contSupp (Cont'.comp f k) ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Proof state:
case fix
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.fix f k) ⊆ S
⊢ Supports (contSupp (Cont'.fix f k)) S

Tactic:
rw [contSupp] at H

Result:
case fix
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : codeSupp' f.fix k ∪ contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.fix f k)) S

Proof state:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H₁ : contSupp (Cont'.cons₁ f k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S

Tactic:
rw [contSupp_cons₁] at H₁

Result:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : 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
⊢ Supports (contSupp (Cont'.cons₁ f k)) S

Proof state:
case cons₂
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp k.cons₂ ⊆ S
⊢ Supports (contSupp k.cons₂) S

Tactic:
have H' := H

Result:
case cons₂
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H' : contSupp k.cons₂ ⊆ S
⊢ Supports (contSupp k.cons₂) S