awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
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
h_1 :
  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
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ codeSupp fs k.cons₂ ⊆ S
have H'₁ : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧
  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₂) ⊆
    S
Tactic: rw [codeSupp, contSupp_cons₁] at H'
Cleared hypotheses: H', h_1, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
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 H' : codeSupp (f.comp g) k ⊆ S
⊢ Supports (codeSupp' (f.comp g) k) S
have H'₁ : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
Tactic: rw [codeSupp_comp] at H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
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
H' : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
⊢ Supports (codeSupp' (f.comp g) k) S
have H'₁ : codeSupp g (Cont'.comp f k) ⊆ S
Tactic: have H' := Finset.union_subset_right H'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
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
H'_1 : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
⊢ Supports (codeSupp' (f.comp g) k) S
have comp : ∀ (h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S),
  Supports (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k)) S
Tactic: refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
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
H'_1 : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S
⊢ Supports (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k)) S
have comp : Supports (trStmts₁ (trNormal f k) ∪ codeSupp' f k) S
Tactic: refine supports_union.2 ⟨IHg H', ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
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
H'_1 : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S
⊢ Supports (trStmts₁ (trNormal f k) ∪ codeSupp' f k) S
have comp : codeSupp f k ⊆ S
Tactic: refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
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
H'_1 : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S
comp : codeSupp f k ⊆ S
⊢ Supports (trStmts₁ (trNormal f k) ∪ codeSupp' f k) S
have comp₁ : codeSupp' f k ⊆ S → Supports (codeSupp' f k) S
Tactic: refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
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
H'_1 : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S
⊢ codeSupp f k ⊆ S
have comp : ∀ (h : codeSupp' g (Cont'.comp f k) ⊆ S ∧ trStmts₁ (trNormal f k) ⊆ S ∧ codeSupp' f k ⊆ S)
  (H :
    (trStmts₁ (trNormal (f.comp g) k) ⊆ S ∧
        codeSupp' g (Cont'.comp f k) ⊆ S ∧ trStmts₁ (trNormal f k) ⊆ S ∧ codeSupp' f k ⊆ S) ∧
      contSupp k ⊆ S),
  codeSupp' f k ⊆ S ∧ contSupp k ⊆ S
Tactic: simp only [codeSupp', codeSupp, Finset.union_subset_iff] at h H ⊢
Cleared hypotheses: H, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
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 H' : codeSupp (f.case g) k ⊆ S
⊢ Supports (codeSupp' (f.case g) k) S
have H'₁ : 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 H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
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
H' : trStmts₁ (trNormal (f.case g) k) ⊆ S ∧ codeSupp f k ⊆ S ∧ codeSupp g k ⊆ S
⊢ Supports (codeSupp' (f.case g) k) S
have case : codeSupp' f k ∪ codeSupp' g k ⊆ S → Supports (codeSupp' f k ∪ codeSupp' g k) S
Tactic: refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun _ => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H H' : codeSupp f.fix k ⊆ S
⊢ Supports (codeSupp' f.fix k) S
have H'₁ : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
Tactic: simp only [codeSupp_fix, Finset.union_subset_iff] at H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
⊢ Supports (codeSupp' f.fix k) S
have fix : ∀ (h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S),
  Supports (codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k})) S
Tactic: refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
⊢ Supports (codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k})) S
have fix : Supports (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) S
Tactic: refine supports_union.2 ⟨IHf H'.2, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
⊢ Supports (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) S
have fix : codeSupp f (Cont'.fix f k) ⊆ S
Tactic: refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
fix : codeSupp f (Cont'.fix f k) ⊆ S
⊢ Supports (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) S
have fix₁ : {Λ'.ret k} ⊆ S → Supports {Λ'.ret k} S
Tactic: refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (H : codeSupp f k ⊆ S), Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S
have fix : ∀
  (h :
    codeSupp' f (Cont'.fix f k) ⊆ S ∧
      (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
        {Λ'.ret k} ⊆ S)
  (H :
    (trStmts₁ (trNormal f.fix k) ⊆ S ∧
        codeSupp' f (Cont'.fix f k) ⊆ S ∧
          (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
            {Λ'.ret k} ⊆ S) ∧
      contSupp k ⊆ S),
  codeSupp' f (Cont'.fix f k) ⊆ S ∧
    (trStmts₁ (trNormal f.fix k) ⊆ S ∧
        codeSupp' f (Cont'.fix f k) ⊆ S ∧
          (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
            {Λ'.ret k} ⊆ S) ∧
      contSupp k ⊆ S
Tactic: simp only [codeSupp', codeSupp, Finset.union_subset_iff, contSupp, trStmts₁,
        Finset.insert_subset_iff] at h H ⊢
Cleared hypotheses: H, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
c : Code
k : Cont'
H : codeSupp c k ⊆ S
⊢ Supports (codeSupp' c k) S
have 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
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
-- 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
⊢ Supports (codeSupp' c k) S
have 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
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
-- 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
⊢ Supports (codeSupp' c k) S
have 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
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
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H H₁ : contSupp (Cont'.cons₁ f k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S
have 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
Tactic: rw [contSupp_cons₁] at H₁
Cleared hypotheses: H₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : 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
have H₂ : codeSupp f k.cons₂ ⊆ S
Tactic: have H₂ := Finset.union_subset_right H₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : 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
have cons₁ : ∀ (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
Tactic: refine trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : 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
have cons₁ : Supports (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) S
Tactic: refine supports_union.2 ⟨codeSupp'_supports H₂, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : 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
have H₃ : codeSupp' f k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S ∧ contSupp k ⊆ S
Tactic: simp only [codeSupp, contSupp_cons₂, Finset.union_subset_iff] at H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H H' : contSupp k.cons₂ ⊆ S
⊢ Supports (contSupp k.cons₂) S
have H'₁ : trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k ⊆ S
Tactic: rw [contSupp_cons₂] at H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H H' : contSupp (Cont'.comp f k) ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S
have H'₁ : codeSupp f k ⊆ S
Tactic: rw [contSupp_comp] at H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : 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
have H₂ : contSupp k ⊆ S
Tactic: have H₂ := Finset.union_subset_right H'