awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
Γ' : Type u_2
inst_1 : Inhabited Γ'
Λ : Type u_3
inst_2 : Inhabited Λ
Λ' : Type u_4
inst_3 : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
e : step M c = none
⊢ match (motive := Option (Cfg Γ Λ) → Prop) none with
  | some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none
have none : match (motive := Option (Cfg Γ Λ) → Prop) none with
| some b₁ =>
  ∃ (b₂ : Cfg Γ' Λ'),
    (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
      Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
| none => Option.map (Cfg.map f₁ g₁.f) none = none
Tactic: rw [← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs, e]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
Γ' : Type u_2
inst_1 : Inhabited Γ'
Λ : Type u_3
inst_2 : Inhabited Λ
Λ' : Type u_4
inst_3 : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
val : Cfg Γ Λ
e : step M c = some val
⊢ match (motive := Option (Cfg Γ Λ) → Prop) some val with
  | some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none
have some : Cfg.map f₁ g₁.f val ∈ step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c)
Tactic: refine ⟨_, ⟨step_supports M ss e cs, rfl⟩, TransGen.single ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
Γ' : Type u_2
inst_1 : Inhabited Γ'
Λ : Type u_3
inst_2 : Inhabited Λ
Λ' : Type u_4
inst_3 : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
val : Cfg Γ Λ
e : step M c = some val
⊢ Cfg.map f₁ g₁.f val ∈ step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c)
have some : Cfg.map f₁ g₁.f val ∈ Option.map (Cfg.map f₁ g₁.f) (some val)
Tactic: rw [← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs, e]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q : Stmt Γ Λ σ
⊢ q ∈ stmts₁ q
have move : ∀ (a : Dir) (a_1 : Stmt Γ Λ σ), move a a_1 ∈ stmts₁ (move a a_1)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q : Stmt Γ Λ σ
move : ∀ (a : Dir) (a_1 : Stmt Γ Λ σ), Stmt.move a a_1 ∈ stmts₁ (Stmt.move a a_1)
⊢ q ∈ stmts₁ q
have write : ∀ (a : Γ → σ → Γ) (a_1 : Stmt Γ Λ σ), write a a_1 ∈ stmts₁ (write a a_1)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q : Stmt Γ Λ σ
move : ∀ (a : Dir) (a_1 : Stmt Γ Λ σ), Stmt.move a a_1 ∈ stmts₁ (Stmt.move a a_1)
write : ∀ (a : Γ → σ → Γ) (a_1 : Stmt Γ Λ σ), Stmt.write a a_1 ∈ stmts₁ (Stmt.write a a_1)
⊢ q ∈ stmts₁ q
have load : ∀ (a : Γ → σ → σ) (a_1 : Stmt Γ Λ σ), load a a_1 ∈ stmts₁ (load a a_1)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q : Stmt Γ Λ σ
move : ∀ (a : Dir) (a_1 : Stmt Γ Λ σ), Stmt.move a a_1 ∈ stmts₁ (Stmt.move a a_1)
write : ∀ (a : Γ → σ → Γ) (a_1 : Stmt Γ Λ σ), Stmt.write a a_1 ∈ stmts₁ (Stmt.write a a_1)
load : ∀ (a : Γ → σ → σ) (a_1 : Stmt Γ Λ σ), Stmt.load a a_1 ∈ stmts₁ (Stmt.load a a_1)
⊢ q ∈ stmts₁ q
have branch : ∀ (a : Γ → σ → Bool) (a_1 a_2 : Stmt Γ Λ σ), branch a a_1 a_2 ∈ stmts₁ (branch a a_1 a_2)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q : Stmt Γ Λ σ
move : ∀ (a : Dir) (a_1 : Stmt Γ Λ σ), Stmt.move a a_1 ∈ stmts₁ (Stmt.move a a_1)
write : ∀ (a : Γ → σ → Γ) (a_1 : Stmt Γ Λ σ), Stmt.write a a_1 ∈ stmts₁ (Stmt.write a a_1)
load : ∀ (a : Γ → σ → σ) (a_1 : Stmt Γ Λ σ), Stmt.load a a_1 ∈ stmts₁ (Stmt.load a a_1)
branch : ∀ (a : Γ → σ → Bool) (a_1 a_2 : Stmt Γ Λ σ), Stmt.branch a a_1 a_2 ∈ stmts₁ (Stmt.branch a a_1 a_2)
⊢ q ∈ stmts₁ q
have goto : ∀ (a : Γ → σ → Λ), goto a ∈ stmts₁ (goto a)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q : Stmt Γ Λ σ
move : ∀ (a : Dir) (a_1 : Stmt Γ Λ σ), Stmt.move a a_1 ∈ stmts₁ (Stmt.move a a_1)
write : ∀ (a : Γ → σ → Γ) (a_1 : Stmt Γ Λ σ), Stmt.write a a_1 ∈ stmts₁ (Stmt.write a a_1)
load : ∀ (a : Γ → σ → σ) (a_1 : Stmt Γ Λ σ), Stmt.load a a_1 ∈ stmts₁ (Stmt.load a a_1)
branch : ∀ (a : Γ → σ → Bool) (a_1 a_2 : Stmt Γ Λ σ), Stmt.branch a a_1 a_2 ∈ stmts₁ (Stmt.branch a a_1 a_2)
goto : ∀ (a : Γ → σ → Λ), Stmt.goto a ∈ stmts₁ (Stmt.goto a)
⊢ q ∈ stmts₁ q
have halt : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ halt) halt
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁_1
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₁), q₀ ∈ stmts₁ q₁
IH₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂
h₁₂ : q₁_1 ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
have h₁₃ : q₁_1 = branch p q₁ q₂ ∨ q₁_1 ∈ stmts₁ q₁ ∨ q₁_1 ∈ stmts₁ q₂
Tactic: simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁_1
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₁), q₀ ∈ stmts₁ q₁
IH₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂
h₁₂ : q₁_1 = branch p q₁ q₂ ∨ q₁_1 ∈ stmts₁ q₁ ∨ q₁_1 ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
have branch : ∀ (h₀₁ : q₀ ∈ stmts₁ (branch p q₁ q₂)) (IH₁ : ∀ (h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₁), q₀ ∈ stmts₁ q₁)
  (IH₂ : ∀ (h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂), q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
Tactic: rcases h₁₂ with (rfl | h₁₂ | h₁₂)
Cleared hypotheses: q₁_1, h₀₁, IH₁, IH₂, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁_1
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₁), q₀ ∈ stmts₁ q₁
IH₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂
h₁₂ : q₁_1 = Stmt.branch p q₁ q₂ ∨ q₁_1 ∈ stmts₁ q₁ ∨ q₁_1 ∈ stmts₁ q₂
branch :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Stmt.branch p q₁ q₂)) (IH₁ : ∀ (h₁₂ : Stmt.branch p q₁ q₂ ∈ stmts₁ q₁), q₀ ∈ stmts₁ q₁)
    (IH₂ : ∀ (h₁₂ : Stmt.branch p q₁ q₂ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂),
    q₀ ∈ insert (Stmt.branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
⊢ q₀ ∈ insert (Stmt.branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
have branch₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₁), q₀ ∈ insert (Stmt.branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
Tactic: rcases h₁₂ with (rfl | h₁₂ | h₁₂)
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁_1
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₁), q₀ ∈ stmts₁ q₁
IH₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂
h₁₂ : q₁_1 = Stmt.branch p q₁ q₂ ∨ q₁_1 ∈ stmts₁ q₁ ∨ q₁_1 ∈ stmts₁ q₂
branch :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Stmt.branch p q₁ q₂)) (IH₁ : ∀ (h₁₂ : Stmt.branch p q₁ q₂ ∈ stmts₁ q₁), q₀ ∈ stmts₁ q₁)
    (IH₂ : ∀ (h₁₂ : Stmt.branch p q₁ q₂ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂),
    q₀ ∈ insert (Stmt.branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
branch₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₁), q₀ ∈ insert (Stmt.branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
⊢ q₀ ∈ insert (Stmt.branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
have branch₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₂), q₀ ∈ insert (Stmt.branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
Tactic: rcases h₁₂ with (rfl | h₁₂ | h₁₂)
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
l : Γ → σ → Λ
h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) {goto l} q₁
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {goto l} q₀
have h₁₃ : q₁ = goto l
Tactic: simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
l : Γ → σ → Λ
h₁₂ : q₁ = goto l
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {goto l} q₀
have h₂ : q₀ ∈ stmts₁ (goto l)
Tactic: subst h₁₂
Cleared hypotheses: q₁, h₀₁, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) {halt} q₁
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {halt} q₀
have h₁₃ : q₁ = halt
Tactic: simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {halt} q₀
have h₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ halt) q₀
Tactic: subst h₁₂
Cleared hypotheses: q₁, h₀₁, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ insert (move a q) (stmts₁ q)
⊢ q₀ ∈ insert (move a q) (stmts₁ q)
have h₁₃ : q₁ = move a q ∨ q₁ ∈ stmts₁ q
Tactic: simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ = move a q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (move a q) (stmts₁ q)
have move : ∀ (h₀₁ : q₀ ∈ stmts₁ (move a q)) (IH : ∀ (h₁₂ : move a q ∈ stmts₁ q), q₀ ∈ stmts₁ q), q₀ ∈ insert (move a q) (stmts₁ q)
Tactic: rcases h₁₂ with rfl | h₁₂
Cleared hypotheses: q₁, h₀₁, IH, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q
move :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Stmt.move a q)) (IH : ∀ (h₁₂ : Stmt.move a q ∈ stmts₁ q), q₀ ∈ stmts₁ q),
    q₀ ∈ insert (Stmt.move a q) (stmts₁ q)
