-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
c : Code
k : Cont'
H : codeSupp c k ⊆ S
cons :
  ∀ (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), Supports (codeSupp' (f.cons fs) k) S
comp :
  ∀ (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), Supports (codeSupp' (f.comp g) k) S
case :
  ∀ (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.case g) k ⊆ S), Supports (codeSupp' (f.case g) k) S
fix :
  ∀ (f : Code) (IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S) {k : Cont'}
    (H : codeSupp f.fix k ⊆ S), Supports (codeSupp' f.fix k) S
zero' : ∀ {k : Cont'} (H : codeSupp Code.zero' k ⊆ S), Supports (codeSupp' Code.zero' k) S
succ : ∀ {k : Cont'} (H : codeSupp Code.succ k ⊆ S), Supports (codeSupp' Code.succ k) S
⊢ Supports (codeSupp' c k) S
have tail : ∀ {k : Cont'} (H : codeSupp Code.tail k ⊆ S), Supports (codeSupp' Code.tail k) S
Tactic: induction c generalizing k with
  | cons f fs IHf IHfs =>
    have H' := H; simp only [codeSupp_cons, Finset.union_subset_iff] at H'
    refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_
    refine supports_union.2 ⟨IHf H'.2, ?_⟩
    refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun h => ?_
    · simp only [codeSupp, Finset.union_subset_iff, contSupp] at h H ⊢
      exact ⟨h.2.2.1, h.2.2.2, H.2⟩
    refine supports_union.2 ⟨IHfs ?_, ?_⟩
    · rw [codeSupp, contSupp_cons₁] at H'
      exact Finset.union_subset_right (Finset.union_subset_right H'.2)
    exact
      trStmts₁_supports (head_supports <| Finset.union_subset_right H)
        (Finset.union_subset_right h)
  | comp f g IHf IHg =>
    have H' := H; rw [codeSupp_comp] at H'; have H' := Finset.union_subset_right H'
    refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_
    refine supports_union.2 ⟨IHg H', ?_⟩
    refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_
    · simp only [codeSupp', codeSupp, Finset.union_subset_iff] at h H ⊢
      exact ⟨h.2.2, H.2⟩
    exact IHf (Finset.union_subset_right H')
  | case f g IHf IHg =>
    have H' := H; simp only [codeSupp_case, Finset.union_subset_iff] at H'
    refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun _ => ?_
    exact supports_union.2 ⟨IHf H'.2.1, IHg H'.2.2⟩
  | fix f IHf =>
    have H' := H; simp only [codeSupp_fix, Finset.union_subset_iff] at H'
    refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_
    refine supports_union.2 ⟨IHf H'.2, ?_⟩
    refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_
    · simp only [codeSupp', codeSupp, Finset.union_subset_iff, contSupp, trStmts₁,
        Finset.insert_subset_iff] at h H ⊢
      exact ⟨h.1, ⟨H.1.1, h⟩, H.2⟩
    exact supports_singleton.2 (ret_supports <| Finset.union_subset_right H)
  | _ => exact trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H)
Cleared hypotheses: c, k, H