awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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: 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 : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
⊢ Supports (insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))) S
have h₁ : Λ'.read 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 : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
⊢ Supports (insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))) S
have h₂ : (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ 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 : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
⊢ Supports (insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))) S
have h₃ : ∀ ⦃x : Λ'⦄ (x_1 : Option Γ') (h : x ∈ trStmts₁ (q x_1)), x ∈ S
Tactic: simp [Finset.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
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
⊢ Supports (insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))) S
have h₃ : ∀ ⦃x : Λ'⦄ (x_1 : Option Γ') (h : x ∈ trStmts₁ (q x_1)), x ∈ S
Tactic: try simp [Finset.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
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
⊢ Supports (insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))) S
have h₃ : ∀ ⦃x : Λ'⦄ (x_1 : Option Γ') (h : x ∈ trStmts₁ (q x_1)), x ∈ S
Tactic: first | have h₃ := h₂ W | try simp [Finset.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
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S
have h₁ : q.succ ∈ 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.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S
have h₂ : insert (unrev q) (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.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : insert (unrev q) (trStmts₁ q) ⊆ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S
have h₃ : unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S
Tactic: simp [Finset.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
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : insert (unrev q) (trStmts₁ q) ⊆ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S
have h₃ : unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S
Tactic: try simp [Finset.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
q : Λ'
q_ih : ∀ (H₁ : Λ'.Supports S q) (HS₁ : trStmts₁ q ⊆ S), Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : insert (unrev q) (trStmts₁ q) ⊆ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S
have h₃ : unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S
Tactic: first | have h₃ := h₂ W | try simp [Finset.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
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₁ : 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
have h₁ : q₁.pred 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₂ : Λ'
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₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
have h₂ : insert (unrev q₂) (trStmts₁ q₁ ∪ 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₂ : Λ'
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₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂) ⊆ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
have h₃ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
Tactic: simp [Finset.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
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₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂) ⊆ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
have h₃ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
Tactic: try simp [Finset.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
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₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂) ⊆ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
have h₃ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
Tactic: first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ') (H₁ : Λ'.Supports S (q a)) (HS₁ : trStmts₁ (q a) ⊆ S), Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : ∀ ⦃x : Λ'⦄ (x_1 : Option Γ') (h : x ∈ trStmts₁ (q x_1)), x ∈ S
⊢ Supports (insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))) S
have read : Supports (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) S
Tactic: refine supports_insert.2 ⟨fun _ => h₂ _ W, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S
have succ : Supports (insert (unrev q) (trStmts₁ q)) S
Tactic: refine supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₂.1, fun _ => h₂.1⟩, ?_⟩
-- 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₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
have pred : Supports (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) S
Tactic: refine -- pred
      supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₂.2 _ (Or.inl W),
                          fun _ => h₂.1, fun _ => h₂.1⟩, ?_⟩
-- 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₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) S
have pred : Supports (trStmts₁ q₁ ∪ trStmts₁ q₂) S
Tactic: refine supports_insert.2 ⟨⟨fun _ => h₂.2 _ (Or.inr W), fun _ => h₂.1⟩, ?_⟩
-- 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₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (trStmts₁ q₁ ∪ trStmts₁ q₂) S
have pred : Supports (trStmts₁ q₁) S
Tactic: refine supports_union.2 ⟨?_, ?_⟩
-- 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₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
pred : Supports (trStmts₁ q₁) S
⊢ Supports (trStmts₁ q₁ ∪ trStmts₁ q₂) S
have pred₁ : Supports (trStmts₁ q₂) S
Tactic: refine supports_union.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
q : Λ'
K : Finset Λ'
H₁ : Λ'.Supports S q
H₂ : trStmts₁ q ∪ K ⊆ S
H₃ : K ⊆ S → Supports K S
⊢ Supports (trStmts₁ q ∪ K) S
have H₄ : trStmts₁ q ⊆ S ∧ K ⊆ S
Tactic: simp only [Finset.union_subset_iff] at H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
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))
have pos : s = some Γ'.consₗ → Λ'.Supports S (id (unrev (Λ'.ret k).succ))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
s : Option Γ'
pos : s = some Γ'.consₗ → Λ'.Supports S (id (unrev (Λ'.ret k).succ))
⊢ Λ'.Supports S
    ((if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main) (unrev (Λ'.ret k).succ))
have neg : ¬s = some Γ'.consₗ → Λ'.Supports S (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main (unrev (Λ'.ret k).succ))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
a_ih : ∀ {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)
have cons : Λ'.Supports S (trNormal f (Cont'.cons₁ fs k))
Tactic: simp [Λ'.Supports, head]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
a_ih : ∀ {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))
have cons : codeSupp f (Cont'.cons₁ fs k) ⊆ S
Tactic: apply IHf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
a_ih : ∀ {k : Cont'} (Hk : codeSupp fs k ⊆ S), Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (f.cons fs) k ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S
have Hk₁ : trStmts₁ (trNormal (f.cons fs) k) ∪ codeSupp f (Cont'.cons₁ fs k) ⊆ S
Tactic: rw [codeSupp_cons] at Hk
Cleared hypotheses: Hk
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f g : Code
a_ih : ∀ {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)
have comp : Λ'.Supports S (trNormal g (Cont'.comp f k))
Tactic: simp [Λ'.Supports, head]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f g : Code
a_ih : ∀ {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))
have comp : codeSupp g (Cont'.comp f k) ⊆ S
Tactic: apply IHg
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
f g : Code
a_ih : ∀ {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
⊢ codeSupp g (Cont'.comp f k) ⊆ S
have Hk₁ : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
Tactic: rw [codeSupp_comp] at Hk
Cleared hypotheses: Hk
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
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)
have Hk₁ : 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 Hk
Cleared hypotheses: Hk
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
k : Cont'
Hk : codeSupp f.fix k ⊆ S
⊢ Λ'.Supports S (trNormal f.fix k)
have fix : Λ'.Supports S (trNormal f (Cont'.fix f k))
Tactic: simp [Λ'.Supports, head]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
k : Cont'
Hk : codeSupp f.fix k ⊆ S
⊢ Λ'.Supports S (trNormal f (Cont'.fix f k))
have fix : codeSupp f (Cont'.fix f k) ⊆ S
Tactic: apply IHf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'} (Hk : codeSupp f k ⊆ S), Λ'.Supports S (trNormal f k)
k : Cont'
Hk : codeSupp f.fix k ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S
have Hk₁ : trStmts₁ (trNormal f.fix k) ∪ codeSupp f (Cont'.fix f k) ⊆ S
Tactic: rw [codeSupp_fix] at Hk
Cleared hypotheses: Hk
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
c : Code
k : Cont'
Hk : codeSupp c k ⊆ S
⊢ Λ'.Supports S (trNormal c k)
have zero' : ∀ {k : Cont'} (Hk : codeSupp Code.zero' k ⊆ S), Λ'.Supports S (trNormal Code.zero' 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)
⊢ Λ'.Supports S (trNormal c k)
have zero'₁ : ∀ {k : Cont'} (Hk : codeSupp Code.zero' 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
⊢ Λ'.Supports S (trNormal c k)
have succ : ∀ {k : Cont'} (Hk : codeSupp Code.succ k ⊆ S), Λ'.Supports S (trNormal Code.succ 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)
⊢ Λ'.Supports S (trNormal c k)
have 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))
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