⊢ q₀ ∈ insert (Stmt.move a q) (stmts₁ q)
have move₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ insert (Stmt.move a q) (stmts₁ q)
Tactic: rcases h₁₂ with rfl | h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ insert (write a q) (stmts₁ q)
⊢ q₀ ∈ insert (write a q) (stmts₁ q)
have h₁₃ : q₁ = write a q ∨ q₁ ∈ stmts₁ q
Tactic: simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ = write a q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (write a q) (stmts₁ q)
have write : ∀ (h₀₁ : q₀ ∈ stmts₁ (write a q)) (IH : ∀ (h₁₂ : write a q ∈ stmts₁ q), q₀ ∈ stmts₁ q),
  q₀ ∈ insert (write a q) (stmts₁ q)
Tactic: rcases h₁₂ with rfl | h₁₂
Cleared hypotheses: q₁, h₀₁, IH, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ = Stmt.write a q ∨ q₁ ∈ stmts₁ q
write :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Stmt.write a q)) (IH : ∀ (h₁₂ : Stmt.write a q ∈ stmts₁ q), q₀ ∈ stmts₁ q),
    q₀ ∈ insert (Stmt.write a q) (stmts₁ q)
⊢ q₀ ∈ insert (Stmt.write a q) (stmts₁ q)
have write₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ insert (Stmt.write a q) (stmts₁ q)
Tactic: rcases h₁₂ with rfl | h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ insert (load a q) (stmts₁ q)
⊢ q₀ ∈ insert (load a q) (stmts₁ q)
have h₁₃ : q₁ = load a q ∨ q₁ ∈ stmts₁ q
Tactic: simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ = load a q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a q) (stmts₁ q)
have load : ∀ (h₀₁ : q₀ ∈ stmts₁ (load a q)) (IH : ∀ (h₁₂ : load a q ∈ stmts₁ q), q₀ ∈ stmts₁ q), q₀ ∈ insert (load a q) (stmts₁ q)
Tactic: rcases h₁₂ with rfl | h₁₂
Cleared hypotheses: q₁, h₀₁, IH, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ = Stmt.load a q ∨ q₁ ∈ stmts₁ q
load :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Stmt.load a q)) (IH : ∀ (h₁₂ : Stmt.load a q ∈ stmts₁ q), q₀ ∈ stmts₁ q),
    q₀ ∈ insert (Stmt.load a q) (stmts₁ q)
