awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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))
⊢ Λ'.Supports S (trNormal c k)
have tail : ∀ {k : Cont'} (Hk : codeSupp Code.tail k ⊆ S), Λ'.Supports S (trNormal Code.tail 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
Cleared hypotheses: c, k, Hk
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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)
⊢ Λ'.Supports S (trNormal c k)
have tail₁ : ∀ {k : Cont'} (Hk : codeSupp Code.tail k ⊆ S), contSupp k ⊆ S
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
Cleared hypotheses: c, k, Hk
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ Λ'.Supports S (trNormal c k)
have 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)
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
Cleared hypotheses: c, k, Hk
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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)
⊢ Λ'.Supports S (trNormal c k)
have 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))
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
Cleared hypotheses: c, k, Hk
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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))
⊢ Λ'.Supports S (trNormal c k)
have 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)
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
Cleared hypotheses: c, k, Hk
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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)
⊢ Λ'.Supports S (trNormal c k)
have 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))
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
Cleared hypotheses: c, k, Hk
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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))
⊢ Λ'.Supports S (trNormal c k)
have 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)
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
Cleared hypotheses: c, k, Hk
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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)
⊢ Λ'.Supports S (trNormal c k)
have 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)
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
Cleared hypotheses: c, k, Hk
-- 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 H' : codeSupp (f.cons fs) k ⊆ S
⊢ Supports (codeSupp' (f.cons fs) k) S
have H'₁ : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
Tactic: simp only [codeSupp_cons, Finset.union_subset_iff] at H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ Supports (codeSupp' (f.cons fs) k) S
have cons : ∀
  (h :
    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),
  Supports
    (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
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 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 :
  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
⊢ Supports
    (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
have cons : Supports
  (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
Tactic: refine supports_union.2 ⟨IHf H'.2, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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 :
  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
⊢ codeSupp fs k.cons₂ ⊆ S
have cons : ∀
  (h :
    codeSupp' f (Cont'.cons₁ fs k) ⊆ S ∧
      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₂)))) ⊆
          S ∧
        codeSupp' fs k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S)
  (H : codeSupp' (f.cons fs) k ⊆ S ∧ contSupp k ⊆ S),
  codeSupp' fs k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S ∧ contSupp k ⊆ S
Tactic: simp only [codeSupp, Finset.union_subset_iff, contSupp] at h H ⊢
Cleared hypotheses: H, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ Supports (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k))) S
have cons : codeSupp fs k.cons₂ ⊆ S
Tactic: refine supports_union.2 ⟨IHfs ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
cons : codeSupp fs k.cons₂ ⊆ S
⊢ Supports (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k))) S
have cons₁ : Supports (trStmts₁ (head stack (Λ'.ret k))) S
Tactic: refine supports_union.2 ⟨IHfs ?_, ?_⟩