awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
cons₁ :
  Eq (α := List ℕ → Part Cfg) (fun (v_1 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_1)) fun (x : List ℕ) ↦ do
    let a ← k.eval (v.headI :: x)
    pure (Cfg.halt a)
⊢ Eq (α := Part Cfg)
    (do
      let v_1 ← fs.eval as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1))
    do
    let x ← fs.eval as
    let a ← k.eval (v.headI :: x)
    pure (Cfg.halt a)

Tactic:
congr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
cons₁ :
  ∀ (v' : List ℕ),
    eval step (Cfg.ret (Cont.cons₂ v k) v') = do
      let a ← k.eval (v.headI :: v')
      pure (Cfg.halt a)
⊢ Eq (α := List ℕ → Part Cfg) (fun (v_1 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_1)) fun (x : List ℕ) ↦ do
    let a ← k.eval (v.headI :: x)
    pure (Cfg.halt a)

Tactic:
funext v'
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
cons₁ :
  eval step (stepRet (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
cons₂ : Reaches step (Cfg.ret (Cont.cons₂ v k) v') (stepRet (Cont.cons₂ v k) v')
rw : Cfg
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

Tactic:
rw [reaches_eval]

Premises used: StateTransition.reaches_eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₂ v k) v') (stepRet (Cont.cons₂ v k) v')

Tactic:
ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl, StateTransition.Reaches
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₂ v k) v') (stepRet (Cont.cons₂ v k) v')

Tactic:
exact ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
cons₁ :
  eval step (stepRet k (v.headI :: v')) = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
cons₂ :
  Cfg.halt <$> k.eval (v.headI :: v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
cons₃ cons₄ : Cfg.halt <$> k.eval (v.headI :: v') = Cfg.halt <$> k.eval (v.headI :: v')
⊢ eval step (stepRet (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

Tactic:
rw [stepRet, IH, bind_pure_comp]

Premises used: LawfulMonad.bind_pure_comp, Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
cons₂ : eval step (stepRet k (ns.headI :: v)) = Cfg.halt <$> (fun (v : List ℕ) ↦ k.eval (ns.headI :: v)) v
⊢ eval step (stepRet (Cont.cons₂ ns k) v) = Cfg.halt <$> (Cont.cons₂ ns k).eval v

Tactic:
rw [Cont.eval, stepRet]

Premises used: Turing.ToPartrec.Cont.eval, Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet k (ns.headI :: v)) = Cfg.halt <$> (fun (v : List ℕ) ↦ k.eval (ns.headI :: v)) v

Tactic:
IH
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet k (ns.headI :: v)) = Cfg.halt <$> (fun (v : List ℕ) ↦ k.eval (ns.headI :: v)) v

Tactic:
exact IH
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
comp :
  (do
      let v ← f.eval v
      eval step (Cfg.ret k v)) =
    Cfg.halt <$> (fun (v : List ℕ) ↦ f.eval v >>= k.eval) v
⊢ eval step (stepRet (Cont.comp f k) v) = Cfg.halt <$> (Cont.comp f k).eval v

Tactic:
rw [Cont.eval, stepRet, code_is_ok]

Premises used: Turing.ToPartrec.Cont.eval, Turing.ToPartrec.code_is_ok, Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
comp :
  Eq (α := Part Cfg)
    (do
      let v ← f.eval v
      eval step (Cfg.ret k v))
    do
    let x ← f.eval v
    let a ← k.eval x
    pure (Cfg.halt a)
⊢ (do
      let v ← f.eval v
      eval step (Cfg.ret k v)) =
    Cfg.halt <$> (fun (v : List ℕ) ↦ f.eval v >>= k.eval) v

Tactic:
simp only [← bind_pure_comp, bind_assoc]

Premises used: LawfulMonad.bind_assoc, LawfulMonad.bind_pure_comp
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
comp :
  Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret k v)) fun (x : List ℕ) ↦ do
    let a ← k.eval x
    pure (Cfg.halt a)
⊢ Eq (α := Part Cfg)
    (do
      let v ← f.eval v
      eval step (Cfg.ret k v))
    do
    let x ← f.eval v
    let a ← k.eval x
    pure (Cfg.halt a)

Tactic:
congr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
comp :
  ∀ (v' : List ℕ),
    eval step (Cfg.ret k v') = do
      let a ← k.eval v'
      pure (Cfg.halt a)
⊢ Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret k v)) fun (x : List ℕ) ↦ do
    let a ← k.eval x
    pure (Cfg.halt a)

Tactic:
funext v'
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
comp :
  eval step (stepRet k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)
comp₁ : Reaches step (Cfg.ret k v') (stepRet k v')
rw : Cfg
⊢ eval step (Cfg.ret k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)

Tactic:
rw [reaches_eval]

Premises used: StateTransition.reaches_eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret k v') (stepRet k v')

Tactic:
ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl, StateTransition.Reaches
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret k v') (stepRet k v')

