awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q q' : Λ'
move :
  ∀ (p : Γ' → Bool) (k₁ k₂ : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)
clear :
  ∀ (p : Γ' → Bool) (k : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)
copy :
  ∀ (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q), q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy
push :
  ∀ (k : K') (s : Option Γ' → Option Γ') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.push k s q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k s q)
read :
  ∀ (q : Option Γ' → Λ') (q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)),
    q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)
succ :
  ∀ (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q), q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
have pred : ∀ (q₁ q₂ : Λ') (q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁)
  (q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂),
  q' ∈ trStmts₁ (q₁.pred q₂) → trStmts₁ q' ⊆ trStmts₁ (q₁.pred q₂)
Tactic: induction q with
  | move _ _ _ q q_ih => _ | clear _ _ q q_ih => _ | copy q q_ih => _ | push _ _ q q_ih => _
  | read q q_ih => _ | succ q q_ih => _ | pred q₁ q₂ q₁_ih q₂_ih => _ | ret => _
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q q' : Λ'
move :
  ∀ (p : Γ' → Bool) (k₁ k₂ : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)
clear :
  ∀ (p : Γ' → Bool) (k : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)
copy :
  ∀ (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q), q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy
push :
  ∀ (k : K') (s : Option Γ' → Option Γ') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.push k s q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k s q)
read :
  ∀ (q : Option Γ' → Λ') (q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)),
    q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)
succ :
  ∀ (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q), q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ
pred :
  ∀ (q₁ q₂ : Λ') (q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁)
    (q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂),
    q' ∈ trStmts₁ (q₁.pred q₂) → trStmts₁ q' ⊆ trStmts₁ (q₁.pred q₂)
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
have ret : ∀ (k : Cont'), q' ∈ trStmts₁ (Λ'.ret k) → trStmts₁ q' ⊆ trStmts₁ (Λ'.ret k)
Tactic: induction q with
  | move _ _ _ q q_ih => _ | clear _ _ q q_ih => _ | copy q q_ih => _ | push _ _ q q_ih => _
  | read q q_ih => _ | succ q q_ih => _ | pred q₁ q₂ q₁_ih q₂_ih => _ | ret => _
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' : Λ'
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)
have move : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)
Tactic: simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' : Λ'
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)
have move : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)
Tactic: all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' : Λ'
p : Γ' → Bool
k : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)
have clear : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.clear p k q) (trStmts₁ q)
Tactic: simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' : Λ'
p : Γ' → Bool
k : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)
have clear : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.clear p k q) (trStmts₁ q)
Tactic: all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy
have copy : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.copy (trStmts₁ q)
Tactic: simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy
have copy : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.copy (trStmts₁ q)
Tactic: all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' : Λ'
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.push k s q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k s q)
have push : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.push k s q) (trStmts₁ q)
Tactic: simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' : Λ'
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.push k s q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k s q)
have push : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.push k s q) (trStmts₁ q)
Tactic: all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)
have read : Membership.mem (γ := Finset Λ') (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) q' →
  trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))
Tactic: simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)
have read : Membership.mem (γ := Finset Λ') (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) q' →
  trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))
Tactic: all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ
have succ : (q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧
  (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))
Tactic: simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ
have succ : (q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧
  (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))
Tactic: all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ q' ∈ trStmts₁ (q₁.pred q₂) → trStmts₁ q' ⊆ trStmts₁ (q₁.pred q₂)
have pred : (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
  (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))
Tactic: simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ q' ∈ trStmts₁ (q₁.pred q₂) → trStmts₁ q' ⊆ trStmts₁ (q₁.pred q₂)
have pred : (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
  (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))
Tactic: all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ Membership.mem (γ := Finset Λ') (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)) q' →
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))
have read : ∀ (x : Option Γ') (h : q' ∈ trStmts₁ (q x)),
  trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s))
Tactic: simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, forall_exists_index]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
s : Option Γ'
h : q' ∈ trStmts₁ (q s)
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ Membership.mem (γ := Finset Λ') (insert (Λ'.read q) (Finset.biUnion Finset.univ fun (s : Option Γ') ↦ trStmts₁ (q s)))
    x
have read : x = Λ'.read q ∨ ∃ (a : Option Γ'), x ∈ trStmts₁ (q a)
Tactic: simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, Finset.mem_insert]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ (q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧
    (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))
have succ : q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
succ : q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))
⊢ (q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧
    (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))
have succ₁ : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
h : q' ∈ trStmts₁ q
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x ∈ insert q.succ (insert (unrev q) (trStmts₁ q))
have succ : x = q.succ ∨ x = unrev q ∨ x ∈ trStmts₁ q
Tactic: simp only [Finset.mem_insert]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
      (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))
have pred : ∀ (h : q' ∈ trStmts₁ q₁) (x : Λ') (h' : x ∈ trStmts₁ q'),
  x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
