awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' : Λ
a : Γ
some :
  Option.some { q := g₁ q', Tape := Tape.write (f₁.f a) (Tape.map f₁ T) : Cfg Γ' Λ' } =
    Option.some
      { q := (Prod.map g₁ (Stmt.map f₁) (q', Stmt.write a)).1,
        Tape :=
          match (motive := Stmt Γ' → Tape Γ') (Prod.map g₁ (Stmt.map f₁) (q', Stmt.write a)).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.write a))))
    (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.write a))))

Tactic:
simp only [Option.map_some, Tape.map_write]

Premises used: Option.map_some, Turing.Tape.map_write
-- 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' : Λ
a : Γ
⊢ some { q := g₁ q', Tape := Tape.write (f₁.f a) (Tape.map f₁ T) : Cfg Γ' Λ' } =
    some
      { q := (Prod.map g₁ (Stmt.map f₁) (q', Stmt.write a)).1,
        Tape :=
          match (motive := Stmt Γ' → Tape Γ') (Prod.map g₁ (Stmt.map f₁) (q', Stmt.write a)).2 with
          | Stmt.move d => Tape.move d (Tape.map f₁ T)
          | Stmt.write a => Tape.write a (Tape.map f₁ T) }

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 Λ'
f₁ : PointedMap Γ Γ'
g₁ : PointedMap Λ Λ'
l : List Γ
⊢ Cfg.map f₁ g₁.f (init l) = init (List.map f₁.f l)

Tactic:
congr (congr_arg Cfg.mk g₁.map_pt) (Tape.map_mk₁ _ _)

Premises used: Turing.TM0.Cfg.map, congr_arg, Turing.TM0.init, Turing.Tape.map_mk₁, congr, Turing.TM0.Cfg.mk, Turing.PointedMap.map_pt
-- 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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
_ :
  ∀ ⦃a₂ : Cfg Γ' Λ'⦄,
    (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) c a₂ →
      match (motive := Option (Cfg Γ Λ) → Prop) step M c with
      | some b₁ =>
        ∃ (b₂ : Cfg Γ' Λ'),
          (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
            Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) a₂ b₂
      | none => step (M.map f₁ f₂ g₁.f g₂) a₂ = none
⊢ ∀ ⦃a₂ : Cfg Γ' Λ'⦄,
    (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) c a₂ →
      match (motive := Option (Cfg Γ Λ) → Prop) step M c with
      | some b₁ =>
        ∃ (b₂ : Cfg Γ' Λ'),
          (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
            Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) a₂ b₂
      | none => step (M.map f₁ f₂ g₁.f g₂) a₂ = none

Tactic:
_
-- 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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
this :
  ∀ (cs : c.q ∈ S),
    match (motive := Option (Cfg Γ Λ) → Prop) step M c with
    | some b₁ =>
      ∃ (b₂ : Cfg Γ' Λ'),
        (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
          Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
    | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none
⊢ (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) c a₂ →
    match (motive := Option (Cfg Γ Λ) → Prop) step M c with
    | some b₁ =>
      ∃ (b₂ : Cfg Γ' Λ'),
        (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
          Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) a₂ b₂
    | none => step (M.map f₁ f₂ g₁.f g₂) a₂ = none

Tactic:
⟨cs, 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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
none :
  ∀ (e : step M c = Option.none),
    match (motive := Option (Cfg Γ Λ) → Prop) Option.none with
    | Option.some b₁ =>
      ∃ (b₂ : Cfg Γ' Λ'),
        (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
          Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
    | Option.none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = Option.none
some :
  ∀ (val : Cfg Γ Λ) (e : step M c = Option.some val),
    match (motive := Option (Cfg Γ Λ) → Prop) Option.some val with
    | Option.some b₁ =>
      ∃ (b₂ : Cfg Γ' Λ'),
        (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
          Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
    | Option.none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = Option.none
⊢ match (motive := Option (Cfg Γ Λ) → Prop) step M c with
  | Option.some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | Option.none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = Option.none

Tactic:
cases e : step M c

Premises used: Turing.TM0.step
-- 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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
e : step M c = Option.none
none :
  match (motive := Option (Cfg Γ Λ) → Prop) Option.none with
  | some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | Option.none => Option.map (Cfg.map f₁ g₁.f) Option.none = Option.none
⊢ match (motive := Option (Cfg Γ Λ) → Prop) Option.none with
  | some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | Option.none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = Option.none

Tactic:
rw [← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs, e]

Premises used: Turing.TM0.Machine.map_step, Turing.PointedMap.f
-- 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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
e : step M c = none
⊢ match (motive := Option (Cfg Γ Λ) → Prop) none with
  | some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => Option.map (Cfg.map f₁ g₁.f) none = 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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
val : Cfg Γ Λ
e : step M c = some val
⊢ match (motive := Option (Cfg Γ Λ) → Prop) some val with
  | some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none

Tactic:
⟨_, ⟨step_supports M ss e cs, rfl⟩, TransGen.single ?_⟩

Premises used: Turing.TM0.step_supports, Relation.TransGen.single, And.intro, Exists.intro, 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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
val : Cfg Γ Λ
e : step M c = Option.some val
some : Cfg.map f₁ g₁.f val ∈ step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c)
⊢ match (motive := Option (Cfg Γ Λ) → Prop) Option.some val with
  | Option.some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none

Tactic:
refine ⟨_, ⟨step_supports M ss e cs, rfl⟩, TransGen.single ?_⟩
-- 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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
val : Cfg Γ Λ
e : step M c = Option.some val
some : Cfg.map f₁ g₁.f val ∈ Option.map (Cfg.map f₁ g₁.f) (Option.some val)
⊢ Cfg.map f₁ g₁.f val ∈ step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c)

Tactic:
rw [← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs, e]

Premises used: Turing.TM0.Machine.map_step, Turing.PointedMap.f
-- 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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
val : Cfg Γ Λ
e : step M c = some val
⊢ Cfg.map f₁ g₁.f val ∈ Option.map (Cfg.map f₁ g₁.f) (some val)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q : Stmt Γ Λ σ
move : ∀ (a : Dir) (a_1 : Stmt Γ Λ σ), Stmt.move a a_1 ∈ stmts₁ (Stmt.move a a_1)
write : ∀ (a : Γ → σ → Γ) (a_1 : Stmt Γ Λ σ), Stmt.write a a_1 ∈ stmts₁ (Stmt.write 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 : Γ → σ → Λ), Stmt.goto a ∈ stmts₁ (Stmt.goto a)
halt : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ Stmt.halt) Stmt.halt
⊢ q ∈ stmts₁ q

Tactic:
cases q
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a : Dir
a_1 : Stmt Γ Λ σ
⊢ move a a_1 ∈ stmts₁ (move a a_1)

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM1.stmts₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a : Γ → σ → Γ
a_1 : Stmt Γ Λ σ
⊢ write a a_1 ∈ stmts₁ (write a a_1)

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM1.stmts₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a : Γ → σ → σ
a_1 : Stmt Γ Λ σ
⊢ load a a_1 ∈ stmts₁ (load a a_1)

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM1.stmts₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a : Γ → σ → Bool
a_1 a_2 : Stmt Γ Λ σ
⊢ branch a a_1 a_2 ∈ stmts₁ (branch a a_1 a_2)

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM1.stmts₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a : Γ → σ → Λ
⊢ goto a ∈ stmts₁ (goto a)

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM1.stmts₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ halt) halt

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

Premises used: Finset.mem_singleton_self, Finset.mem_insert_self, Turing.TM1.stmts₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁_1
p : Γ → σ → 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 p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
⊢ q₁_1 = branch p q₁ q₂ ∨ q₁_1 ∈ stmts₁ q₁ ∨ q₁_1 ∈ stmts₁ q₂

Tactic:
simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂

Premises used: Finset.mem_singleton, Finset.mem_insert, Finset.mem_union
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁_1
p : Γ → σ → 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 p q₁ q₂ ∨ q₁_1 ∈ stmts₁ q₁ ∨ q₁_1 ∈ stmts₁ q₂
branch :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Stmt.branch p q₁ q₂)) (IH₁ : ∀ (h₁₂ : Stmt.branch p q₁ q₂ ∈ stmts₁ q₁), q₀ ∈ stmts₁ q₁)
    (IH₂ : ∀ (h₁₂ : Stmt.branch p q₁ q₂ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂),
    q₀ ∈ insert (Stmt.branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
branch₁ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₁), q₀ ∈ insert (Stmt.branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
branch₂ : ∀ (h₁₂ : q₁_1 ∈ stmts₁ q₂), q₀ ∈ insert (Stmt.branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
⊢ q₀ ∈ insert (Stmt.branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
rcases h₁₂ with (rfl | h₁₂ | h₁₂)

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (branch p q₁ q₂)
IH₁ : ∀ (h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₁), q₀ ∈ stmts₁ q₁
IH₂ : ∀ (h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
unfold stmts₁ at h₀₁

Premises used: Turing.TM1.stmts₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₁), q₀ ∈ stmts₁ q₁
IH₂ : ∀ (h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂
h₀₁ : q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
h₀₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : ∀ (h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₁), q₀ ∈ stmts₁ q₁
IH₂ : ∀ (h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₂), q₀ ∈ stmts₁ q₂
h₀₁ : q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁_1
p : Γ → σ → 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 ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
grind
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁_1 q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁_1
p : Γ → σ → 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 ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
grind
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
l : Γ → σ → Λ
h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) {goto l} q₁
⊢ q₁ = goto l

Tactic:
simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂

Premises used: Finset.mem_singleton, Finset.mem_insert, Finset.mem_union
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
l : Γ → σ → Λ
h₁₂ : q₁ = goto l
⊢ q₀ ∈ stmts₁ (goto l)

Tactic:
subst h₁₂
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
l : Γ → σ → Λ
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {goto l} q₀

Tactic:
h₀₁

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
l : Γ → σ → Λ
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {goto l} q₀

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) {halt} q₁
⊢ q₁ = halt

Tactic:
simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂

Premises used: Finset.mem_singleton, Finset.mem_insert, Finset.mem_union
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ halt) q₀

Tactic:
subst h₁₂
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
h₀₁ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ halt) q₀
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {halt} q₀

Tactic:
h₀₁

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
h₀₁ : Membership.mem (γ := Finset (Stmt Γ Λ σ)) (stmts₁ halt) q₀
⊢ Membership.mem (γ := Finset (Stmt Γ Λ σ)) {halt} q₀

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ insert (move a q) (stmts₁ q)
⊢ q₁ = move a q ∨ q₁ ∈ stmts₁ q

Tactic:
simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂

Premises used: Finset.mem_singleton, Finset.mem_insert, Finset.mem_union
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ = Stmt.move a q ∨ q₁ ∈ stmts₁ q
move :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Stmt.move a q)) (IH : ∀ (h₁₂ : Stmt.move a q ∈ stmts₁ q), q₀ ∈ stmts₁ q),
    q₀ ∈ insert (Stmt.move a q) (stmts₁ q)
move₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ insert (Stmt.move a q) (stmts₁ q)
⊢ q₀ ∈ insert (Stmt.move a q) (stmts₁ q)

Tactic:
rcases h₁₂ with rfl | h₁₂

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (move a q)
IH : ∀ (h₁₂ : move a q ∈ stmts₁ q), q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (move a q) (stmts₁ q)

Tactic:
h₀₁

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
a : Dir
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (move a q)
IH : ∀ (h₁₂ : move a q ∈ stmts₁ q), q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (move a q) (stmts₁ q)

Tactic:
exact h₀₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Dir
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (move a q) (stmts₁ q)

Tactic:
grind
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ insert (write a q) (stmts₁ q)
⊢ q₁ = write a q ∨ q₁ ∈ stmts₁ q

Tactic:
simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂

Premises used: Finset.mem_singleton, Finset.mem_insert, Finset.mem_union
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ stmts₁ q
h₁₂ : q₁ = Stmt.write a q ∨ q₁ ∈ stmts₁ q
write :
  ∀ (h₀₁ : q₀ ∈ stmts₁ (Stmt.write a q)) (IH : ∀ (h₁₂ : Stmt.write a q ∈ stmts₁ q), q₀ ∈ stmts₁ q),
    q₀ ∈ insert (Stmt.write a q) (stmts₁ q)
write₁ : ∀ (h₁₂ : q₁ ∈ stmts₁ q), q₀ ∈ insert (Stmt.write a q) (stmts₁ q)
⊢ q₀ ∈ insert (Stmt.write a q) (stmts₁ q)

Tactic:
rcases h₁₂ with rfl | h₁₂

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (write a q)
IH : ∀ (h₁₂ : write a q ∈ stmts₁ q), q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (write a q) (stmts₁ q)

Tactic:
h₀₁

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (write a q)
IH : ∀ (h₁₂ : write a q ∈ stmts₁ q), q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (write a q) (stmts₁ q)

Tactic:
exact h₀₁