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
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) <;> [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₁ (load a q)
hs : SupportsStmt S (load a q)
⊢ SupportsStmt S q₁
have h₁ : q₁ = load 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₁ = load a q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
have load : ∀ (IH : ∀ (h : load a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (load a q)), SupportsStmt S (load 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.load a q ∨ q₁ ∈ stmts₁ q
load :
  ∀ (IH : ∀ (h : Stmt.load a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.load a q)),
    SupportsStmt S (Stmt.load a q)
⊢ SupportsStmt S q₁
have load₁ : ∀ (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₁ = load a q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
have load : ∀ (IH : ∀ (h : load a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (load a q)), SupportsStmt S (load 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 : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = Stmt.load a q ∨ q₁ ∈ stmts₁ q
load :
  ∀ (IH : ∀ (h : Stmt.load a q ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S (Stmt.load a q)),
    SupportsStmt S (Stmt.load a q)
⊢ SupportsStmt S q₁
have load₁ : ∀ (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 (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
⊢ SupportsStmt S q₁
have branch : ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
  (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
  (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁) (h : q₁ ∈ stmts₁ (branch p q₁_1 q₂))
  (hs : SupportsStmt S (branch p q₁_1 q₂)), SupportsStmt S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁) (h : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂))
    (hs : SupportsStmt S (Stmt.branch p q₁_1 q₂)), SupportsStmt S q₁
⊢ SupportsStmt S q₁
have branch₁ : ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
  (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
  (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁)
  (hs : SupportsStmt S q₁_1 ∧ SupportsStmt S q₂) (h : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
  SupportsStmt S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁) (h : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂))
    (hs : SupportsStmt S (Stmt.branch p q₁_1 q₂)), SupportsStmt S q₁
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁)
    (hs : SupportsStmt S q₁_1 ∧ SupportsStmt S q₂) (h : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    SupportsStmt S q₁
⊢ SupportsStmt S q₁
have goto : ∀ (l : Γ → σ → Λ) (h : q₁ ∈ stmts₁ (goto l)) (hs : SupportsStmt S (goto l)), SupportsStmt S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁) (h : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂))
    (hs : SupportsStmt S (Stmt.branch p q₁_1 q₂)), SupportsStmt S q₁
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁)
    (hs : SupportsStmt S q₁_1 ∧ SupportsStmt S q₂) (h : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    SupportsStmt S q₁
goto : ∀ (l : Γ → σ → Λ) (h : q₁ ∈ stmts₁ (Stmt.goto l)) (hs : SupportsStmt S (Stmt.goto l)), SupportsStmt S q₁
⊢ SupportsStmt S q₁
have goto₁ : ∀ (l : Γ → σ → Λ) (hs : ∀ (a : Γ) (v : σ), l a v ∈ S) (h : q₁ = Stmt.goto l), SupportsStmt S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁) (h : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂))
    (hs : SupportsStmt S (Stmt.branch p q₁_1 q₂)), SupportsStmt S q₁
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁)
    (hs : SupportsStmt S q₁_1 ∧ SupportsStmt S q₂) (h : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    SupportsStmt S q₁
goto : ∀ (l : Γ → σ → Λ) (h : q₁ ∈ stmts₁ (Stmt.goto l)) (hs : SupportsStmt S (Stmt.goto l)), SupportsStmt S q₁
goto₁ : ∀ (l : Γ → σ → Λ) (hs : ∀ (a : Γ) (v : σ), l a v ∈ S) (h : q₁ = Stmt.goto l), SupportsStmt S q₁
⊢ SupportsStmt S q₁
have halt : ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ halt) q₁)
  (hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S halt), SupportsStmt S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁) (h : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂))
    (hs : SupportsStmt S (Stmt.branch p q₁_1 q₂)), SupportsStmt S q₁
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁)
    (hs : SupportsStmt S q₁_1 ∧ SupportsStmt S q₂) (h : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    SupportsStmt S q₁
goto : ∀ (l : Γ → σ → Λ) (h : q₁ ∈ stmts₁ (Stmt.goto l)) (hs : SupportsStmt S (Stmt.goto l)), SupportsStmt S q₁
goto₁ : ∀ (l : Γ → σ → Λ) (hs : ∀ (a : Γ) (v : σ), l a v ∈ S) (h : q₁ = Stmt.goto l), SupportsStmt S q₁
halt :
  ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ Stmt.halt) q₁)
    (hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt), SupportsStmt S q₁
⊢ SupportsStmt S q₁
have halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt), SupportsStmt S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁) (h : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂))
    (hs : SupportsStmt S (Stmt.branch p q₁_1 q₂)), SupportsStmt S q₁
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁)
    (hs : SupportsStmt S q₁_1 ∧ SupportsStmt S q₂) (h : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    SupportsStmt S q₁
goto : ∀ (l : Γ → σ → Λ) (h : q₁ ∈ stmts₁ (Stmt.goto l)) (hs : SupportsStmt S (Stmt.goto l)), SupportsStmt S q₁
goto₁ : ∀ (l : Γ → σ → Λ) (hs : ∀ (a : Γ) (v : σ), l a v ∈ S) (h : q₁ = Stmt.goto l), SupportsStmt S q₁
halt :
  ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ Stmt.halt) q₁)
    (hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt), SupportsStmt S q₁
halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt), SupportsStmt S q₁
⊢ SupportsStmt S q₁
have move : ∀ (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₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁) (h : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂))
    (hs : SupportsStmt S (Stmt.branch p q₁_1 q₂)), SupportsStmt S q₁
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁)
    (hs : SupportsStmt S q₁_1 ∧ SupportsStmt S q₂) (h : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    SupportsStmt S q₁
goto : ∀ (l : Γ → σ → Λ) (h : q₁ ∈ stmts₁ (Stmt.goto l)) (hs : SupportsStmt S (Stmt.goto l)), SupportsStmt S q₁
goto₁ : ∀ (l : Γ → σ → Λ) (hs : ∀ (a : Γ) (v : σ), l a v ∈ S) (h : q₁ = Stmt.goto l), SupportsStmt S q₁
halt :
  ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ Stmt.halt) q₁)
    (hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt), SupportsStmt S q₁
halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt), SupportsStmt S q₁
move :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (h : q₁ ∈ stmts₁ (Stmt.move a q)) (hs : SupportsStmt S (Stmt.move a q)), SupportsStmt S q₁
⊢ SupportsStmt S q₁
have move₁ : ∀ (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), SupportsStmt S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁) (h : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂))
    (hs : SupportsStmt S (Stmt.branch p q₁_1 q₂)), SupportsStmt S q₁
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁)
    (hs : SupportsStmt S q₁_1 ∧ SupportsStmt S q₂) (h : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    SupportsStmt S q₁
goto : ∀ (l : Γ → σ → Λ) (h : q₁ ∈ stmts₁ (Stmt.goto l)) (hs : SupportsStmt S (Stmt.goto l)), SupportsStmt S q₁
goto₁ : ∀ (l : Γ → σ → Λ) (hs : ∀ (a : Γ) (v : σ), l a v ∈ S) (h : q₁ = Stmt.goto l), SupportsStmt S q₁
halt :
  ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ Stmt.halt) q₁)
    (hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt), SupportsStmt S q₁
halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt), SupportsStmt S q₁
move :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (h : q₁ ∈ stmts₁ (Stmt.move a q)) (hs : SupportsStmt S (Stmt.move a q)), SupportsStmt S q₁
move₁ :
  ∀ (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), SupportsStmt S q₁
⊢ SupportsStmt S q₁
have write : ∀ (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₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁) (h : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂))
    (hs : SupportsStmt S (Stmt.branch p q₁_1 q₂)), SupportsStmt S q₁
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁)
    (hs : SupportsStmt S q₁_1 ∧ SupportsStmt S q₂) (h : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    SupportsStmt S q₁
goto : ∀ (l : Γ → σ → Λ) (h : q₁ ∈ stmts₁ (Stmt.goto l)) (hs : SupportsStmt S (Stmt.goto l)), SupportsStmt S q₁
goto₁ : ∀ (l : Γ → σ → Λ) (hs : ∀ (a : Γ) (v : σ), l a v ∈ S) (h : q₁ = Stmt.goto l), SupportsStmt S q₁
halt :
  ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ Stmt.halt) q₁)
    (hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt), SupportsStmt S q₁
halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt), SupportsStmt S q₁
move :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (h : q₁ ∈ stmts₁ (Stmt.move a q)) (hs : SupportsStmt S (Stmt.move a q)), SupportsStmt S q₁
move₁ :
  ∀ (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), SupportsStmt S q₁
write :
  ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (h : q₁ ∈ stmts₁ (Stmt.write a q)) (hs : SupportsStmt S (Stmt.write a q)), SupportsStmt S q₁
⊢ SupportsStmt S q₁
have write₁ : ∀ (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), SupportsStmt S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
branch :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁) (h : q₁ ∈ stmts₁ (Stmt.branch p q₁_1 q₂))
    (hs : SupportsStmt S (Stmt.branch p q₁_1 q₂)), SupportsStmt S q₁
branch₁ :
  ∀ (p : Γ → σ → Bool) (q₁_1 q₂ : Stmt Γ Λ σ)
    (IH₁ : ∀ (h : q₁ ∈ stmts₁ q₁_1) (hs : SupportsStmt S q₁_1), SupportsStmt S q₁)
    (IH₂ : ∀ (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂), SupportsStmt S q₁)
    (hs : SupportsStmt S q₁_1 ∧ SupportsStmt S q₂) (h : q₁ = Stmt.branch p q₁_1 q₂ ∨ q₁ ∈ stmts₁ q₁_1 ∨ q₁ ∈ stmts₁ q₂),
    SupportsStmt S q₁
goto : ∀ (l : Γ → σ → Λ) (h : q₁ ∈ stmts₁ (Stmt.goto l)) (hs : SupportsStmt S (Stmt.goto l)), SupportsStmt S q₁
goto₁ : ∀ (l : Γ → σ → Λ) (hs : ∀ (a : Γ) (v : σ), l a v ∈ S) (h : q₁ = Stmt.goto l), SupportsStmt S q₁
halt :
  ∀ (h : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ Stmt.halt) q₁)
    (hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt), SupportsStmt S q₁
halt₁ : ∀ (hs : True) (h : q₁ = Stmt.halt), SupportsStmt S q₁
move :
  ∀ (a : Dir) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (h : q₁ ∈ stmts₁ (Stmt.move a q)) (hs : SupportsStmt S (Stmt.move a q)), SupportsStmt S q₁
move₁ :
  ∀ (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), SupportsStmt S q₁
write :
  ∀ (a : Γ → σ → Γ) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (h : q₁ ∈ stmts₁ (Stmt.write a q)) (hs : SupportsStmt S (Stmt.write a q)), SupportsStmt S q₁
write₁ :
  ∀ (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), SupportsStmt S q₁
⊢ SupportsStmt S q₁
have load : ∀ (a : Γ → σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
  (h : q₁ ∈ stmts₁ (load a q)) (hs : SupportsStmt S (load a q)), SupportsStmt S q₁
Tactic: induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]
Cleared hypotheses: q₂, h, hs