Tactic:
exact ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
comp :
  Cfg.halt <$> k.eval v' = do
    let a ← k.eval v'
    pure (Cfg.halt a)
comp₁ comp₂ : Cfg.halt <$> k.eval v' = Cfg.halt <$> k.eval v'
⊢ eval step (stepRet k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)

Tactic:
rw [IH, bind_pure_comp]

Premises used: LawfulMonad.bind_pure_comp
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
pos : v.headI = 0 → eval step (stepRet k v.tail) = Cfg.halt <$> k.eval v.tail
neg : ¬v.headI = 0 → eval step (stepNormal f (Cont.fix f k) v.tail) = Cfg.halt <$> (f.fix.eval v.tail >>= k.eval)
⊢ eval step (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) =
    Cfg.halt <$> if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval

Tactic:
split_ifs
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : v.headI = 0
⊢ eval step (stepRet k v.tail) = Cfg.halt <$> k.eval v.tail

Tactic:
IH
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : v.headI = 0
⊢ eval step (stepRet k v.tail) = Cfg.halt <$> k.eval v.tail

Tactic:
exact IH
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : ¬v.headI = 0
neg :
  Eq (α := Part Cfg)
    (do
      let v ← f.fix.eval v.tail
      eval step (Cfg.ret k v))
    do
    let x ← f.fix.eval v.tail
    let a ← k.eval x
    pure (Cfg.halt a)
⊢ eval step (stepNormal f (Cont.fix f k) v.tail) = Cfg.halt <$> (f.fix.eval v.tail >>= k.eval)

Tactic:
simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]

Premises used: LawfulMonad.bind_assoc, LawfulMonad.bind_pure_comp, Turing.ToPartrec.cont_eval_fix, Turing.ToPartrec.code_is_ok
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : ¬v.headI = 0
neg :
  Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret k v)) fun (x : List ℕ) ↦ do
    let a ← k.eval x
    pure (Cfg.halt a)
⊢ Eq (α := Part Cfg)
    (do
      let v ← f.fix.eval v.tail
      eval step (Cfg.ret k v))
    do
    let x ← f.fix.eval v.tail
    let a ← k.eval x
    pure (Cfg.halt a)

Tactic:
congr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : ¬v.headI = 0
neg :
  ∀ (x : List ℕ),
    eval step (Cfg.ret k x) = do
      let a ← k.eval x
      pure (Cfg.halt a)
⊢ Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret k v)) fun (x : List ℕ) ↦ do
    let a ← k.eval x
    pure (Cfg.halt a)

Tactic:
funext
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : ¬v.headI = 0
x : List ℕ
neg : eval step (Cfg.ret k x) = eval step (stepRet k x)
⊢ eval step (Cfg.ret k x) = do
    let a ← k.eval x
    pure (Cfg.halt a)

Tactic:
rw [bind_pure_comp, ← IH]

Premises used: LawfulMonad.bind_pure_comp
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : ¬v.headI = 0
x : List ℕ
⊢ eval step (Cfg.ret k x) = eval step (stepRet k x)

Tactic:
reaches_eval (ReflTransGen.single rfl)

Premises used: StateTransition.reaches_eval, Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : ¬v.headI = 0
x : List ℕ
⊢ eval step (Cfg.ret k x) = eval step (stepRet k x)

Tactic:
exact reaches_eval (ReflTransGen.single rfl)

Premises used: StateTransition.reaches_eval, Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k : Cont
v : List ℕ
halt : ∀ {v : List ℕ}, eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.halt.eval v
cons₁ :
  ∀ (fs : Code) (as : List ℕ) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v)
    {v : List ℕ}, eval step (stepRet (Cont.cons₁ fs as k) v) = Cfg.halt <$> (Cont.cons₁ fs as k).eval v
cons₂ :
  ∀ (ns : List ℕ) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v) {v : List ℕ},
    eval step (stepRet (Cont.cons₂ ns k) v) = Cfg.halt <$> (Cont.cons₂ ns k).eval v
comp :
  ∀ (f : Code) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v) {v : List ℕ},
    eval step (stepRet (Cont.comp f k) v) = Cfg.halt <$> (Cont.comp f k).eval v
fix :
  ∀ (f : Code) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v) {v : List ℕ},
    eval step (stepRet (Cont.fix f k) v) = Cfg.halt <$> (Cont.fix f k).eval v
⊢ eval step (stepRet k v) = Cfg.halt <$> k.eval v

Tactic:
induction k generalizing v with
  | halt =>
    simp only [Cont.eval, map_pure]
    exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
  | cons₁ fs as k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IH, bind_pure_comp]
  | cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH
  | comp f k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [IH, bind_pure_comp]
  | fix f k IH =>
    rw [Cont.eval, stepRet]; simp only
    split_ifs; · exact IH
    simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
    congr; funext; rw [bind_pure_comp, ← IH]
    exact reaches_eval (ReflTransGen.single rfl)

Premises used: Iff.mpr, Turing.ToPartrec.Cont.eval, LawfulMonad.bind_assoc, Part.eq_some_iff, LawfulMonad.bind_pure_comp, Relation.ReflTransGen.refl, StateTransition.reaches_eval, Turing.ToPartrec.cont_eval_fix, Relation.ReflTransGen.single, StateTransition.mem_eval, And.intro, LawfulApplicative.map_pure, Turing.ToPartrec.code_is_ok, Turing.ToPartrec.stepRet, rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
c' : Cfg Γ Λ
h₁ : c' ∈ step M { q := q, Tape := T : Cfg Γ Λ }
h₂ : { q := q, Tape := T : Cfg Γ Λ }.q ∈ S
rcases :
  ∀ (q' : Λ) (a : Stmt Γ) (h : M q T.head = some (q', a))
    (h₁ :
      Membership.mem (α := Cfg Γ Λ) (step M { q := q, Tape := T : Cfg Γ Λ })
        (match (motive := Prod.{u_2, u_1} Λ (Stmt Γ) → Cfg Γ Λ) (q', a) with
          | (q', a) =>
            { q := q',
              Tape :=
                match (motive := Stmt Γ → Tape Γ) a with
                | Stmt.move d => Tape.move d T
                | Stmt.write a => Tape.write a T } :
          Cfg Γ Λ)),
    Cfg.q.{u_1, u_2} (Γ := Γ)
        (match (motive := Prod.{u_2, u_1} Λ (Stmt Γ) → Cfg Γ Λ) (q', a) with
        | (q', a) =>
          { q := q',
            Tape :=
              match (motive := Stmt Γ → Tape Γ) a with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T }) ∈
      S
⊢ c'.q ∈ S

Tactic:
rcases Option.map_eq_some_iff.1 h₁ with ⟨⟨q', a⟩, h, rfl⟩

Premises used: Iff.mp, rfl, Option.map_eq_some_iff
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
h₂ : { q := q, Tape := T : Cfg Γ Λ }.q ∈ S
q' : Λ
a : Stmt Γ
h : M q T.head = some (q', a)
h₁ :
  Membership.mem (α := Cfg Γ Λ) (step M { q := q, Tape := T : Cfg Γ Λ })
    (match (motive := Prod.{u_2, u_1} Λ (Stmt Γ) → Cfg Γ Λ) (q', a) with
      | (q', a) =>
        { q := q',
          Tape :=
            match (motive := Stmt Γ → Tape Γ) a with
            | Stmt.move d => Tape.move d T
            | Stmt.write a => Tape.write a T } :
      Cfg Γ Λ)
⊢ Cfg.q.{u_1, u_2} (Γ := Γ)
      (match (motive := Prod.{u_2, u_1} Λ (Stmt Γ) → Cfg Γ Λ) (q', a) with
      | (q', a) =>
        { q := q',
          Tape :=
            match (motive := Stmt Γ → Tape Γ) a with
            | Stmt.move d => Tape.move d T
            | Stmt.write a => Tape.write a T }) ∈
    S

Tactic:
ss.2 h h₂

Premises used: And.right
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
h₂ : { q := q, Tape := T : Cfg Γ Λ }.q ∈ S
q' : Λ
a : Stmt Γ
h : M q T.head = some (q', a)
h₁ :
  Membership.mem (α := Cfg Γ Λ) (step M { q := q, Tape := T : Cfg Γ Λ })
    (match (motive := Prod.{u_2, u_1} Λ (Stmt Γ) → Cfg Γ Λ) (q', a) with
      | (q', a) =>
        { q := q',
          Tape :=
            match (motive := Stmt Γ → Tape Γ) a with
            | Stmt.move d => Tape.move d T
            | Stmt.write a => Tape.write a T } :
      Cfg Γ Λ)
⊢ Cfg.q.{u_1, u_2} (Γ := Γ)
      (match (motive := Prod.{u_2, u_1} Λ (Stmt Γ) → Cfg Γ Λ) (q', a) with
      | (q', a) =>
        { q := q',
          Tape :=
            match (motive := Stmt Γ → Tape Γ) a with
            | Stmt.move d => Tape.move d T
            | Stmt.write a => Tape.write a T }) ∈
    S

Tactic:
exact ss.2 h h₂

Premises used: And.right
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
M : Machine Γ Λ
left : Membership.mem (γ := Set Λ) Set.univ default
right :
  ∀ {q : Λ} {a : Γ} {q' : Λ} {s : Stmt Γ},
    (q', s) ∈ M q a → Membership.mem (γ := Set Λ) Set.univ q → Membership.mem (γ := Set Λ) Set.univ q'
⊢ Supports M Set.univ

Tactic:
constructor
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
M : Machine Γ Λ
⊢ Membership.mem (γ := Set Λ) Set.univ default

Tactic:
apply Set.mem_univ

Premises used: Set.mem_univ
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
M : Machine Γ Λ
q : Λ
a : Γ
q' : Λ
s : Stmt Γ
h : (q', s) ∈ M q a
h_1 : Membership.mem (γ := Set Λ) Set.univ q
⊢ Membership.mem (γ := Set Λ) Set.univ q'

Tactic:
apply Set.mem_univ

Premises used: Set.mem_univ
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Γ' : Type u_2
inst_1 : Inhabited Γ'
Λ : Type u_3
inst_2 : Inhabited Λ
Λ' : Type u_4
inst_3 : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T : Cfg Γ Λ }.q ∈ S
simp :
  Eq (α := Option (Cfg Γ' Λ'))
    (Option.map (fun (x : Cfg Γ Λ) ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun (x : Prod.{u_3, u_1} Λ (Stmt Γ)) ↦
          { q := x.1,
            Tape :=
              match (motive := Stmt Γ → Tape Γ) x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        (M q T.head)))
    (Option.map
      (fun (x : Prod.{u_4, u_2} Λ' (Stmt Γ')) ↦
        { q := x.1,
          Tape :=
            match (motive := Stmt Γ' → Tape Γ') x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) (M q T.head)))
⊢ Eq (α := Option (Cfg Γ' Λ'))
    (Option.map
      (fun (x : Cfg Γ Λ) ↦
        match (motive := Cfg Γ Λ → Cfg Γ' Λ') x with
        | { q := q, Tape := T } => { q := g₁ q, Tape := Tape.map f₁ T })
      (match (motive := Cfg Γ Λ → Option (Cfg Γ Λ)) { q := q, Tape := T : Cfg Γ Λ } with
      | { q := q, Tape := T } =>
        Option.map
          (fun (x : Prod.{u_3, u_1} Λ (Stmt Γ)) ↦
            match (motive := Prod.{u_3, u_1} Λ (Stmt Γ) → Cfg Γ Λ) x with
            | (q', a) =>
              { q := q',
                Tape :=
                  match (motive := Stmt Γ → Tape Γ) a with
                  | Stmt.move d => Tape.move d T
                  | Stmt.write a => Tape.write a T })
          (M q T.head)))
    (match (motive := Cfg Γ' Λ' → Option (Cfg Γ' Λ'))
      match (motive := Cfg Γ Λ → Cfg Γ' Λ') { q := q, Tape := T : Cfg Γ Λ } with
      | { q := q, Tape := T } => { q := g₁ q, Tape := Tape.map f₁ T } with
    | { q := q, Tape := T } =>
      Option.map
        (fun (x : Prod.{u_4, u_2} Λ' (Stmt Γ')) ↦
          match (motive := Prod.{u_4, u_2} Λ' (Stmt Γ') → Cfg Γ' Λ') x with
          | (q', a) =>
            { q := q',
              Tape :=
                match (motive := Stmt Γ' → Tape Γ') a with
                | Stmt.move d => Tape.move d T
                | Stmt.write a => Tape.write a T })
        (match (motive := Λ' → Γ' → Option (Prod.{u_4, u_2} Λ' (Stmt Γ'))) q, T.head with
        | q, l => Option.map (Prod.map g₁ (Stmt.map f₁)) (M (g₂ q) (f₂.f l))))

Tactic:
simp only [Turing.Tape.map_fst, g₂₁ q h, f₂₁ _]

Premises used: Turing.Tape.map_fst
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Γ' : Type u_2
inst_1 : Inhabited Γ'
Λ : Type u_3
inst_2 : Inhabited Λ
Λ' : Type u_4
inst_3 : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T : Cfg Γ Λ }.q ∈ S
⊢ Eq (α := Option (Cfg Γ' Λ'))
    (Option.map (fun (x : Cfg Γ Λ) ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun (x : Prod.{u_3, u_1} Λ (Stmt Γ)) ↦
          { q := x.1,
            Tape :=
              match (motive := Stmt Γ → Tape Γ) x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        none))
    (Option.map
      (fun (x : Prod.{u_4, u_2} Λ' (Stmt Γ')) ↦
        { q := x.1,
          Tape :=
            match (motive := Stmt Γ' → Tape Γ') x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) none))

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Γ' : Type u_2
inst_1 : Inhabited Γ'
Λ : Type u_3
inst_2 : Inhabited Λ
Λ' : Type u_4
inst_3 : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T : Cfg Γ Λ }.q ∈ S
q' : Λ
d : Dir
some :
  Option.some { q := g₁ q', Tape := Tape.move d (Tape.map f₁ T) : Cfg Γ' Λ' } =
    Option.some
      { q := (Prod.map g₁ (Stmt.map f₁) (q', Stmt.move d)).1,
        Tape :=
          match (motive := Stmt Γ' → Tape Γ') (Prod.map g₁ (Stmt.map f₁) (q', Stmt.move d)).2 with
          | Stmt.move d => Tape.move d (Tape.map f₁ T)
          | Stmt.write a => Tape.write a (Tape.map f₁ T) }
⊢ Eq (α := Option (Cfg Γ' Λ'))
    (Option.map (fun (x : Cfg Γ Λ) ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun (x : Prod.{u_3, u_1} Λ (Stmt Γ)) ↦
          { q := x.1,
            Tape :=
              match (motive := Stmt Γ → Tape Γ) x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        (Option.some (q', Stmt.move d))))
    (Option.map
      (fun (x : Prod.{u_4, u_2} Λ' (Stmt Γ')) ↦
        { q := x.1,
          Tape :=
            match (motive := Stmt Γ' → Tape Γ') x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) (Option.some (q', Stmt.move d))))

Tactic:
simp only [Option.map_some, Tape.map_move f₁]

Premises used: Option.map_some, Turing.Tape.map_move
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Γ' : Type u_2
inst_1 : Inhabited Γ'
Λ : Type u_3
inst_2 : Inhabited Λ
Λ' : Type u_4
inst_3 : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T : Cfg Γ Λ }.q ∈ S
q' : Λ
d : Dir
⊢ some { q := g₁ q', Tape := Tape.move d (Tape.map f₁ T) : Cfg Γ' Λ' } =
    some
      { q := (Prod.map g₁ (Stmt.map f₁) (q', Stmt.move d)).1,
        Tape :=
          match (motive := Stmt Γ' → Tape Γ') (Prod.map g₁ (Stmt.map f₁) (q', Stmt.move d)).2 with
          | Stmt.move d => Tape.move d (Tape.map f₁ T)
          | Stmt.write a => Tape.write a (Tape.map f₁ T) }

Tactic:
rfl