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

Goal state before:
pp: case gff
⊢ (false || false) = false

pp: case f00
⊢ 0 ||| 0 = 0

pp: case f0n
⊢ ∀ (n : PosNum), 0 ||| pos n = bif false || true then pos n else 0

pp: case fn0
⊢ ∀ (n : PosNum), pos n ||| 0 = bif true || false then pos n else 0

pp: case fnn
⊢ ∀ (m n : PosNum), pos m ||| pos n = pos (m.lor n)

pp: case p11
⊢ pos (lor 1 1) = bif true || true then 1 else 0

pp: case p1b
⊢ ∀ (b : Bool) (n : PosNum), pos (lor 1 (PosNum.bit b n)) = bit (true || b) (bif false || true then pos n else 0)

pp: case pb1
⊢ ∀ (a : Bool) (m : PosNum), pos ((PosNum.bit a m).lor 1) = bit (a || true) (bif true || false then pos m else 0)

pp: case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), pos ((PosNum.bit a m).lor (PosNum.bit b n)) = bit (a || b) (pos (m.lor n))

Tactic:
<;>

Goal state after:
case gff
⊢ (false || false) = false

case f00
⊢ 0 ||| 0 = 0

case f0n
⊢ ∀ (n : PosNum), 0 ||| pos n = bif false || true then pos n else 0

case fn0
⊢ ∀ (n : PosNum), pos n ||| 0 = bif true || false then pos n else 0

case fnn
⊢ ∀ (m n : PosNum), pos m ||| pos n = pos (m.lor n)

case p11
⊢ pos (lor 1 1) = bif true || true then 1 else 0

case p1b
⊢ ∀ (b : Bool) (n : PosNum), pos (lor 1 (PosNum.bit b n)) = bit (true || b) (bif false || true then pos n else 0)

case pb1
⊢ ∀ (a : Bool) (m : PosNum), pos ((PosNum.bit a m).lor 1) = bit (a || true) (bif true || false then pos m else 0)

case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), pos ((PosNum.bit a m).lor (PosNum.bit b n)) = bit (a || b) (pos (m.lor n))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case cons.nil
Γ : 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 : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (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')
l₁ : List Bool
e : [].length = (a :: l₂).length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

pp: case cons.cons
Γ : 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 : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (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')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : (b :: l₂').length = (a :: l₂).length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
<;>

Goal state after:
case cons.nil
Γ : 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 : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (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')
l₁ : List Bool
e : [].length = (a :: l₂).length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

case cons.cons
Γ : 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 : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (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')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : (b :: l₂').length = (a :: l₂).length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case none
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ (Option.map some none).getD default = none

pp: case some
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
val✝ : Γ k
⊢ (Option.map some (some val✝)).getD default = some val✝

Tactic:
<;>

Goal state after:
case none
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ (Option.map some none).getD default = none

case some
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
val✝ : Γ k
⊢ (Option.map some (some val✝)).getD default = some val✝
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case zero
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) 0 (addBottom L) = addBottom (ListBlank.modifyNth f 0 L)

pp: case succ
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) (n✝ + 1) (addBottom L) = addBottom (ListBlank.modifyNth f (n✝ + 1) L)

Tactic:
<;>

Goal state after:
case zero
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) 0 (addBottom L) = addBottom (ListBlank.modifyNth f 0 L)

case succ
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) (n✝ + 1) (addBottom L) = addBottom (ListBlank.modifyNth f (n✝ + 1) L)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Γ k
⊢ TM2.SupportsStmt S (stRun (push a✝) q) ↔ TM2.SupportsStmt S q

pp: case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ TM2.SupportsStmt S (stRun (peek a✝) q) ↔ TM2.SupportsStmt S q

pp: case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ TM2.SupportsStmt S (stRun (pop a✝) q) ↔ TM2.SupportsStmt S q

Tactic:
<;>

Goal state after:
case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Γ k
⊢ TM2.SupportsStmt S (stRun (push a✝) q) ↔ TM2.SupportsStmt S q

case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ TM2.SupportsStmt S (stRun (peek a✝) q) ↔ TM2.SupportsStmt S q

case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ TM2.SupportsStmt S (stRun (pop a✝) q) ↔ TM2.SupportsStmt S q
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Γ k
⊢ trNormal (stRun (StAct.push a✝) q) = goto fun x x_1 ↦ go k (StAct.push a✝) q

pp: case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trNormal (stRun (StAct.peek a✝) q) = goto fun x x_1 ↦ go k (StAct.peek a✝) q

pp: case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trNormal (stRun (StAct.pop a✝) q) = goto fun x x_1 ↦ go k (StAct.pop a✝) q

Tactic:
<;>

Goal state after:
case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Γ k
⊢ trNormal (stRun (StAct.push a✝) q) = goto fun x x_1 ↦ go k (StAct.push a✝) q

case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trNormal (stRun (StAct.peek a✝) q) = goto fun x x_1 ↦ go k (StAct.peek a✝) q

case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trNormal (stRun (StAct.pop a✝) q) = goto fun x x_1 ↦ go k (StAct.pop a✝) q
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Γ k
⊢ trStmts₁ (stRun (StAct.push a✝) q) = {go k (StAct.push a✝) q, ret q} ∪ trStmts₁ q

pp: case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trStmts₁ (stRun (StAct.peek a✝) q) = {go k (StAct.peek a✝) q, ret q} ∪ trStmts₁ q

pp: case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trStmts₁ (stRun (StAct.pop a✝) q) = {go k (StAct.pop a✝) q, ret q} ∪ trStmts₁ q

Tactic:
<;>

Goal state after:
case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Γ k
⊢ trStmts₁ (stRun (StAct.push a✝) q) = {go k (StAct.push a✝) q, ret q} ∪ trStmts₁ q

case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trStmts₁ (stRun (StAct.peek a✝) q) = {go k (StAct.peek a✝) q, ret q} ∪ trStmts₁ q

case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trStmts₁ (stRun (StAct.pop a✝) q) = {go k (StAct.pop a✝) q, ret q} ∪ trStmts₁ q
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gff
⊢ (false && false) = false

pp: case f00
⊢ 0 &&& 0 = 0

pp: case f0n
⊢ ∀ (n : PosNum), 0 &&& pos n = bif false && true then pos n else 0

pp: case fn0
⊢ ∀ (n : PosNum), pos n &&& 0 = bif true && false then pos n else 0

pp: case fnn
⊢ ∀ (m n : PosNum), pos m &&& pos n = m.land n

pp: case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

pp: case p1b
⊢ ∀ (b : Bool) (n : PosNum), PosNum.land 1 (PosNum.bit b n) = bit (true && b) (bif false && true then pos n else 0)

pp: case pb1
⊢ ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).land 1 = bit (a && true) (bif true && false then pos m else 0)

pp: case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)

Tactic:
<;>

Goal state after:
case gff
⊢ (false && false) = false

case f00
⊢ 0 &&& 0 = 0

case f0n
⊢ ∀ (n : PosNum), 0 &&& pos n = bif false && true then pos n else 0

case fn0
⊢ ∀ (n : PosNum), pos n &&& 0 = bif true && false then pos n else 0

case fnn
⊢ ∀ (m n : PosNum), pos m &&& pos n = m.land n

case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

case p1b
⊢ ∀ (b : Bool) (n : PosNum), PosNum.land 1 (PosNum.bit b n) = bit (true && b) (bif false && true then pos n else 0)

case pb1
⊢ ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).land 1 = bit (a && true) (bif true && false then pos m else 0)

case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gff
⊢ (false && false) = false

pp: case f00
⊢ 0 &&& 0 = 0

pp: case f0n
n✝ : PosNum
⊢ 0 &&& pos n✝ = bif false && true then pos n✝ else 0

pp: case fn0
n✝ : PosNum
⊢ pos n✝ &&& 0 = bif true && false then pos n✝ else 0

pp: case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝

pp: case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

pp: case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit b✝ n✝) = bit (true && b✝) (bif false && true then pos n✝ else 0)

pp: case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land 1 = bit (a✝ && true) (bif true && false then pos m✝ else 0)

pp: case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land (PosNum.bit b✝ n✝) = bit (a✝ && b✝) (m✝.land n✝)

Tactic:
<;>

Goal state after:
case gff
⊢ (false && false) = false

case f00
⊢ 0 &&& 0 = 0

case f0n
n✝ : PosNum
⊢ 0 &&& pos n✝ = bif false && true then pos n✝ else 0

case fn0
n✝ : PosNum
⊢ pos n✝ &&& 0 = bif true && false then pos n✝ else 0

case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝

case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit b✝ n✝) = bit (true && b✝) (bif false && true then pos n✝ else 0)

case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land 1 = bit (a✝ && true) (bif true && false then pos m✝ else 0)

