awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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₁ : Λ
a : Γ → σ → σ
a_1 : TM1.Stmt Γ Λ σ
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 Γ
⊢ TM0.step (tr M) { q := (some (TM1.Stmt.load a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) } =
    TM0.step (tr M) { q := (some a_1, a T.head v), Tape := T }

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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₁ : Λ
a : Γ → σ → σ
a_1 : TM1.Stmt Γ Λ σ
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.load a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (TM1.Stmt.load a a_1) v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux (TM1.Stmt.load a a_1) v T).var),
      Tape := (TM1.stepAux (TM1.Stmt.load a a_1) v T).Tape }

Tactic:
exact (reaches₁_eq (by rfl)).2 (IH _ _)

Premises used: Iff.mpr, StateTransition.reaches₁_eq
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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 :
  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 }
⊢ 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 Γ Λ σ)) (TM1.stepAux (TM1.Stmt.branch p a a_1) v T).l with
          | Option.some x => Option.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 }

Tactic:
unfold TM1.stepAux

Premises used: Turing.TM1.stepAux
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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 }
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 }
⊢ 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 }

Tactic:
cases e : p T.1 v

Premises used: Turing.Tape.head
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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
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)))
⊢ 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 }

Tactic:
simp only [TM0.step, tr, trAux, e]

Premises used: Turing.TM0.step, Turing.TM1to0.tr, Turing.TM1to0.trAux
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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
⊢ 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:
rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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
⊢ 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:
exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₂ _ _)

Premises used: Iff.mpr, StateTransition.reaches₁_eq
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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
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)))
⊢ 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 }

Tactic:
simp only [TM0.step, tr, trAux, e]

Premises used: Turing.TM0.step, Turing.TM1to0.tr, Turing.TM1to0.trAux
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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
⊢ 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:
rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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
⊢ 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 true then TM1.stepAux a v T else TM1.stepAux a_1 v T).l with
          | some x => 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:
exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₁ _ _)

Premises used: Iff.mpr, StateTransition.reaches₁_eq
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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₁ : Λ
a : Γ → σ → Λ
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.goto a), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (TM1.Stmt.goto a) v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux (TM1.Stmt.goto a) v T).var),
      Tape := (TM1.stepAux (TM1.Stmt.goto a) v T).Tape }

Tactic:
TransGen.single (congr_arg some (congr (congr_arg TM0.Cfg.mk rfl) (Tape.write_self T)))

Premises used: Option.some, Turing.Tape.write_self, congr_arg, Relation.TransGen.single, StateTransition.Reaches₁, congr, rfl, Turing.TM0.Cfg.mk
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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₁ : Λ
a : Γ → σ → Λ
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.goto a), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (TM1.Stmt.goto a) v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux (TM1.Stmt.goto a) v T).var),
      Tape := (TM1.stepAux (TM1.Stmt.goto a) v T).Tape }

Tactic:
exact TransGen.single (congr_arg some (congr (congr_arg TM0.Cfg.mk rfl) (Tape.write_self T)))

Premises used: Option.some, Turing.Tape.write_self, congr_arg, Relation.TransGen.single, congr, rfl, Turing.TM0.Cfg.mk
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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₁ : Λ
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some TM1.Stmt.halt, v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) TM1.Cfg.l (TM1.stepAux TM1.Stmt.halt v T) with
          | some x => some (M x)
          | none => none,
          TM1.Cfg.var.{u_1, u_2, u_3} (Λ := Λ) (TM1.stepAux TM1.Stmt.halt v T)),
      Tape := TM1.Cfg.Tape.{u_1, u_2, u_3} (Λ := Λ) (TM1.stepAux TM1.Stmt.halt v T) }

Tactic:
TransGen.single (congr_arg some (congr (congr_arg TM0.Cfg.mk rfl) (Tape.write_self T)))

Premises used: Option.some, Turing.Tape.write_self, congr_arg, Relation.TransGen.single, StateTransition.Reaches₁, congr, rfl, Turing.TM0.Cfg.mk
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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₁ : Λ
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some TM1.Stmt.halt, v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) TM1.Cfg.l (TM1.stepAux TM1.Stmt.halt v T) with
          | some x => some (M x)
          | none => none,
          TM1.Cfg.var.{u_1, u_2, u_3} (Λ := Λ) (TM1.stepAux TM1.Stmt.halt v T)),
      Tape := TM1.Cfg.Tape.{u_1, u_2, u_3} (Λ := Λ) (TM1.stepAux TM1.Stmt.halt v T) }

Tactic:
exact TransGen.single (congr_arg some (congr (congr_arg TM0.Cfg.mk rfl) (Tape.write_self T)))

Premises used: Option.some, Turing.Tape.write_self, congr_arg, Relation.TransGen.single, congr, rfl, Turing.TM0.Cfg.mk
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
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₁ : Λ
some :
  ∀ (x : TM1.Stmt Γ Λ σ),
    Reaches₁ (TM0.step (tr M)) { q := (Option.some x, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux x v T).l with
            | Option.some x => Option.some (M x)
            | none => none,
            (TM1.stepAux x v T).var),
        Tape := (TM1.stepAux x v T).Tape }
⊢ Reaches₁ (TM0.step (tr M)) { q := (Option.some (M l₁), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (M l₁) v T).l with
          | Option.some x => Option.some (M x)
          | none => none,
          (TM1.stepAux (M l₁) v T).var),
      Tape := (TM1.stepAux (M l₁) 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)))

Premises used: Option.some, Turing.Tape.write_self, Turing.TM1.stepAux, congr_arg, Relation.TransGen.single, Turing.TM0.Stmt.move, congr, rfl, Turing.TM0.Stmt.write, Turing.TM0.Cfg.mk
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
l : List Γ
rw :
  Eq.{u_1 + 1} (α := Part (ListBlank Γ))
    (Part.map (α := TM1.Cfg Γ Λ σ) ((fun (c : TM0.Cfg Γ (Λ' M)) ↦ c.Tape.right₀) ∘ trCfg M)
      (eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }))
    (Part.map (fun (c : TM1.Cfg Γ Λ σ) ↦ c.Tape.right₀) (eval (TM1.step M) (TM1.init l)))
⊢ Eq (α := Part (ListBlank Γ))
    (Part.map (fun (c : TM0.Cfg Γ (Λ' M)) ↦ c.Tape.right₀)
      (trCfg M <$> eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }))
    (TM1.eval M l)

Tactic:
rw [Part.map_eq_map, Part.map_map, TM1.eval]

Premises used: Turing.TM1.eval, Part.map_eq_map, Part.map_map
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
l : List Γ
⊢ Eq.{u_1 + 1} (α := Part (ListBlank Γ))
    (Part.map (α := TM1.Cfg Γ Λ σ) ((fun (c : TM0.Cfg Γ (Λ' M)) ↦ c.Tape.right₀) ∘ trCfg M)
      (eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }))
    (Part.map (fun (c : TM1.Cfg Γ Λ σ) ↦ c.Tape.right₀) (eval (TM1.step M) (TM1.init l)))

Tactic:
congr with ⟨⟩