mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case bit.bit
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
        (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x y
yb : Bool
y : ℕ
hyb : bit yb y ≠ 0
a✝ :
  bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 ↦
        bit (f xb b)
          (binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
            (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x n))
      y
⊢ bitwise f (bit xb x) (bit yb y) =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 ↦
        bit (f xb b)
          (binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
            (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x n))
      (bit yb y)

Tactic:
[

Goal state after:
case bit.bit
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
        (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x y
yb : Bool
y : ℕ
hyb : bit yb y ≠ 0
a✝ :
  bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 ↦
        bit (f xb b)
          (binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
            (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x n))
      y
⊢ bitwise f (bit xb x) (bit yb y) =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 ↦
        bit (f xb b)
          (binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
            (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x n))
      (bit yb y)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
n m : ℕ
this : bitwise f = swap (bitwise f)
| bitwise f n m

Tactic:
this

Goal state after:
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
n m : ℕ
this : bitwise f = swap (bitwise f)
| swap (bitwise f) n m
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i ≠ true ∧ b.testBit i ≠ true ∧ c.testBit i ≠ true
⊢ v.testBit i ≠ true

Tactic:
[

Goal state after:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i ≠ true ∧ b.testBit i ≠ true ∧ c.testBit i ≠ true
⊢ v.testBit i ≠ true
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℕ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ f x ^ p

Tactic:
[

Goal state after:
f : ℝ → ℝ
p : ℕ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ f x ^ p
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℤ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ f x ^ p

Tactic:
[

Goal state after:
f : ℝ → ℝ
p : ℤ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ f x ^ p
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case h
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w✝ = replicate m none ++ some a :: replicate n none
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ (replicate n none).reduceOption = []

Tactic:
[

Goal state after:
case h
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w✝ = replicate m none ++ some a :: replicate n none
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ (replicate n none).reduceOption = []
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ a.bit0 = b.bit0

Tactic:
this

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ b.bit0 = b.bit0
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
⊢ x ∈ {x | ∃ s_1 ∈ M.accept, ∃ i, s_1 ∈ M.evalFrom (s i) x} ↔ x ∈ ⋃ i, {x | ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x}

Tactic:
[

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
⊢ x ∈ {x | ∃ s_1 ∈ M.accept, ∃ i, s_1 ∈ M.evalFrom (s i) x} ↔ x ∈ ⋃ i, {x | ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x}
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case nil
α : Type u_1
⊢ [].reduceOption.length = (filter Option.isSome []).length

Tactic:
[

Goal state after:
case nil
α : Type u_1
⊢ [].reduceOption.length = (filter Option.isSome []).length
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length = (filter Option.isSome l).length

Tactic:
induction l with
  | nil => simp_rw [reduceOption_nil, filter_nil, length]
  | cons hd tl hl => cases hd <;> simp [hl]

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.length = l.reduceOption.length + (filter Option.isNone l).length

Tactic:
[

Goal state after:
α : Type u_1
l : List (Option α)
⊢ l.length = l.reduceOption.length + (filter Option.isNone l).length
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ ↑a + ↑a < ↑b + ↑b + 1

Tactic:
this

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑b + ↑b + 1
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))

Tactic:
[

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
a : α
⊢ M.stepSet ∅ a = ∅

Tactic:
[

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
a : α
⊢ M.stepSet ∅ a = ∅
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l✝ : List α
a✝ : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l✝ ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l✝
s : σ
⊢ s ∈ M.evalFrom S (l✝ ++ [a✝]) ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} (l✝ ++ [a✝])

Tactic:
[

Goal state after:
case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l✝ : List α
a✝ : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l✝ ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l✝
s : σ
⊢ s ∈ M.evalFrom S (l✝ ++ [a✝]) ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} (l✝ ++ [a✝])
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑a + ↑a + 1

Tactic:
this

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑b + ↑b + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ a.bit1 = b.bit1

Tactic:
this

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ b.bit1 = b.bit1
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case succ
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate (n✝ + 1) none)
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
[

Goal state after:
case succ
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate (n✝ + 1) none)
⊢ s₂ ∈ M.εClosure {s₁}
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝¹ x✝ : Num
⊢ x✝¹ + x✝ = x✝ + x✝¹

Tactic:
[

Goal state after:
x✝¹ x✝ : Num
⊢ x✝¹ + x✝ = x✝ + x✝¹
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝² x✝¹ x✝ : Num
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
[

Goal state after:
x✝² x✝¹ x✝ : Num
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝¹ x✝ : Num
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
[

Goal state after:
x✝¹ x✝ : Num
⊢ x✝¹ * x✝ = x✝ * x✝¹
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ (∃ x', x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x') → ∃ n, M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
[

Goal state after:
case nil.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ (∃ x', x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x') → ∃ n, M.IsPath s₁ s₂ (List.replicate n none)
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton.mp
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
h : ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}
x' : List (Option α)
left✝ : x'.reduceOption = x
right✝ : M.IsPath s₁ t x'
⊢ ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
[

Goal state after:
case append_singleton.mp
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
h : ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}
x' : List (Option α)
left✝ : x'.reduceOption = x
right✝ : M.IsPath s₁ t x'
⊢ ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
⊢ (∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x') → ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))

Tactic:
[

Goal state after:
case append_singleton.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
⊢ (∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x') → ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left✝¹ : x'.reduceOption = x
n : ℕ
t : σ
left✝ : M.IsPath s₁ t x'
u : σ
a✝¹ : u ∈ M.step t (some a)
a✝ : M.IsPath u s₂ (List.replicate n none)
⊢ (∃ x', x'.reduceOption = x ∧ M.IsPath s₁ t x') ∧ ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}

Tactic:
[

Goal state after:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
x' : List (Option α)
left✝¹ : x'.reduceOption = x
n : ℕ
t : σ
left✝ : M.IsPath s₁ t x'
u : σ
a✝¹ : u ∈ M.step t (some a)
a✝ : M.IsPath u s₂ (List.replicate n none)
⊢ (∃ x', x'.reduceOption = x ∧ M.IsPath s₁ t x') ∧ ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start : Set σ
this : M.toεNFA.stepSet = M.stepSet
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start

Tactic:
this

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
this : M.toεNFA.stepSet = M.stepSet
⊢ List.foldl M.stepSet start = List.foldl M.stepSet start
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially f

Tactic:
this

Goal state after:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially (g + (f - g))
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
x✝ : Reaches₁ f b c
bc : Reaches₁ f b c := x✝
left✝ : Reaches f a b
b0 : f b = none
b' : σ
h' : b' ∈ f b
right✝ : ReflTransGen (fun a b ↦ b ∈ f a) b' c
⊢ False

Tactic:
cases b0.symm.trans h'

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
left✝ : Reaches f a b
b0 : f b = none
b' : σ
h' : b' ∈ f b
⊢ False

Tactic:
cases b0.symm.trans h'

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case succ
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' ↑Nat.succ

Tactic:
| succ =>

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case succ
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
⊢ Nat.Partrec ↑Nat.succ

Tactic:
| succ =>

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case succ
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
⊢ Nat.RecursiveIn O ↑Nat.succ

Tactic:
| succ =>

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
L R : ListBlank Γ
⊢ map f (mk' L R) = mk' (ListBlank.map f L) (ListBlank.map f R)

Tactic:
by
  simp only [Tape.mk', Tape.map, ListBlank.head_map,
    ListBlank.tail_map]

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

Goal state before:
pp: case none
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : 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 none with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ 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:
rw [← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs, e]

Goal state after:
case none
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : 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 none with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ 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
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : 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✝ ∈ 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]

Goal state after:
case some
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : 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✝)
Module: Mathlib.Computability.Reduce

Goal state before:
pp: case h.h
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ ≤ of p✝ → of p✝ ≤ of p✝¹ → of p✝¹ = of p✝

Tactic:
intro hp

Goal state after:
case h.h
p✝¹ p✝ : Set ℕ
hp : of p✝¹ ≤ of p✝
⊢ of p✝ ≤ of p✝¹ → of p✝¹ = of p✝
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : a = head✝
⊢ (deriv 1 head).rmatch tail = true ↔ head✝ = a ∧ head :: tail = []

Tactic:
[

Goal state after:
case cons.cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : a = head✝
⊢ (deriv 1 head).rmatch tail = true ↔ head✝ = a ∧ head :: tail = []
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : ¬a = head✝
⊢ (deriv 0 head).rmatch tail = true ↔ head✝ = a ∧ head :: tail = []

Tactic:
[

Goal state after:
case cons.cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : ¬a = head✝
⊢ (deriv 0 head).rmatch tail = true ↔ head✝ = a ∧ head :: tail = []
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f))
      (update S k
        (match StAct.peek f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => (S k).tail))

Tactic:
Function.update_eq_self

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S = TM2.stepAux q (stVar v (S k) (StAct.peek f)) S
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case plus
α : Type u_1
inst✝ : DecidableEq α
a✝¹ a✝ : RegularExpression α
ih₁ : ∀ (x : List α), a✝¹.rmatch x = true ↔ x ∈ a✝¹.matches'
ih₂ : ∀ (x : List α), a✝.rmatch x = true ↔ x ∈ a✝.matches'
x : List α
⊢ (a✝¹.plus a✝).rmatch x = true ↔ x ∈ (a✝¹.plus a✝).matches'

Tactic:
plus_def,

Goal state after:
case plus
α : Type u_1
inst✝ : DecidableEq α
a✝¹ a✝ : RegularExpression α
ih₁ : ∀ (x : List α), a✝¹.rmatch x = true ↔ x ∈ a✝¹.matches'
ih₂ : ∀ (x : List α), a✝.rmatch x = true ↔ x ∈ a✝.matches'
x : List α
⊢ (a✝¹ + a✝).rmatch x = true ↔ x ∈ (a✝¹ + a✝).matches'
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        (Tape.write (((addBottom L).nth (S k).length).1, update ((addBottom L).nth (S k).length).2 k (some (f v)))
          ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))))) =
    TM1.stepAux q v ((Tape.move Dir.right)^[(S k).length + 1] (Tape.mk' ∅ (addBottom ?m.135)))

Tactic:
this

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        ((Tape.move Dir.right)^[(S k).length]
          (Tape.mk' ∅ (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) (S k).length (addBottom L))))) =
    TM1.stepAux q v ((Tape.move Dir.right)^[(S k).length + 1] (Tape.mk' ∅ (addBottom ?m.135)))
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
R S : RegularExpression α
⊢ map id (R + S) = R + S

Tactic:
[

Goal state after:
α : Type u_1
R S : RegularExpression α
⊢ map id (R + S) = R + S
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
R S : RegularExpression α
⊢ map id (R * S) = R * S

Tactic:
[

Goal state after:
α : Type u_1
R S : RegularExpression α
⊢ map id (R * S) = R * S
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
R : RegularExpression α
⊢ map id R.star = R.star

Tactic:
[

Goal state after:
α : Type u_1
R : RegularExpression α
⊢ map id R.star = R.star
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.succ
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
⊢ ∃ c, ∀ (v : List.Vector ℕ 1), c.eval ↑v = pure <$> (↑fun v ↦ v.head.succ) v

Tactic:
| succ =>

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

Goal state before:
pp: case zero
n : ℕ
⊢ ↑zero >>> n = ↑0

Tactic:
apply Nat.zero_shiftRight

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

Goal state before:
pp: case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (S k) k_1)).reverse) ∧
      TM1.stepAux q
          (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
          (Tape.move Dir.right (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L')))

Tactic:
Function.update_eq_self

Goal state after:
case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
⊢ ∃ L',
    (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
      TM1.stepAux q
          (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
          (Tape.move Dir.right (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L')))