awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀
halt₁ : ∀ (h₁₂ : q₁ = Stmt.halt), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.halt} q₀
⊢ q₀ ∈ stmts₁ q₂
have move : ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (move a q)),
  q₀ ∈ stmts₁ (move a 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₀
halt₁ : ∀ (h₁₂ : q₁ = Stmt.halt), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.halt} q₀
move :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (Stmt.move a q)),
    q₀ ∈ stmts₁ (Stmt.move a q)
⊢ q₀ ∈ stmts₁ q₂
have move₁ : ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q),
  q₀ ∈ insert (Stmt.move a q) (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₂)
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₀
halt₁ : ∀ (h₁₂ : q₁ = Stmt.halt), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.halt} q₀
move :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (Stmt.move a q)),
    q₀ ∈ stmts₁ (Stmt.move a q)
move₁ :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q),
    q₀ ∈ insert (Stmt.move a q) (stmts₁ q)
⊢ q₀ ∈ stmts₁ q₂
have write : ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (write a q)),
  q₀ ∈ stmts₁ (write a 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₀
halt₁ : ∀ (h₁₂ : q₁ = Stmt.halt), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.halt} q₀
move :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (Stmt.move a q)),
    q₀ ∈ stmts₁ (Stmt.move a q)
move₁ :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q),
    q₀ ∈ insert (Stmt.move a q) (stmts₁ q)
write :
  ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (Stmt.write a q)),
    q₀ ∈ stmts₁ (Stmt.write a q)
⊢ q₀ ∈ stmts₁ q₂
have write₁ : ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q)
  (h₁₂ : q₁ = Stmt.write a q ∨ q₁ ∈ stmts₁ q), q₀ ∈ insert (Stmt.write a q) (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₂)
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₀
halt₁ : ∀ (h₁₂ : q₁ = Stmt.halt), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.halt} q₀
move :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (Stmt.move a q)),
    q₀ ∈ stmts₁ (Stmt.move a q)
move₁ :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q),
    q₀ ∈ insert (Stmt.move a q) (stmts₁ q)
write :
  ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (Stmt.write a q)),
    q₀ ∈ stmts₁ (Stmt.write a q)
write₁ :
  ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q)
    (h₁₂ : q₁ = Stmt.write a q ∨ q₁ ∈ stmts₁ q), q₀ ∈ insert (Stmt.write a q) (stmts₁ q)
⊢ q₀ ∈ stmts₁ q₂
have load : ∀ (a : Γ → σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (load a q)),
  q₀ ∈ stmts₁ (load a 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₀
halt₁ : ∀ (h₁₂ : q₁ = Stmt.halt), Membership.mem (γ := Finset (Stmt Γ Λ σ)) {Stmt.halt} q₀
move :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (Stmt.move a q)),
    q₀ ∈ stmts₁ (Stmt.move a q)
move₁ :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q),
    q₀ ∈ insert (Stmt.move a q) (stmts₁ q)
write :
  ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (Stmt.write a q)),
    q₀ ∈ stmts₁ (Stmt.write a q)
write₁ :
  ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q)
    (h₁₂ : q₁ = Stmt.write a q ∨ q₁ ∈ stmts₁ q), q₀ ∈ insert (Stmt.write a q) (stmts₁ q)
load :
  ∀ (a : Γ → σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q) (h₁₂ : q₁ ∈ stmts₁ (Stmt.load a q)),
    q₀ ∈ stmts₁ (Stmt.load a q)