case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land (PosNum.bit b✝ n✝) = bit (a✝ && b✝) (m✝.land n✝)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.move.left
Γ : 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 Γ Λ σ
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 Dir.left q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.left q) v (Tape.mk' L R)))

pp: case some.move.right
Γ : 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 Γ Λ σ
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 Dir.right q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.right q) v (Tape.mk' L R)))

Tactic:
<;>

Goal state after:
case some.move.left
Γ : 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 Γ Λ σ
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 Dir.left q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.left q) v (Tape.mk' L R)))

case some.move.right
Γ : 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 Γ Λ σ
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 Dir.right q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.right q) v (Tape.mk' L R)))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case zero
v : List ℕ
⊢ Nat.rec (Part.some [0]) (fun y x ↦ Part.some [y]) 0 = Part.some [0 - 1]

pp: case succ
v : List ℕ
n✝ : ℕ
⊢ Nat.rec (Part.some [0]) (fun y x ↦ Part.some [y]) (n✝ + 1) = Part.some [n✝ + 1 - 1]

Tactic:
<;>

Goal state after:
case zero
v : List ℕ
⊢ Nat.rec (Part.some [0]) (fun y x ↦ Part.some [y]) 0 = Part.some [0 - 1]

case succ
v : List ℕ
n✝ : ℕ
⊢ Nat.rec (Part.some [0]) (fun y x ↦ Part.some [y]) (n✝ + 1) = Part.some [n✝ + 1 - 1]
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.move.left
Γ : 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 Γ Λ σ
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 q) v (trTape' enc0 L.tail (ListBlank.cons L.head R)))
    (trCfg enc enc0 (stepAux q v (Tape.mk' L.tail (ListBlank.cons L.head R))))

pp: case some.move.right
Γ : 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 Γ Λ σ
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 q) v (trTape' enc0 (ListBlank.cons R.head L) R.tail))
    (trCfg enc enc0 (stepAux q v (Tape.move Dir.right (Tape.mk' L R))))

Tactic:
<;>

Goal state after:
case some.move.left
Γ : 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 Γ Λ σ
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 q) v (trTape' enc0 L.tail (ListBlank.cons L.head R)))
    (trCfg enc enc0 (stepAux q v (Tape.mk' L.tail (ListBlank.cons L.head R))))

case some.move.right
Γ : 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 Γ Λ σ
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 q) v (trTape' enc0 (ListBlank.cons R.head L) R.tail))
    (trCfg enc enc0 (stepAux q v (Tape.move Dir.right (Tape.mk' L R))))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gff
⊢ (false && false) = false

pp: case f00
⊢ 0 &&& 0 = 0

pp: case f0n
n✝ : PosNum
⊢ 0 &&& pos n✝ = bif false && true then pos n✝ else 0

pp: case fn0
n✝ : PosNum
⊢ pos n✝ &&& 0 = bif true && false then pos n✝ else 0

pp: case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝

pp: case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

pp: case p1b.false
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit false n✝) = bit (true && false) (bif false && true then pos n✝ else 0)

pp: case p1b.true
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit true n✝) = bit (true && true) (bif false && true then pos n✝ else 0)

pp: case pb1.false
m✝ : PosNum
⊢ (PosNum.bit false m✝).land 1 = bit (false && true) (bif true && false then pos m✝ else 0)

pp: case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).land 1 = bit (true && true) (bif true && false then pos m✝ else 0)

pp: case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit false n✝) = bit (false && false) (m✝.land n✝)

pp: case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit true n✝) = bit (false && true) (m✝.land n✝)

pp: case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit false n✝) = bit (true && false) (m✝.land n✝)

pp: case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit true n✝) = bit (true && true) (m✝.land n✝)

Tactic:
<;>

Goal state after:
case gff
⊢ (false && false) = false

case f00
⊢ 0 &&& 0 = 0

case f0n
n✝ : PosNum
⊢ 0 &&& pos n✝ = bif false && true then pos n✝ else 0

case fn0
n✝ : PosNum
⊢ pos n✝ &&& 0 = bif true && false then pos n✝ else 0

case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝

case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

case p1b.false
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit false n✝) = bit (true && false) (bif false && true then pos n✝ else 0)

case p1b.true
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit true n✝) = bit (true && true) (bif false && true then pos n✝ else 0)

case pb1.false
m✝ : PosNum
⊢ (PosNum.bit false m✝).land 1 = bit (false && true) (bif true && false then pos m✝ else 0)

case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).land 1 = bit (true && true) (bif true && false then pos m✝ else 0)

case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit false n✝) = bit (false && false) (m✝.land n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit true n✝) = bit (false && true) (m✝.land n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit false n✝) = bit (true && false) (m✝.land n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit true n✝) = bit (true && true) (m✝.land n✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gff
⊢ (false && !false) = false

pp: case f00
⊢ ldiff 0 0 = 0

pp: case f0n
⊢ ∀ (n : PosNum), ldiff 0 (pos n) = bif false && !true then pos n else 0

pp: case fn0
⊢ ∀ (n : PosNum), (pos n).ldiff 0 = bif true && !false then pos n else 0

pp: case fnn
⊢ ∀ (m n : PosNum), (pos m).ldiff (pos n) = m.ldiff n

pp: case p11
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0

pp: case p1b
⊢ ∀ (b : Bool) (n : PosNum), PosNum.ldiff 1 (PosNum.bit b n) = bit (true && !b) (bif false && !true then pos n else 0)

pp: case pb1
⊢ ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).ldiff 1 = bit (a && !true) (bif true && !false then pos m else 0)

pp: case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)

Tactic:
<;>

Goal state after:
case gff
⊢ (false && !false) = false

case f00
⊢ ldiff 0 0 = 0

case f0n
⊢ ∀ (n : PosNum), ldiff 0 (pos n) = bif false && !true then pos n else 0

case fn0
⊢ ∀ (n : PosNum), (pos n).ldiff 0 = bif true && !false then pos n else 0

case fnn
⊢ ∀ (m n : PosNum), (pos m).ldiff (pos n) = m.ldiff n

case p11
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0

case p1b
⊢ ∀ (b : Bool) (n : PosNum), PosNum.ldiff 1 (PosNum.bit b n) = bit (true && !b) (bif false && !true then pos n else 0)

case pb1
⊢ ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).ldiff 1 = bit (a && !true) (bif true && !false then pos m else 0)

case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)