⊢ q₀ ∈ insert (Stmt.load a q) (stmts₁ q)
have load₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ insert (Stmt.load a q) (stmts₁ q)
Tactic: rcases h₁₂ with rfl | h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
⊢ q₀ ∈ stmts₁ q₂
have branch : ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₁_1), q₀ ∈ stmts₁ q₁_1)
  (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂) (h₁₂ : q₁ ∈ stmts₁ (branch p q₁_1 q₂)),
  q₀ ∈ stmts₁ (branch p q₁_1 q₂)
Tactic: induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)
  | branch p q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · grind
    · grind
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | _ _ q IH =>
    rcases h₁₂ with rfl | h₁₂
    · exact h₀₁
    · grind
Cleared hypotheses: q₂, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₁_1), q₀ ∈ stmts₁ q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂) (h₁₂ : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂)),
    q₀ ∈ stmts₁ (Stmt.branch p q₁_1 q₂)
⊢ q₀ ∈ stmts₁ q₂
have branch₁ : ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₁_1), q₀ ∈ stmts₁ q₁_1)
  (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂)
  (h₁₂ : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
  q₀ ∈ insert (Stmt.branch p q₁_1 q₂) (stmts₁ q₁_1 ∪ stmts₁ q₂)
Tactic: induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)
  | branch p q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · grind
    · grind
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | _ _ q IH =>
    rcases h₁₂ with rfl | h₁₂
    · exact h₀₁
    · grind
