mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v (((Tape.move d)^[i] ∘ Tape.move d) T)

Tactic:
]

Goal state after:
case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v (((Tape.move d)^[i] ∘ Tape.move d) T)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux q v ((Tape.move d)^[i] (Tape.move d T)) = stepAux q v ((Tape.move d)^[i] (Tape.move d T))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit1.bit1
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit true n)) = Nat.bit (g true true) ↑(p m n)

Tactic:
]

Goal state after:
case pos.pos.bit1.bit1
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit true n)) = Nat.bit (g true true) ↑(p m n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit1.bit1
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(bit (g true true) (p m n)) = ↑(bit (g true true) (p m n))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit1.bit0
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit false n)) = Nat.bit (g true false) ↑(p m n)

Tactic:
]

Goal state after:
case pos.pos.bit1.bit0
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit true m) (PosNum.bit false n)) = Nat.bit (g true false) ↑(p m n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit1.bit0
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(bit (g true false) (p m n)) = ↑(bit (g true false) (p m n))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit0.bit1
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit true n)) = Nat.bit (g false true) ↑(p m n)

Tactic:
]

Goal state after:
case pos.pos.bit0.bit1
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit true n)) = Nat.bit (g false true) ↑(p m n)
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
]

Goal state after:
case neg.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ (P.deriv a).rmatch t = true

Tactic:
]

Goal state after:
case neg.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ (P.deriv a).rmatch t = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
⊢ (Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons a L) R) =
    trTape' enc0 (ListBlank.cons a L).tail (ListBlank.cons (ListBlank.cons a L).head R)

Tactic:
simp only [trTape', ListBlank.cons_flatMap, ListBlank.head_cons, ListBlank.tail_cons]

Goal state after:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
⊢ (Tape.move Dir.left)^[n]
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯))
        (R.flatMap (fun x ↦ (enc x).toList) ⋯)) =
    Tape.mk' (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯)
      (ListBlank.append (enc a).toList (R.flatMap (fun x ↦ (enc x).toList) ⋯))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit0.bit1
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(bit (g false true) (p m n)) = ↑(bit (g false true) (p m n))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit0.bit0
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit false n)) = Nat.bit (g false false) ↑(p m n)

Tactic:
]

Goal state after:
case pos.pos.bit0.bit0
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit false n)) = Nat.bit (g false false) ↑(p m n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit0.bit0
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
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(bit (g false false) (p m n)) = ↑(bit (g false false) (p m n))

Tactic:
]

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

Goal state before:
pp: case succ
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
L✝ : Tape Bool
i : ℕ
IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L✝) = L✝
⊢ L✝ = L✝

Tactic:
]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mp.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true) →
    ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
]

Goal state after:
case mp.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true) →
    ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
l : σ → Λ
hs : ∀ (v : σ), l v ∈ S
⊢ SupportsStmt S (goto l)

Tactic:
exact hs

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : P.star.rmatch u = true
⊢ u.length < t.length + u.length + 1

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : P.star.rmatch u = true
⊢ u.length < t.length + u.length + 1
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case load.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
a✝¹ : σ → σ
a✝ : Stmt Γ Λ σ
hs : SupportsStmt S a✝
IH : load a✝¹ a✝ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S (load a✝¹ a✝)
⊢ SupportsStmt S (load a✝¹ a✝)

Tactic:
exact hs

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

Goal state before:
pp: case push.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k✝ : K
a✝¹ : σ → Γ k✝
a✝ : Stmt Γ Λ σ
hs : SupportsStmt S a✝
IH : push k✝ a✝¹ a✝ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S (push k✝ a✝¹ a✝)
⊢ SupportsStmt S (push k✝ a✝¹ a✝)

Tactic:
exact hs

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

Goal state before:
pp: case peek.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
hs : SupportsStmt S a✝
IH : peek k✝ a✝¹ a✝ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S (peek k✝ a✝¹ a✝)
⊢ SupportsStmt S (peek k✝ a✝¹ a✝)

Tactic:
exact hs

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mp.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : ∃ S, u = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
hwf : u.length < (a :: x).length
⊢ ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
]

Goal state after:
case mp.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : ∃ S, u = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
hwf : u.length < (a :: x).length
⊢ ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case pop.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
hs : SupportsStmt S a✝
IH : pop k✝ a✝¹ a✝ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S (pop k✝ a✝¹ a✝)
⊢ SupportsStmt S (pop k✝ a✝¹ a✝)

Tactic:
exact hs

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

Goal state before:
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 : l₂'.length = l₂.length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append (a :: l₁) L') (ListBlank.append l₂' R'))

Tactic:
]

Goal state after:
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 : l₂'.length = l₂.length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append (a :: l₁) L') (ListBlank.append l₂' R'))
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
t' : List α
ht' : t' ∈ (a :: t) :: S'
⊢ t' ≠ [] ∧ P.rmatch t' = true

Tactic:
cases ht' with

Goal state after: