awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
k : Cont'
zero' : trStmts₁ (trNormal Code.zero' k) ⊆ trStmts₁ (trNormal Code.zero' k)
succ : trStmts₁ (trNormal Code.succ k) ⊆ trStmts₁ (trNormal Code.succ k)
⊢ trStmts₁ (trNormal c k) ⊆ codeSupp' c k
have tail : trStmts₁ (trNormal Code.tail k) ⊆ trStmts₁ (trNormal Code.tail k)
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
k : Cont'
zero' : trStmts₁ (trNormal Code.zero' k) ⊆ trStmts₁ (trNormal Code.zero' k)
succ : trStmts₁ (trNormal Code.succ k) ⊆ trStmts₁ (trNormal Code.succ k)
tail : trStmts₁ (trNormal Code.tail k) ⊆ trStmts₁ (trNormal Code.tail k)
⊢ trStmts₁ (trNormal c k) ⊆ codeSupp' c k
have cons : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.cons a_1) k) ⊆ codeSupp' (a.cons a_1) k
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
k : Cont'
zero' : trStmts₁ (trNormal Code.zero' k) ⊆ trStmts₁ (trNormal Code.zero' k)
succ : trStmts₁ (trNormal Code.succ k) ⊆ trStmts₁ (trNormal Code.succ k)
tail : trStmts₁ (trNormal Code.tail k) ⊆ trStmts₁ (trNormal Code.tail k)
cons : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.cons a_1) k) ⊆ codeSupp' (a.cons a_1) k
⊢ trStmts₁ (trNormal c k) ⊆ codeSupp' c k
have comp : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.comp a_1) k) ⊆ codeSupp' (a.comp a_1) k
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
k : Cont'
zero' : trStmts₁ (trNormal Code.zero' k) ⊆ trStmts₁ (trNormal Code.zero' k)
succ : trStmts₁ (trNormal Code.succ k) ⊆ trStmts₁ (trNormal Code.succ k)
tail : trStmts₁ (trNormal Code.tail k) ⊆ trStmts₁ (trNormal Code.tail k)
cons : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.cons a_1) k) ⊆ codeSupp' (a.cons a_1) k
comp : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.comp a_1) k) ⊆ codeSupp' (a.comp a_1) k
⊢ trStmts₁ (trNormal c k) ⊆ codeSupp' c k
have case : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.case a_1) k) ⊆ codeSupp' (a.case a_1) k
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
k : Cont'
zero' : trStmts₁ (trNormal Code.zero' k) ⊆ trStmts₁ (trNormal Code.zero' k)
succ : trStmts₁ (trNormal Code.succ k) ⊆ trStmts₁ (trNormal Code.succ k)
tail : trStmts₁ (trNormal Code.tail k) ⊆ trStmts₁ (trNormal Code.tail k)
cons : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.cons a_1) k) ⊆ codeSupp' (a.cons a_1) k
comp : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.comp a_1) k) ⊆ codeSupp' (a.comp a_1) k
case : ∀ (a a_1 : Code), trStmts₁ (trNormal (a.case a_1) k) ⊆ codeSupp' (a.case a_1) k
⊢ trStmts₁ (trNormal c k) ⊆ codeSupp' c k
have fix : ∀ (a : Code), trStmts₁ (trNormal a.fix k) ⊆ codeSupp' a.fix k
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f g : Code
k : Cont'
⊢ codeSupp (f.comp g) k = trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k)
have simp : trStmts₁ (trNormal g (Cont'.comp f k)) ∪
    (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) =
  trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
Tactic: simp only [codeSupp, codeSupp', trNormal, Finset.union_assoc, contSupp]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f g : Code
k : Cont'
⊢ trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
have rw : trStmts₁ (trNormal g (Cont'.comp f k)) ∪
    (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k ∪ contSupp k)) =
  trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
Tactic: rw [← Finset.union_assoc _ _ (contSupp k),
    Finset.union_eq_right.2 (codeSupp'_self _ _)]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f g : Code
k : Cont'
rw :
  trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k ∪ contSupp k)) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
⊢ trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
have rw₁ : trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k)) =
  trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
Tactic: rw [← Finset.union_assoc _ _ (contSupp k),
    Finset.union_eq_right.2 (codeSupp'_self _ _)]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x : Option Γ'
⊢ Λ'.Supports S ((if x = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) k) (unrev q))
have pos : x = some Γ'.consₗ → Λ'.Supports S (id (unrev q))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x : Option Γ'
pos : x = some Γ'.consₗ → Λ'.Supports S (id (unrev q))
⊢ Λ'.Supports S ((if x = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) k) (unrev q))
have neg : ¬x = some Γ'.consₗ → Λ'.Supports S (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) k (unrev q))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret k))
have W : ∀ {q : Λ'}, q ∈ trStmts₁ q
Tactic: have W := fun {q} => trStmts₁_self q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : contSupp (Cont'.cons₁ a a_1) ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.cons₁ a a_1)))
have H₂ : trStmts₁
      (move₂ (fun (x : Γ') ↦ false) main aux
        (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
          (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal a a_1.cons₂)))) ⊆
    S ∧
  codeSupp a a_1.cons₂ ⊆ S
Tactic: rw [contSupp_cons₁, Finset.union_subset_iff] at H₁
Cleared hypotheses: H₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Cont'
H₁ : contSupp a.cons₂ ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret a.cons₂))
have H₂ : trStmts₁ (head stack (Λ'.ret a)) ⊆ S ∧ contSupp a ⊆ S
Tactic: rw [contSupp_cons₂, Finset.union_subset_iff] at H₁
Cleared hypotheses: H₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : contSupp (Cont'.comp a a_1) ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.comp a a_1)))
have H₂ : codeSupp a a_1 ⊆ S
Tactic: rw [contSupp_comp] at H₁
Cleared hypotheses: H₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : contSupp (Cont'.fix a a_1) ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.fix a a_1)))
have H₂ : codeSupp a (Cont'.fix a a_1) ⊆ S
Tactic: rw [contSupp_fix] at H₁
Cleared hypotheses: H₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a (Cont'.fix a a_1) ⊆ S
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.fix a a_1)))
have L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s), a ∈ s ∪ t
Tactic: have L := @Finset.mem_union_left
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a (Cont'.fix a a_1) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s), a ∈ s ∪ t
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.fix a a_1)))
have R : ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t), a ∈ s ∪ t
Tactic: have R := @Finset.mem_union_right
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a (Cont'.fix a a_1) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s), a ∈ s ∪ t
R : ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t), a ∈ s ∪ t
s : Option Γ'
⊢ (bif natEnd (s.getD default) then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S
have fix : (bif false then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S
Tactic: cases natEnd (s.getD default)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a : Code
a_1 : Cont'
H₁ : codeSupp a (Cont'.fix a a_1) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s), a ∈ s ∪ t
R : ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t), a ∈ s ∪ t
s : Option Γ'
fix : (bif false then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S
⊢ (bif natEnd (s.getD default) then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S
have fix₁ : (bif true then Λ'.ret a_1 else Λ'.clear natEnd main (trNormal a (Cont'.fix a a_1))) ∈ S
Tactic: cases natEnd (s.getD default)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret k))
have halt : ∀ (H₁ : contSupp Cont'.halt ⊆ S), TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret Cont'.halt))
Tactic: cases k with
  | halt => trivial
  | cons₁ => rw [contSupp_cons₁, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | cons₂ => rw [contSupp_cons₂, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | comp => rw [contSupp_comp] at H₁; exact fun _ => H₁ (codeSupp_self _ _ W)
  | fix =>
    rw [contSupp_fix] at H₁
    have L := @Finset.mem_union_left; have R := @Finset.mem_union_right
    intro s; dsimp only; cases natEnd (s.getD default)
    · refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)
    · exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)
Cleared hypotheses: k, H₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
halt : ∀ (H₁ : contSupp Cont'.halt ⊆ S), TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret Cont'.halt))
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret k))
have cons₁ : ∀ (a : Code) (a_1 : Cont') (H₁ : contSupp (Cont'.cons₁ a a_1) ⊆ S),
  TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.cons₁ a a_1)))
Tactic: cases k with
  | halt => trivial
  | cons₁ => rw [contSupp_cons₁, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | cons₂ => rw [contSupp_cons₂, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | comp => rw [contSupp_comp] at H₁; exact fun _ => H₁ (codeSupp_self _ _ W)
  | fix =>
    rw [contSupp_fix] at H₁
    have L := @Finset.mem_union_left; have R := @Finset.mem_union_right
    intro s; dsimp only; cases natEnd (s.getD default)
    · refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)
    · exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)
Cleared hypotheses: k, H₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
halt : ∀ (H₁ : contSupp Cont'.halt ⊆ S), TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret Cont'.halt))
cons₁ :
  ∀ (a : Code) (a_1 : Cont') (H₁ : contSupp (Cont'.cons₁ a a_1) ⊆ S),
    TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.cons₁ a a_1)))
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret k))
have cons₂ : ∀ (a : Cont') (H₁ : contSupp a.cons₂ ⊆ S), TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret a.cons₂))
Tactic: cases k with
  | halt => trivial
  | cons₁ => rw [contSupp_cons₁, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | cons₂ => rw [contSupp_cons₂, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | comp => rw [contSupp_comp] at H₁; exact fun _ => H₁ (codeSupp_self _ _ W)
  | fix =>
    rw [contSupp_fix] at H₁
    have L := @Finset.mem_union_left; have R := @Finset.mem_union_right
    intro s; dsimp only; cases natEnd (s.getD default)
    · refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)
    · exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)
Cleared hypotheses: k, H₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
halt : ∀ (H₁ : contSupp Cont'.halt ⊆ S), TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret Cont'.halt))
cons₁ :
  ∀ (a : Code) (a_1 : Cont') (H₁ : contSupp (Cont'.cons₁ a a_1) ⊆ S),
    TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.cons₁ a a_1)))
cons₂ : ∀ (a : Cont') (H₁ : contSupp a.cons₂ ⊆ S), TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret a.cons₂))
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret k))
have comp : ∀ (a : Code) (a_1 : Cont') (H₁ : contSupp (Cont'.comp a a_1) ⊆ S),
  TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.comp a a_1)))
Tactic: cases k with
  | halt => trivial
  | cons₁ => rw [contSupp_cons₁, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | cons₂ => rw [contSupp_cons₂, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | comp => rw [contSupp_comp] at H₁; exact fun _ => H₁ (codeSupp_self _ _ W)
  | fix =>
    rw [contSupp_fix] at H₁
    have L := @Finset.mem_union_left; have R := @Finset.mem_union_right
    intro s; dsimp only; cases natEnd (s.getD default)
    · refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)
    · exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)
Cleared hypotheses: k, H₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
halt : ∀ (H₁ : contSupp Cont'.halt ⊆ S), TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret Cont'.halt))
cons₁ :
  ∀ (a : Code) (a_1 : Cont') (H₁ : contSupp (Cont'.cons₁ a a_1) ⊆ S),
    TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.cons₁ a a_1)))
cons₂ : ∀ (a : Cont') (H₁ : contSupp a.cons₂ ⊆ S), TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret a.cons₂))
comp :
  ∀ (a : Code) (a_1 : Cont') (H₁ : contSupp (Cont'.comp a a_1) ⊆ S),
    TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.comp a a_1)))
⊢ TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret k))
have fix : ∀ (a : Code) (a_1 : Cont') (H₁ : contSupp (Cont'.fix a a_1) ⊆ S),
  TM2.SupportsStmt (Γ := fun (x : K') ↦ Γ') S (tr (Λ'.ret (Cont'.fix a a_1)))
Tactic: cases k with
  | halt => trivial
  | cons₁ => rw [contSupp_cons₁, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | cons₂ => rw [contSupp_cons₂, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | comp => rw [contSupp_comp] at H₁; exact fun _ => H₁ (codeSupp_self _ _ W)
  | fix =>
    rw [contSupp_fix] at H₁
    have L := @Finset.mem_union_left; have R := @Finset.mem_union_right
    intro s; dsimp only; cases natEnd (s.getD default)
    · refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)
    · exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)
