mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.one.one
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
⊢ ↑(p 1 1) = Nat.bit (g true true) 0

Tactic:
p11

Goal state after:
case pos.pos.one.one
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
⊢ ↑(bif g true true then 1 else 0) = Nat.bit (g true true) 0
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some.some.move
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
d : Dir
q : TM1.Stmt Γ Λ σ
a_ih✝ :
  ∀ (v : σ),
    some q ∈ TM1.stmts M S →
      some (trAux M a q v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.move d q) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.move d q) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.move d q)
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
cases h₁; refine TM1.stmts_trans ?_ h₂
      unfold TM1.stmts₁
      exact Finset.mem_insert_of_mem TM1.stmts₁_self

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some.some.write
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
b : Γ → σ → Γ
q : TM1.Stmt Γ Λ σ
a_ih✝ :
  ∀ (v : σ),
    some q ∈ TM1.stmts M S →
      some (trAux M a q v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.write b q) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.write b q) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.write b q)
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
cases h₁; refine TM1.stmts_trans ?_ h₂
      unfold TM1.stmts₁
      exact Finset.mem_insert_of_mem TM1.stmts₁_self

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
⊢ stepAux (write (enc a).toList q) v
      (Tape.mk' (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯)
        (ListBlank.append (enc b).toList (R.flatMap (fun x ↦ (enc x).toList) ⋯))) =
    stepAux q v
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯))
        (R.flatMap (fun x ↦ (enc x).toList) ⋯))

Tactic:
suffices ∀ {L' R'} (l₁ l₂ l₂' : List Bool) (_ : l₂'.length = l₂.length),
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
      stepAux q v (Tape.mk' (L'.append (List.reverseAux l₂ l₁)) R') by
    exact this [] _ _ ((enc b).2.trans (enc a).2.symm)

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
⊢ ∀ {L' R' : ListBlank Bool} (l₁ l₂ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
R S : RegularExpression α
⊢ (map f (R + S)).matches' = (Language.map f) (R + S).matches'

Tactic:
simp only [matches'_map, map, matches'_add, map_add]

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
d : Dir
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move d q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move d q) v (Tape.mk' L R)))

Tactic:
cases d <;>
          simp only [trNormal, stepAux_move, stepAux,
            Tape.move_left_mk',
            trTape'_move_left enc0, trTape'_move_right enc0] <;>
        apply IH

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case zero'
k' k : Cont
v : List ℕ
⊢ Cfg.ret (k.then k') (0 :: v) = (Cfg.ret k (0 :: v)).then k'

Tactic:
simp only [Cfg.then]

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case succ
k' k : Cont
v : List ℕ
⊢ Cfg.ret (k.then k') [v.headI.succ] = (Cfg.ret k [v.headI.succ]).then k'

Tactic:
simp only [Cfg.then]

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case tail
k' k : Cont
v : List ℕ
⊢ Cfg.ret (k.then k') v.tail = (Cfg.ret k v.tail).then k'

Tactic:
simp only [Cfg.then]

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case halt
k' : Cont
v : List ℕ
⊢ stepRet k' v = (Cfg.halt v).then k'

Tactic:
simp only [Cfg.then]

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
v'' : List ℕ
h₁ : v'' ∈ f.eval v
h₂ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v'')
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
reaches_eval

Goal state after:
case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
v'' : List ℕ
h₁ : v'' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v'')
h₂ : Cfg.halt v' ∈ eval step ?m.307
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)

case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
v'' : List ℕ
h₁ : v'' ∈ f.eval v
h₂ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v'')
⊢ Reaches step (Cfg.ret Cont.halt v'') ?m.307

f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
v'' : List ℕ
h₁ : v'' ∈ f.eval v
h₂ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v'')
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h : x ∈ eval step (stepRet k v'.tail)
⊢ x ∈ eval step (Cfg.ret k v'.tail)

Tactic:
reaches_eval

Goal state after:
case pos
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h : x ∈ eval step (stepRet k v'.tail)
⊢ x ∈ eval step ?m.426

case pos
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h : x ∈ eval step (stepRet k v'.tail)
⊢ Reaches step (Cfg.ret k v'.tail) ?m.426

f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h : x ∈ eval step (stepRet k v'.tail)
⊢ Cfg
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
h : IsTopologicalBasis {s | IsClopen s}
⊢ TotallySeparatedSpace X

Tactic:
by
  constructor
  rintro x - y - hxy
  choose U hU using exists_isOpen_xor_mem hxy
  obtain ⟨hU₀, hU₁⟩ := hU
  rcases hU₁ with hx | hy
  · choose V hV using h.isOpen_iff.mp hU₀ x hx.1
    exact ⟨V, Vᶜ, hV.1.isOpen, hV.1.compl.isOpen, hV.2.1, notMem_subset hV.2.2 hx.2,
      (union_compl_self V).superset, disjoint_compl_right⟩
  · choose V hV using h.isOpen_iff.mp hU₀ y hy.1
    exact ⟨Vᶜ, V, hV.1.compl.isOpen, hV.1.isOpen, notMem_subset hV.2.2 hy.2, hV.2.1,
      (union_comm _ _ ▸ union_compl_self V).superset, disjoint_compl_left⟩

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
VisClopen' : IsClopen (Subtype.val '' V)
⊢ ↑x ∈ Subtype.val '' V

Tactic:
simp [Vx]

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case mpr
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)

Tactic:
reaches_eval

Goal state after:
case mpr
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step ?m.617
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)

case mpr
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
⊢ Reaches step (Cfg.ret k v') ?m.617

f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he✝¹ : v'.tail ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he✝ : v'.tail ∈ f.fix.eval v
he : Sum.inl v'.tail ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
⊢ x ∈ eval step (Cfg.ret (Cont.fix f k) v')

Tactic:
reaches_eval

Goal state after:
case pos.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he✝¹ : v'.tail ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he✝ : v'.tail ∈ f.fix.eval v
he : Sum.inl v'.tail ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
⊢ x ∈ eval step ?m.779

case pos.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he✝¹ : v'.tail ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he✝ : v'.tail ∈ f.fix.eval v
he : Sum.inl v'.tail ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
⊢ Reaches step (Cfg.ret (Cont.fix f k) v') ?m.779

f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he✝¹ : v'.tail ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he✝ : v'.tail ∈ f.fix.eval v
he : Sum.inl v'.tail ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case neg.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he✝ : v' ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right✝ :
  v' ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) v₁.tail
⊢ x ∈ eval step (Cfg.ret (Cont.fix f k) v₁)

Tactic:
reaches_eval

Goal state after:
case neg.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he✝ : v' ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right✝ :
  v' ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) v₁.tail
⊢ x ∈ eval step ?m.887

case neg.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he✝ : v' ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right✝ :
  v' ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) v₁.tail
⊢ Reaches step (Cfg.ret (Cont.fix f k) v₁) ?m.887

f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he✝ : v' ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right✝ :
  v' ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) v₁.tail
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₁ fs v✝ k) v) = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

Tactic:
reaches_eval

Goal state after:
case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.61 = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v✝ k) v) ?m.61

f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step (Cfg.ret (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

Tactic:
reaches_eval

Goal state after:
case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.171 = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.comp f k) v) ?m.171

f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_2
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (a : σ → σ) (q : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt S q →
        (∀ x ∈ trStmts₁ q, x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q) ∧ ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l')) →
      TM2.SupportsStmt S (TM2.Stmt.load a q) →
        (∀ x ∈ trStmts₁ (TM2.Stmt.load a q), x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a q)) ∧
            ∀ l' ∈ trStmts₁ (TM2.Stmt.load a q), TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
intro _ _ IH ss' sub

Goal state after:
case refine_2
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
a✝ : σ → σ
q✝ : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt S q✝ →
    (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.load a✝ q✝)
sub : ∀ x ∈ trStmts₁ (TM2.Stmt.load a✝ q✝), x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a✝ q✝)) ∧
    ∀ l' ∈ trStmts₁ (TM2.Stmt.load a✝ q✝), TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case halt
v : List ℕ
⊢ eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.halt.eval v

Tactic:
simp only [Cont.eval, map_pure]

Goal state after:
case halt
v : List ℕ
⊢ eval step (stepRet Cont.halt v) = pure (Cfg.halt v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

Tactic:
reaches_eval

Goal state after:
case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step ?m.89 = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

case e_a
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') ?m.89

fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg