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₁ 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₁
load :
  ∀ (a : Γ → σ → σ) (q : Stmt Γ Λ σ) (IH : ∀ (h : q₁ ∈ stmts₁ q) (hs : SupportsStmt S q), SupportsStmt S q₁)
    (h : q₁ ∈ stmts₁ (Stmt.load a q)) (hs : SupportsStmt S (Stmt.load a q)), SupportsStmt S q₁
⊢ SupportsStmt S q₁
have load₁ : ∀ (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), 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
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
⊢ some q₂ ∈ stmts M S → some q₁ ∈ stmts M S
have simp : ∀ x ∈ S, q₂ ∈ stmts₁ (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (M a)
Tactic: simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
    forall_eq', exists_imp, and_imp]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
⊢ some q ∈ stmts M S → SupportsStmt S q
have simp : ∀ x ∈ S, q ∈ stmts₁ (M x) → SupportsStmt S q
Tactic: simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
    forall_eq', exists_imp, and_imp]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
c' : Cfg Γ Λ σ
h₁ : c' ∈ step M { l := some l₁, var := v, Tape := T : Cfg Γ Λ σ }
h₂ :
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    { l := some l₁, var := v, Tape := T : Cfg Γ Λ σ }.l
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) c'.l
have h₃ : SupportsStmt S (M l₁)
Tactic: replace h₂ := ss.2 _ (Finset.some_mem_insertNone.1 h₂)
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
c' : Cfg Γ Λ σ
h₁ : c' ∈ step M { l := some l₁, var := v, Tape := T : Cfg Γ Λ σ }
h₂ : SupportsStmt S (M l₁)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) c'.l
have h₃ : stepAux (M l₁) v T = c'
Tactic: simp only [step, Option.mem_def, Option.some.injEq] 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
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
c' : Cfg Γ Λ σ
h₂ : SupportsStmt S (M l₁)
h₁ : stepAux (M l₁) v T = c'
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) c'.l
have subst : Membership.mem (γ := Finset (Option Λ)) ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
  (stepAux (M l₁) v T).l
Tactic: subst c'
Cleared hypotheses: c', h₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
h₂ : SupportsStmt S (M l₁)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (M l₁) v T).l
have revert : ∀ (h₂ : SupportsStmt S (M l₁)),
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (M l₁) v T).l
Tactic: revert h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₁' v T).l
IH₂ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₂' v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (branch p q₁' q₂')
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    (bif p T.head v then stepAux q₁' v T else stepAux q₂' v T).l
have branch : Membership.mem (γ := Finset (Option Λ)) ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
  (bif false then stepAux q₁' v T else stepAux q₂' v T).l
Tactic: cases p T.1 v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₁' v T).l
IH₂ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₂' v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (Stmt.branch p q₁' q₂')
branch :
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    (bif false then stepAux q₁' v T else stepAux q₂' v T).l
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    (bif p T.head v then stepAux q₁' v T else stepAux q₂' v T).l
have branch₁ : Membership.mem (γ := Finset (Option Λ)) ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
  (bif true then stepAux q₁' v T else stepAux q₂' v T).l
Tactic: cases p T.1 v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
⊢ ∀ (h₂ : SupportsStmt S (M l₁)),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (M l₁) v T).l
have induction : ∀ (x : Stmt Γ Λ σ) (h₂ : SupportsStmt S x),
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux x v T).l
Tactic: induction M l₁ generalizing v T with intro hs
    | branch p q₁' q₂' IH₁ IH₂ =>
      unfold stepAux; cases p T.1 v
      · exact IH₂ _ _ hs.2
      · exact IH₁ _ _ hs.1
    | goto => exact Finset.some_mem_insertNone.2 (hs _ _)
    | halt => apply Multiset.mem_cons_self
    | _ _ q IH => exact IH _ _ hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Option Λ
v : σ
T : Tape Γ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
    (TM1.step M { l := l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
have none : FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := none, var := v, Tape := T : TM1.Cfg Γ Λ σ })
  (TM1.step M { l := none, var := v, Tape := T : TM1.Cfg Γ Λ σ })
Tactic: rcases l₁ with - | l₁
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Option Λ
v : σ
T : Tape Γ
none :
  FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := Option.none, var := v, Tape := T : TM1.Cfg Γ Λ σ })
    (TM1.step M { l := Option.none, var := v, Tape := T : TM1.Cfg Γ Λ σ })
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
    (TM1.step M { l := l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
have some : ∀ (l₁ : Λ),
  FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := some l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
    (TM1.step M { l := some l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
Tactic: rcases l₁ with - | l₁
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
v : σ
T : Tape Γ
l₁ : Λ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := some l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
    (TM1.step M { l := some l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
have some : Reaches₁ (TM0.step (tr M)) { q := (some (M l₁), v), Tape := T : TM0.Cfg Γ (Λ' M) }
  {
    q :=
      (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (M l₁) v T).l with
        | some x => some (M x)
        | none => none,
        (TM1.stepAux (M l₁) v T).var),
    Tape := (TM1.stepAux (M l₁) v T).Tape }
Tactic: simp only [trCfg, TM1.step, FRespects, Option.map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a a_1 : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a v T).var),
        Tape := (TM1.stepAux a v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a_1, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a_1 v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a_1 v T).var),
        Tape := (TM1.stepAux a_1 v T).Tape }
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.branch p a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (TM1.Stmt.branch p a a_1) v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux (TM1.Stmt.branch p a a_1) v T).var),
      Tape := (TM1.stepAux (TM1.Stmt.branch p a a_1) v T).Tape }
have some : Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.branch p a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
  {
    q :=
      (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ))
          (bif p T.head v then TM1.stepAux a v T else TM1.stepAux a_1 v T).l with
        | some x => some (M x)
        | none => none,
        (bif p T.head v then TM1.stepAux a v T else TM1.stepAux a_1 v T).var),
    Tape := (bif p T.head v then TM1.stepAux a v T else TM1.stepAux a_1 v T).Tape }
Tactic: unfold TM1.stepAux
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a a_1 : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a v T).var),
        Tape := (TM1.stepAux a v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a_1, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a_1 v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a_1 v T).var),
        Tape := (TM1.stepAux a_1 v T).Tape }
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.branch p a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ))
            (bif p T.head v then TM1.stepAux a v T else TM1.stepAux a_1 v T).l with
          | some x => some (M x)
          | none => none,
          (bif p T.head v then TM1.stepAux a v T else TM1.stepAux a_1 v T).var),
      Tape := (bif p T.head v then TM1.stepAux a v T else TM1.stepAux a_1 v T).Tape }
have some : ∀ (e : p T.head v = false),
  Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.branch p a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ))
            (bif false then TM1.stepAux a v T else TM1.stepAux a_1 v T).l with
          | some x => some (M x)
          | none => none,
          (bif false then TM1.stepAux a v T else TM1.stepAux a_1 v T).var),
      Tape := (bif false then TM1.stepAux a v T else TM1.stepAux a_1 v T).Tape }
Tactic: cases e : p T.1 v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a a_1 : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (Option.some a, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a v T).l with
            | Option.some x => Option.some (M x)
            | none => none,
            (TM1.stepAux a v T).var),
        Tape := (TM1.stepAux a v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (Option.some a_1, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a_1 v T).l with
            | Option.some x => Option.some (M x)
            | none => none,
            (TM1.stepAux a_1 v T).var),
        Tape := (TM1.stepAux a_1 v T).Tape }
v : σ
T : Tape Γ
some :
  ∀ (e : p T.head v = false),
    Reaches₁ (TM0.step (tr M)) { q := (Option.some (TM1.Stmt.branch p a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ))
              (bif false then TM1.stepAux a v T else TM1.stepAux a_1 v T).l with
            | Option.some x => Option.some (M x)
            | none => none,
            (bif false then TM1.stepAux a v T else TM1.stepAux a_1 v T).var),
        Tape := (bif false then TM1.stepAux a v T else TM1.stepAux a_1 v T).Tape }
⊢ Reaches₁ (TM0.step (tr M)) { q := (Option.some (TM1.Stmt.branch p a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ))
            (bif p T.head v then TM1.stepAux a v T else TM1.stepAux a_1 v T).l with
          | Option.some x => Option.some (M x)
          | none => none,
          (bif p T.head v then TM1.stepAux a v T else TM1.stepAux a_1 v T).var),
      Tape := (bif p T.head v then TM1.stepAux a v T else TM1.stepAux a_1 v T).Tape }
have some₁ : ∀ (e : p T.head v = true),
  Reaches₁ (TM0.step (tr M)) { q := (Option.some (TM1.Stmt.branch p a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ))
            (bif true then TM1.stepAux a v T else TM1.stepAux a_1 v T).l with
          | Option.some x => Option.some (M x)
          | none => none,
          (bif true then TM1.stepAux a v T else TM1.stepAux a_1 v T).var),
      Tape := (bif true then TM1.stepAux a v T else TM1.stepAux a_1 v T).Tape }
Tactic: cases e : p T.1 v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a a_1 : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a v T).var),
        Tape := (TM1.stepAux a v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a_1, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a_1 v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a_1 v T).var),
        Tape := (TM1.stepAux a_1 v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = false
⊢ TM0.step (tr M) { q := (some (TM1.Stmt.branch p a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) } =
    TM0.step (tr M) { q := (some a_1, v), Tape := T }
have simp : Eq (α := Option (TM0.Cfg Γ (Λ' M)))
  (Option.map
    (fun (x : Λ' M × TM0.Stmt Γ) ↦
      { q := x.1,
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) x.2 with
          | move d => Tape.move d T
          | write a => Tape.write a T })
    (some (bif false then trAux M T.head a v else trAux M T.head a_1 v)))
  (Option.map
    (fun (x : Λ' M × TM0.Stmt Γ) ↦
      { q := x.1,
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) x.2 with
          | move d => Tape.move d T
          | write a => Tape.write a T })
    (some (trAux M T.head a_1 v)))
Tactic: simp only [TM0.step, tr, trAux, e]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a a_1 : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a v T).var),
        Tape := (TM1.stepAux a v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a_1, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a_1 v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a_1 v T).var),
        Tape := (TM1.stepAux a_1 v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = true
⊢ TM0.step (tr M) { q := (some (TM1.Stmt.branch p a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) } =
    TM0.step (tr M) { q := (some a, v), Tape := T }
have simp : Eq (α := Option (TM0.Cfg Γ (Λ' M)))
  (Option.map
    (fun (x : Λ' M × TM0.Stmt Γ) ↦
      { q := x.1,
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) x.2 with
          | move d => Tape.move d T
          | write a => Tape.write a T })
    (some (bif true then trAux M T.head a v else trAux M T.head a_1 v)))
  (Option.map
    (fun (x : Λ' M × TM0.Stmt Γ) ↦
      { q := x.1,
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) x.2 with
          | move d => Tape.move d T
          | write a => Tape.write a T })
    (some (trAux M T.head a v)))
Tactic: simp only [TM0.step, tr, trAux, e]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
v : σ
T : Tape Γ
l₁ : Λ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (M l₁), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (M l₁) v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux (M l₁) v T).var),
      Tape := (TM1.stepAux (M l₁) v T).Tape }
have some : ∀ (x : TM1.Stmt Γ Λ σ),
  Reaches₁ (TM0.step (tr M)) { q := (some x, v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux x v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux x v T).var),
      Tape := (TM1.stepAux x v T).Tape }
Tactic: induction M l₁ generalizing v T with
    | move _ _ IH => exact TransGen.head rfl (IH _ _)
    | write _ _ IH => exact TransGen.head rfl (IH _ _)
    | load _ _ IH => exact (reaches₁_eq (by rfl)).2 (IH _ _)
    | branch p _ _ IH₁ IH₂ =>
      unfold TM1.stepAux; cases e : p T.1 v
      · exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₂ _ _)
      · exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₁ _ _)
    | _ =>
      exact TransGen.single (congr_arg some (congr (congr_arg TM0.Cfg.mk rfl) (Tape.write_self T)))