⊢ q₀ ∈ stmts₁ q₂
have load₁ : ∀ (a : Γ → σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q)
  (h₁₂ : q₁ = Stmt.load a q ∨ q₁ ∈ stmts₁ q), q₀ ∈ insert (Stmt.load a q) (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 Γ Λ σ
intro : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂), stmts₁ q₁ ⊆ stmts₁ q₂
⊢ q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂
have intro₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q₂) ⦃q₀ : Stmt Γ Λ σ⦄, q₀ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₂
Tactic: classical
  intro h₁₂ q₀ h₀₁
  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
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h : q₁_1 ∈ stmts₁ q₁) (hs : SupportsStmt S q₁), SupportsStmt S q₁_1
IH₂ : ∀ (h : q₁_1 ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁_1
h : q₁_1 ∈ stmts₁ (branch p q₁ q₂)
hs : SupportsStmt S (branch p q₁ q₂)
⊢ SupportsStmt S q₁_1
have h₁ : q₁_1 = branch p q₁ q₂ ∨ q₁_1 ∈ stmts₁ q₁ ∨ q₁_1 ∈ stmts₁ q₂
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h : q₁_1 ∈ stmts₁ q₁) (hs : SupportsStmt S q₁), SupportsStmt S q₁_1
IH₂ : ∀ (h : q₁_1 ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁_1
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁_1 = branch p q₁ q₂ ∨ q₁_1 ∈ stmts₁ q₁ ∨ q₁_1 ∈ stmts₁ q₂
⊢ SupportsStmt S q₁_1
have branch : ∀ (IH₁ : ∀ (h : branch p q₁ q₂ ∈ stmts₁ q₁) (hs : SupportsStmt S q₁), SupportsStmt S (branch p q₁ q₂))
  (IH₂ : ∀ (h : branch p q₁ q₂ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S (branch p q₁ q₂)),
  SupportsStmt S (branch p q₁ q₂)
Tactic: rcases h with (rfl | h | h)
Cleared hypotheses: q₁_1, IH₁, IH₂, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h : q₁_1 ∈ stmts₁ q₁) (hs : SupportsStmt S q₁), SupportsStmt S q₁_1
IH₂ : ∀ (h : q₁_1 ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁_1
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁_1 = Stmt.branch p q₁ q₂ ∨ q₁_1 ∈ stmts₁ q₁ ∨ q₁_1 ∈ stmts₁ q₂
branch :
  ∀ (IH₁ : ∀ (h : Stmt.branch p q₁ q₂ ∈ stmts₁ q₁) (hs : SupportsStmt S q₁), SupportsStmt S (Stmt.branch p q₁ q₂))
    (IH₂ : ∀ (h : Stmt.branch p q₁ q₂ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S (Stmt.branch p q₁ q₂)),
    SupportsStmt S (Stmt.branch p q₁ q₂)
⊢ SupportsStmt S q₁_1
have branch₁ : ∀ (h : q₁_1 ∈ stmts₁ q₁), SupportsStmt S q₁_1
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
S : Finset Λ
q₁_1 : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h : q₁_1 ∈ stmts₁ q₁) (hs : SupportsStmt S q₁), SupportsStmt S q₁_1
IH₂ : ∀ (h : q₁_1 ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁_1
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁_1 = Stmt.branch p q₁ q₂ ∨ q₁_1 ∈ stmts₁ q₁ ∨ q₁_1 ∈ stmts₁ q₂
branch :
  ∀ (IH₁ : ∀ (h : Stmt.branch p q₁ q₂ ∈ stmts₁ q₁) (hs : SupportsStmt S q₁), SupportsStmt S (Stmt.branch p q₁ q₂))
    (IH₂ : ∀ (h : Stmt.branch p q₁ q₂ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S (Stmt.branch p q₁ q₂)),
    SupportsStmt S (Stmt.branch p q₁ q₂)
branch₁ : ∀ (h : q₁_1 ∈ stmts₁ q₁), SupportsStmt S q₁_1
⊢ SupportsStmt S q₁_1
have branch₂ : ∀ (h : q₁_1 ∈ stmts₁ q₂), SupportsStmt S q₁_1
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
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : Γ → σ → Λ
h : q₁ ∈ stmts₁ (goto l)
hs : SupportsStmt S (goto l)
⊢ SupportsStmt S q₁
have h₁ : q₁ = goto l
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : Γ → σ → Λ
hs : ∀ (a : Γ) (v : σ), l a v ∈ S
h : q₁ = goto l
⊢ SupportsStmt S q₁
have goto : SupportsStmt S (goto l)
Tactic: subst h
Cleared hypotheses: q₁, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ halt) q₁
hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S halt
⊢ SupportsStmt S q₁
have h₁ : q₁ = halt
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
hs : True
h : q₁ = halt
⊢ SupportsStmt S q₁
have halt : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S halt
Tactic: subst h
Cleared hypotheses: q₁, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
h : q₁ ∈ stmts₁ (move a q)
hs : SupportsStmt S (move a q)
⊢ SupportsStmt S q₁
have h₁ : q₁ = move a q ∨ q₁ ∈ stmts₁ q
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = move a q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
have move : ∀ (IH : ∀ (h : move a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (move a q)), SupportsStmt S (move a q)
Tactic: rcases h with (rfl | h)
Cleared hypotheses: q₁, IH, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q
move :
  ∀ (IH : ∀ (h : Stmt.move a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.move a q)),
    SupportsStmt S (Stmt.move a q)
⊢ SupportsStmt S q₁
have move₁ : ∀ (h : q₁ ∈ stmts₁ q), SupportsStmt S 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = move a q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
have move : ∀ (IH : ∀ (h : move a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (move a q)), SupportsStmt S (move a q)
Tactic: rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₁, IH, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q
move :
  ∀ (IH : ∀ (h : Stmt.move a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.move a q)),
    SupportsStmt S (Stmt.move a q)
⊢ SupportsStmt S q₁
have move₁ : ∀ (h : q₁ ∈ stmts₁ q), SupportsStmt S q₁
Tactic: rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
h : q₁ ∈ stmts₁ (write a q)
hs : SupportsStmt S (write a q)
⊢ SupportsStmt S q₁
have h₁ : q₁ = write a q ∨ q₁ ∈ stmts₁ q
Tactic: simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = write a q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
have write : ∀ (IH : ∀ (h : write a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (write a q)), SupportsStmt S (write a q)
Tactic: rcases h with (rfl | h)
Cleared hypotheses: q₁, IH, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = Stmt.write a q ∨ q₁ ∈ stmts₁ q
write :
  ∀ (IH : ∀ (h : Stmt.write a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.write a q)),
    SupportsStmt S (Stmt.write a q)
⊢ SupportsStmt S q₁
have write₁ : ∀ (h : q₁ ∈ stmts₁ q), SupportsStmt S 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
S : Finset Λ
q₁ : Stmt Γ Λ σ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = write a q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
have write : ∀ (IH : ∀ (h : write a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (write a q)), SupportsStmt S (write a q)
Tactic: rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₁, IH, h