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 Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
e : M q T.head = some (q', s)
⊢ Reaches₁ (TM1.step (tr M)) { l := some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
    {
      l :=
        match (motive := Bool → Option (Λ' Γ Λ))
          match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
            M q'
              (Tape.head
                (match (motive := TM0.Stmt Γ → Tape Γ) s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T)) with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
have some : ∀ (e : M q T.head = some (q', s)),
  Reaches₁ (TM1.step (tr M)) { l := some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
    {
      l :=
        match (motive := Bool → Option (Λ' Γ Λ))
          match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
            M q'
              (Tape.head
                (match (motive := TM0.Stmt Γ → Tape Γ) s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T)) with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
Tactic: revert e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
⊢ TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
have move : ∀ (a : Dir),
  TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.move a) q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) TM0.Stmt.move a with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
move :
  ∀ (a : Dir),
    TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.move a) q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
      some
        { l := some (Λ'.normal q'), var := (),
          Tape :=
            match (motive := TM0.Stmt Γ → Tape Γ) TM0.Stmt.move a with
            | TM0.Stmt.move d => Tape.move d T
            | TM0.Stmt.write a => Tape.write a T }
⊢ TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
have write : ∀ (a : Γ),
  TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.write a) q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) TM0.Stmt.write a with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
⊢ ∀ (e : M q T.head = some (q', s)),
    Reaches₁ (TM1.step (tr M)) { l := some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
      {
        l :=
          match (motive := Bool → Option (Λ' Γ Λ))
            match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
              M q'
                (Tape.head
                  (match (motive := TM0.Stmt Γ → Tape Γ) s with
                  | TM0.Stmt.move d => Tape.move d T
                  | TM0.Stmt.write a => Tape.write a T)) with
            | some val => true
            | none => false with
          | true => some (Λ'.normal q')
          | false => none,
        var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
have this : TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
  some
    { l := some (Λ'.normal q'), var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
Tactic: have : TM1.step (tr M) ⟨some (Λ'.act s q'), (), T⟩ = some ⟨some (Λ'.normal q'), (), match s with
        | TM0.Stmt.move d => T.move d
        | TM0.Stmt.write a => T.write a⟩ := by
      cases s <;> rfl
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = some (q', s)
⊢ Reaches₁ (TM1.step (tr M)) { l := some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
    {
      l :=
        match (motive := Bool → Option (Λ' Γ Λ))
          match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
            M q'
              (Tape.head
                (match (motive := TM0.Stmt Γ → Tape Γ) s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T)) with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
have some : { l := some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } ∈
  TM1.step (tr M) { l := some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
Tactic: refine TransGen.head ?_ (TransGen.head' this ?_)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := Option.some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    Option.some
      { l := Option.some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = Option.some (q', s)
some :
  { l := Option.some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } ∈
    TM1.step (tr M) { l := Option.some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
⊢ Reaches₁ (TM1.step (tr M)) { l := Option.some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
    {
      l :=
        match (motive := Bool → Option (Λ' Γ Λ))
          match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
            M q'
              (Tape.head
                (match (motive := TM0.Stmt Γ → Tape Γ) s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T)) with
          | Option.some val => true
          | none => false with
        | true => Option.some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
have some₁ : ReflTransGen (fun (a b : TM1.Cfg Γ (Λ' Γ Λ) Unit) ↦ b ∈ TM1.step (tr M) a)
  { l := Option.some (Λ'.normal q'), var := (),
    Tape :=
      match (motive := TM0.Stmt Γ → Tape Γ) s with
      | TM0.Stmt.move d => Tape.move d T
      | TM0.Stmt.write a => Tape.write a T }
  {
    l :=
      match (motive := Bool → Option (Λ' Γ Λ))
        match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
          M q'
            (Tape.head
              (match (motive := TM0.Stmt Γ → Tape Γ) s with
              | TM0.Stmt.move d => Tape.move d T
              | TM0.Stmt.write a => Tape.write a T)) with
        | Option.some val => true
        | none => false with
      | true => Option.some (Λ'.normal q')
      | false => none,
    var := (),
    Tape :=
      match (motive := TM0.Stmt Γ → Tape Γ) s with
      | TM0.Stmt.move d => Tape.move d T
      | TM0.Stmt.write a => Tape.write a T }
Tactic: refine TransGen.head ?_ (TransGen.head' this ?_)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q : Stmt Γ Λ σ
⊢ q ∈ stmts₁ (Γ := Γ) q
have push : ∀ (k : K) (a : σ → Γ k) (a_1 : Stmt Γ Λ σ), push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (push (Γ := Γ) k a a_1)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q : Stmt Γ Λ σ
push :
  ∀ (k : K) (a : σ → Γ k) (a_1 : Stmt Γ Λ σ), Stmt.push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a a_1)
⊢ q ∈ stmts₁ (Γ := Γ) q
have peek : ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ), peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (peek (Γ := Γ) k a a_1)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q : Stmt Γ Λ σ
push :
  ∀ (k : K) (a : σ → Γ k) (a_1 : Stmt Γ Λ σ), Stmt.push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a a_1)
peek :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ),
    Stmt.peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.peek (Γ := Γ) k a a_1)
⊢ q ∈ stmts₁ (Γ := Γ) q
have pop : ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ), pop (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (pop (Γ := Γ) k a a_1)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q : Stmt Γ Λ σ
push :
  ∀ (k : K) (a : σ → Γ k) (a_1 : Stmt Γ Λ σ), Stmt.push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a a_1)
peek :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ),
    Stmt.peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.peek (Γ := Γ) k a a_1)
pop :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ),
    Stmt.pop (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.pop (Γ := Γ) k 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.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q : Stmt Γ Λ σ
push :
  ∀ (k : K) (a : σ → Γ k) (a_1 : Stmt Γ Λ σ), Stmt.push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a a_1)
peek :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ),
    Stmt.peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.peek (Γ := Γ) k a a_1)
pop :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ),
    Stmt.pop (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.pop (Γ := Γ) k 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.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q : Stmt Γ Λ σ
push :
  ∀ (k : K) (a : σ → Γ k) (a_1 : Stmt Γ Λ σ), Stmt.push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a a_1)
peek :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ),
    Stmt.peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.peek (Γ := Γ) k a a_1)
pop :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ),
    Stmt.pop (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.pop (Γ := Γ) k 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 : σ → Λ), Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (goto (Γ := Γ) a)) (goto (Γ := Γ) a)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q : Stmt Γ Λ σ
push :
  ∀ (k : K) (a : σ → Γ k) (a_1 : Stmt Γ Λ σ), Stmt.push (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.push (Γ := Γ) k a a_1)
peek :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ),
    Stmt.peek (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.peek (Γ := Γ) k a a_1)
pop :
  ∀ (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Stmt Γ Λ σ),
    Stmt.pop (Γ := Γ) k a a_1 ∈ stmts₁ (Γ := Γ) (Stmt.pop (Γ := Γ) k 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 : σ → Λ),
    Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (Stmt.goto (Γ := Γ) a)) (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.StackTuringMachine (hypothesis)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁_1
f : σ → 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 (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
⊢ q₀ ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
have h₁₃ : q₁_1 = branch (Γ := Γ) f q₁ q₂ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₁ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₂
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁_1
f : σ → 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 (Γ := Γ) f q₁ q₂ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₁ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₂
⊢ q₀ ∈ insert (branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
have branch : ∀ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (branch (Γ := Γ) f q₁ q₂))
  (IH₁ : ∀ (h₁₂ : branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁)
  (IH₂ : ∀ (h₁₂ : branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂),
  q₀ ∈ insert (branch (Γ := Γ) f 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.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁_1
f : σ → 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 (Γ := Γ) f q₁ q₂ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₁ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₂
branch :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁ q₂))
    (IH₁ : ∀ (h₁₂ : Stmt.branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁)
    (IH₂ : ∀ (h₁₂ : Stmt.branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂),
    q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
⊢ q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
have branch₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₁),
  q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
Tactic: rcases h₁₂ with (rfl | h₁₂ | h₁₂)
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁_1
f : σ → 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 (Γ := Γ) f q₁ q₂ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₁ ∨ q₁_1 ∈ stmts₁ (Γ := Γ) q₂
branch :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (Stmt.branch (Γ := Γ) f q₁ q₂))
    (IH₁ : ∀ (h₁₂ : Stmt.branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₁), q₀ ∈ stmts₁ (Γ := Γ) q₁)
    (IH₂ : ∀ (h₁₂ : Stmt.branch (Γ := Γ) f q₁ q₂ ∈ stmts₁ (Γ := Γ) q₂), q₀ ∈ stmts₁ (Γ := Γ) q₂),
    q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
branch₁ :
  ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₁),
    q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
⊢ q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
have branch₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ (Γ := Γ) q₂),
  q₀ ∈ insert (Stmt.branch (Γ := Γ) f q₁ q₂) (stmts₁ (Γ := Γ) q₁ ∪ stmts₁ (Γ := Γ) q₂)
Tactic: rcases h₁₂ with (rfl | h₁₂ | h₁₂)
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (hypothesis)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
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_singleton, Finset.mem_union] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (hypothesis)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
l : σ → Λ
h₁₂ : q₁ = goto (Γ := Γ) l
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {goto (Γ := Γ) l} q₀
have h₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ (Γ := Γ) (goto (Γ := Γ) l)) q₀
Tactic: subst h₁₂
Cleared hypotheses: q₁, h₀₁, h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (hypothesis)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
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_singleton, Finset.mem_union] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (hypothesis)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
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.StackTuringMachine (hypothesis)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
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_singleton, Finset.mem_union] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
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.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
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.StackTuringMachine (hypothesis)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
k : K
a : σ → Γ k
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
⊢ q₀ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
have h₁₃ : q₁ = push (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) q₁
k : K
a : σ → Γ k
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q
h₁₂ : q₁ = push (Γ := Γ) k a q ∨ q₁ ∈ stmts₁ (Γ := Γ) q
⊢ q₀ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
have push : ∀ (h₀₁ : q₀ ∈ stmts₁ (Γ := Γ) (push (Γ := Γ) k a q))
  (IH : ∀ (h₁₂ : push (Γ := Γ) k a q ∈ stmts₁ (Γ := Γ) q), q₀ ∈ stmts₁ (Γ := Γ) q),
  q₀ ∈ insert (push (Γ := Γ) k a q) (stmts₁ (Γ := Γ) q)
Tactic: rcases h₁₂ with (rfl | h₁₂)
Cleared hypotheses: q₁, h₀₁, IH, h₁₂