Tactic: refine ⟨fun h x h' => ?_, fun _ x h' => ?_, fun h x h' => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
pred :
  ∀ (h : q' ∈ trStmts₁ q₁) (x : Λ') (h' : x ∈ trStmts₁ q'),
    x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
⊢ (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
      (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))
have pred₁ : q' = unrev q₂ →
  ∀ (x : Λ') (h' : x ∈ trStmts₁ (unrev q₂)), x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
Tactic: refine ⟨fun h x h' => ?_, fun _ x h' => ?_, fun h x h' => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
pred :
  ∀ (h : q' ∈ trStmts₁ q₁) (x : Λ') (h' : x ∈ trStmts₁ q'),
    x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
pred₁ :
  q' = unrev q₂ →
    ∀ (x : Λ') (h' : x ∈ trStmts₁ (unrev q₂)), x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
⊢ (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
      (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))
have pred₂ : ∀ (h : q' ∈ trStmts₁ q₂) (x : Λ') (h' : x ∈ trStmts₁ q'),
  x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
Tactic: refine ⟨fun h x h' => ?_, fun _ x h' => ?_, fun h x h' => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₁
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
have pred : x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' = unrev q₂
x : Λ'
h' : x ∈ trStmts₁ (unrev q₂)
⊢ x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
have pred : x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₂
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
have pred : x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' = unrev q₂
x : Λ'
h' : x ∈ trStmts₁ (unrev q₂)
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
have pred : ∀ (h' : x = Λ'.move (fun (x : Γ') ↦ false) rev main q₂),
  x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
Tactic: rcases Finset.mem_insert.1 h' with h' | h'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' = unrev q₂
x : Λ'
h' : x ∈ trStmts₁ (unrev q₂)
pred :
  ∀ (h' : x = Λ'.move (fun (x : Γ') ↦ false) rev main q₂),
    x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
have pred₁ : ∀ (h' : x ∈ trStmts₁ q₂), x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
Tactic: rcases Finset.mem_insert.1 h' with h' | h'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
⊢ q ∈ trStmts₁ q
have move : ∀ (p : Γ' → Bool) (k₁ k₂ : K'), ∀ q ∈ trStmts₁ q, Λ'.move p k₁ k₂ q ∈ trStmts₁ (Λ'.move p k₁ k₂ q)
Tactic: induction q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
move : ∀ (p : Γ' → Bool) (k₁ k₂ : K'), ∀ q ∈ trStmts₁ q, Λ'.move p k₁ k₂ q ∈ trStmts₁ (Λ'.move p k₁ k₂ q)
⊢ q ∈ trStmts₁ q
have clear : ∀ (p : Γ' → Bool) (k : K'), ∀ q ∈ trStmts₁ q, Λ'.clear p k q ∈ trStmts₁ (Λ'.clear p k q)
Tactic: induction q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
move : ∀ (p : Γ' → Bool) (k₁ k₂ : K'), ∀ q ∈ trStmts₁ q, Λ'.move p k₁ k₂ q ∈ trStmts₁ (Λ'.move p k₁ k₂ q)
clear : ∀ (p : Γ' → Bool) (k : K'), ∀ q ∈ trStmts₁ q, Λ'.clear p k q ∈ trStmts₁ (Λ'.clear p k q)
⊢ q ∈ trStmts₁ q
have copy : ∀ q ∈ trStmts₁ q, q.copy ∈ trStmts₁ q.copy
Tactic: induction q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
move : ∀ (p : Γ' → Bool) (k₁ k₂ : K'), ∀ q ∈ trStmts₁ q, Λ'.move p k₁ k₂ q ∈ trStmts₁ (Λ'.move p k₁ k₂ q)
clear : ∀ (p : Γ' → Bool) (k : K'), ∀ q ∈ trStmts₁ q, Λ'.clear p k q ∈ trStmts₁ (Λ'.clear p k q)
copy : ∀ q ∈ trStmts₁ q, q.copy ∈ trStmts₁ q.copy
⊢ q ∈ trStmts₁ q
have push : ∀ (k : K') (s : Option Γ' → Option Γ'), ∀ q ∈ trStmts₁ q, Λ'.push k s q ∈ trStmts₁ (Λ'.push k s q)
Tactic: induction q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
move : ∀ (p : Γ' → Bool) (k₁ k₂ : K'), ∀ q ∈ trStmts₁ q, Λ'.move p k₁ k₂ q ∈ trStmts₁ (Λ'.move p k₁ k₂ q)
clear : ∀ (p : Γ' → Bool) (k : K'), ∀ q ∈ trStmts₁ q, Λ'.clear p k q ∈ trStmts₁ (Λ'.clear p k q)
copy : ∀ q ∈ trStmts₁ q, q.copy ∈ trStmts₁ q.copy
push : ∀ (k : K') (s : Option Γ' → Option Γ'), ∀ q ∈ trStmts₁ q, Λ'.push k s q ∈ trStmts₁ (Λ'.push k s q)
⊢ q ∈ trStmts₁ q
have read : ∀ (f : Option Γ' → Λ'), (∀ (a : Option Γ'), f a ∈ trStmts₁ (f a)) → Λ'.read f ∈ trStmts₁ (Λ'.read f)
Tactic: induction q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
move : ∀ (p : Γ' → Bool) (k₁ k₂ : K'), ∀ q ∈ trStmts₁ q, Λ'.move p k₁ k₂ q ∈ trStmts₁ (Λ'.move p k₁ k₂ q)
clear : ∀ (p : Γ' → Bool) (k : K'), ∀ q ∈ trStmts₁ q, Λ'.clear p k q ∈ trStmts₁ (Λ'.clear p k q)
copy : ∀ q ∈ trStmts₁ q, q.copy ∈ trStmts₁ q.copy
push : ∀ (k : K') (s : Option Γ' → Option Γ'), ∀ q ∈ trStmts₁ q, Λ'.push k s q ∈ trStmts₁ (Λ'.push k s q)
read : ∀ (f : Option Γ' → Λ'), (∀ (a : Option Γ'), f a ∈ trStmts₁ (f a)) → Λ'.read f ∈ trStmts₁ (Λ'.read f)
⊢ q ∈ trStmts₁ q
have succ : ∀ q ∈ trStmts₁ q, q.succ ∈ trStmts₁ q.succ
Tactic: induction q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
move : ∀ (p : Γ' → Bool) (k₁ k₂ : K'), ∀ q ∈ trStmts₁ q, Λ'.move p k₁ k₂ q ∈ trStmts₁ (Λ'.move p k₁ k₂ q)
clear : ∀ (p : Γ' → Bool) (k : K'), ∀ q ∈ trStmts₁ q, Λ'.clear p k q ∈ trStmts₁ (Λ'.clear p k q)
copy : ∀ q ∈ trStmts₁ q, q.copy ∈ trStmts₁ q.copy
push : ∀ (k : K') (s : Option Γ' → Option Γ'), ∀ q ∈ trStmts₁ q, Λ'.push k s q ∈ trStmts₁ (Λ'.push k s q)
read : ∀ (f : Option Γ' → Λ'), (∀ (a : Option Γ'), f a ∈ trStmts₁ (f a)) → Λ'.read f ∈ trStmts₁ (Λ'.read f)
succ : ∀ q ∈ trStmts₁ q, q.succ ∈ trStmts₁ q.succ
⊢ q ∈ trStmts₁ q
have pred : ∀ (q₁ q₂ : Λ'), q₁ ∈ trStmts₁ q₁ → q₂ ∈ trStmts₁ q₂ → q₁.pred q₂ ∈ trStmts₁ (q₁.pred q₂)
Tactic: induction q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
move : ∀ (p : Γ' → Bool) (k₁ k₂ : K'), ∀ q ∈ trStmts₁ q, Λ'.move p k₁ k₂ q ∈ trStmts₁ (Λ'.move p k₁ k₂ q)
clear : ∀ (p : Γ' → Bool) (k : K'), ∀ q ∈ trStmts₁ q, Λ'.clear p k q ∈ trStmts₁ (Λ'.clear p k q)
copy : ∀ q ∈ trStmts₁ q, q.copy ∈ trStmts₁ q.copy
push : ∀ (k : K') (s : Option Γ' → Option Γ'), ∀ q ∈ trStmts₁ q, Λ'.push k s q ∈ trStmts₁ (Λ'.push k s q)
read : ∀ (f : Option Γ' → Λ'), (∀ (a : Option Γ'), f a ∈ trStmts₁ (f a)) → Λ'.read f ∈ trStmts₁ (Λ'.read f)
succ : ∀ q ∈ trStmts₁ q, q.succ ∈ trStmts₁ q.succ
pred : ∀ (q₁ q₂ : Λ'), q₁ ∈ trStmts₁ q₁ → q₂ ∈ trStmts₁ q₂ → q₁.pred q₂ ∈ trStmts₁ (q₁.pred q₂)
⊢ q ∈ trStmts₁ q
have ret : ∀ (k : Cont'), Λ'.ret k ∈ trStmts₁ (Λ'.ret k)
Tactic: induction q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
k : Cont'
⊢ trStmts₁ (trNormal c k) ⊆ codeSupp' c k
have zero' : trStmts₁ (trNormal Code.zero' k) ⊆ trStmts₁ (trNormal Code.zero' 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)
⊢ trStmts₁ (trNormal c k) ⊆ codeSupp' c k
have succ : trStmts₁ (trNormal Code.succ k) ⊆ trStmts₁ (trNormal Code.succ k)
Tactic: cases c
Cleared hypotheses: c