Cleared hypotheses: k, H₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
q : Λ'
H₁ : Λ'.Supports S q
HS₁ : trStmts₁ q ⊆ S
⊢ Supports (trStmts₁ q) S
have W : ∀ {q : Λ'}, q ∈ trStmts₁ q
Tactic: have W := fun {q} => trStmts₁_self q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : ∀ (H₁ : Λ'.Supports S q₁) (HS₁ : trStmts₁ q₁ ⊆ S), Supports (trStmts₁ q₁) S
q₂_ih : ∀ (H₁ : Λ'.Supports S q₂) (HS₁ : trStmts₁ q₂ ⊆ S), Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : trStmts₁ (q₁.pred q₂) ⊆ S
⊢ Supports (trStmts₁ (q₁.pred q₂)) S
have pred : ∀ (HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S),
  Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
Tactic: simp [trStmts₁, -Finset.singleton_subset_iff] at HS₁ ⊢
Cleared hypotheses: HS₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p k₁ k₂ q)
HS₁ : insert (Λ'.move p k₁ k₂ q) (trStmts₁ q) ⊆ S
⊢ Supports (insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)) S
have h₁ : Λ'.move p k₁ k₂ q ∈ S
Tactic: obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p k₁ k₂ q)
HS₁ : insert (Λ'.move p k₁ k₂ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.move p k₁ k₂ q ∈ S
⊢ Supports (insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)) S
have h₂ : trStmts₁ q ⊆ S
Tactic: obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p k₁ k₂ q)
HS₁ : insert (Λ'.move p k₁ k₂ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.move p k₁ k₂ q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)) S
have h₃ : q ∈ S
Tactic: have h₃ := h₂ W
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p k₁ k₂ q)
HS₁ : insert (Λ'.move p k₁ k₂ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.move p k₁ k₂ q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)) S
have h₃ : q ∈ S
Tactic: first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p k q)
HS₁ : insert (Λ'.clear p k q) (trStmts₁ q) ⊆ S
⊢ Supports (insert (Λ'.clear p k q) (trStmts₁ q)) S
have h₁ : Λ'.clear p k q ∈ S
Tactic: obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p k q)
HS₁ : insert (Λ'.clear p k q) (trStmts₁ q) ⊆ S
h₁ : Λ'.clear p k q ∈ S
⊢ Supports (insert (Λ'.clear p k q) (trStmts₁ q)) S
have h₂ : trStmts₁ q ⊆ S
Tactic: obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p k q)
HS₁ : insert (Λ'.clear p k q) (trStmts₁ q) ⊆ S
h₁ : Λ'.clear p k q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert (Λ'.clear p k q) (trStmts₁ q)) S
have h₃ : q ∈ S
Tactic: have h₃ := h₂ W
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p : Γ' → Bool
k : K'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p k q)
HS₁ : insert (Λ'.clear p k q) (trStmts₁ q) ⊆ S
h₁ : Λ'.clear p k q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert (Λ'.clear p k q) (trStmts₁ q)) S
have h₃ : q ∈ S
Tactic: first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
⊢ Supports (insert q.copy (trStmts₁ q)) S
have h₁ : q.copy ∈ S
Tactic: obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
h₁ : q.copy ∈ S
⊢ Supports (insert q.copy (trStmts₁ q)) S
have h₂ : trStmts₁ q ⊆ S
Tactic: obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
h₁ : q.copy ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert q.copy (trStmts₁ q)) S
have h₃ : q ∈ S
Tactic: have h₃ := h₂ W
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
h₁ : q.copy ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert q.copy (trStmts₁ q)) S
have h₃ : q ∈ S
Tactic: first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k s q)
HS₁ : insert (Λ'.push k s q) (trStmts₁ q) ⊆ S
⊢ Supports (insert (Λ'.push k s q) (trStmts₁ q)) S
have h₁ : Λ'.push k s q ∈ S
Tactic: obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k s q)
HS₁ : insert (Λ'.push k s q) (trStmts₁ q) ⊆ S
h₁ : Λ'.push k s q ∈ S
⊢ Supports (insert (Λ'.push k s q) (trStmts₁ q)) S
have h₂ : trStmts₁ q ⊆ S
Tactic: obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k s q)
HS₁ : insert (Λ'.push k s q) (trStmts₁ q) ⊆ S
h₁ : Λ'.push k s q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert (Λ'.push k s q) (trStmts₁ q)) S
have h₃ : q ∈ S
Tactic: have h₃ := h₂ W