Cleared hypotheses: q₂, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₁_1), q₀ ∈ stmts₁ q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂) (h₁₂ : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂)),
    q₀ ∈ stmts₁ (Stmt.branch p q₁_1 q₂)
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₁_1), q₀ ∈ stmts₁ q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂)
    (h₁₂ : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    q₀ ∈ insert (Stmt.branch p q₁_1 q₂) (stmts₁ q₁_1 ∪ stmts₁ q₂)
⊢ q₀ ∈ stmts₁ q₂
have goto : ∀ (l : Γ → σ → Λ) (h₁₂ : q₁ ∈ stmts₁ (goto l)), q₀ ∈ stmts₁ (goto l)
Tactic: induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)
  | branch p q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · grind
    · grind
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | _ _ q IH =>
    rcases h₁₂ with rfl | h₁₂
    · exact h₀₁
    · grind
Cleared hypotheses: q₂, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₁_1), q₀ ∈ stmts₁ q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂) (h₁₂ : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂)),
    q₀ ∈ stmts₁ (Stmt.branch p q₁_1 q₂)
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₁_1), q₀ ∈ stmts₁ q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂)
    (h₁₂ : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    q₀ ∈ insert (Stmt.branch p q₁_1 q₂) (stmts₁ q₁_1 ∪ stmts₁ q₂)
goto : ∀ (l : Γ → σ → Λ) (h₁₂ : q₁ ∈ stmts₁ (Stmt.goto l)), q₀ ∈ stmts₁ (Stmt.goto l)
⊢ q₀ ∈ stmts₁ q₂
have goto₁ : ∀ (l : Γ → σ → Λ) (h₁₂ : q₁ = Stmt.goto l), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.goto l} q₀
Tactic: induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)
  | branch p q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · grind
    · grind
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | _ _ q IH =>
    rcases h₁₂ with rfl | h₁₂
    · exact h₀₁
    · grind
Cleared hypotheses: q₂, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₁_1), q₀ ∈ stmts₁ q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂) (h₁₂ : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂)),
    q₀ ∈ stmts₁ (Stmt.branch p q₁_1 q₂)
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₁_1), q₀ ∈ stmts₁ q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂)
    (h₁₂ : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    q₀ ∈ insert (Stmt.branch p q₁_1 q₂) (stmts₁ q₁_1 ∪ stmts₁ q₂)
goto : ∀ (l : Γ → σ → Λ) (h₁₂ : q₁ ∈ stmts₁ (Stmt.goto l)), q₀ ∈ stmts₁ (Stmt.goto l)
goto₁ : ∀ (l : Γ → σ → Λ) (h₁₂ : q₁ = Stmt.goto l), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.goto l} q₀
⊢ q₀ ∈ stmts₁ q₂
have halt : ∀ (h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ halt) q₁),
  Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ halt) q₀
Tactic: induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)
  | branch p q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · grind
    · grind
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | _ _ q IH =>
    rcases h₁₂ with rfl | h₁₂
    · exact h₀₁
    · grind
Cleared hypotheses: q₂, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₁_1), q₀ ∈ stmts₁ q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂) (h₁₂ : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂)),
    q₀ ∈ stmts₁ (Stmt.branch p q₁_1 q₂)
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ) (IH₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₁_1), q₀ ∈ stmts₁ q₁_1)
    (IH₂ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂)
    (h₁₂ : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    q₀ ∈ insert (Stmt.branch p q₁_1 q₂) (stmts₁ q₁_1 ∪ stmts₁ q₂)
goto : ∀ (l : Γ → σ → Λ) (h₁₂ : q₁ ∈ stmts₁ (Stmt.goto l)), q₀ ∈ stmts₁ (Stmt.goto l)
goto₁ : ∀ (l : Γ → σ → Λ) (h₁₂ : q₁ = Stmt.goto l), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.goto l} q₀
halt :
  ∀ (h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ Stmt.halt) q₁),
    Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ Stmt.halt) q₀
⊢ q₀ ∈ stmts₁ q₂
have halt₁ : ∀ (h₁₂ : q₁ = Stmt.halt), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.halt} q₀
Tactic: induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)
  | branch p q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · grind
    · grind
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | _ _ q IH =>
    rcases h₁₂ with rfl | h₁₂
    · exact h₀₁
    · grind
Cleared hypotheses: q₂, h₁₂