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

Goal state before:
pp: case f
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ
| do
    let y ← lup p.1.1.1.1 ((ofNat (ℕ × Code) p.1.1.1.1.length).1, p.1.2.2.1) p.1.1.1.2
    some (Nat.pair p.2 y)

Tactic:
erw [Option.bind_eq_bind, ← Option.map_eq_bind]

Goal state after:
case f
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ
| Option.map (Nat.pair p.2) (lup p.1.1.1.1 ((ofNat (ℕ × Code) p.1.1.1.1.length).1, p.1.2.2.1) p.1.1.1.2)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ (fun n ↦ 1 * asympBound g a b n) ~[atTop] fun n ↦ (1 + ε ↑n) * asympBound g a b n

Tactic:
refine IsEquivalent.mul (IsEquivalent.symm ?_) IsEquivalent.refl

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ (fun n ↦ 1 + ε ↑n) ~[atTop] fun n ↦ 1
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
i : ℕ
⊢ n.testBit i = false

Tactic:
rw [← h (i + 1), testBit_bit_succ]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.comp
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.comp cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.comp cg)))))
          (k', c') n =
        evaln k' c' n
⊢ ((lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
          (k' + 1, cg) n).bind
      fun x ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x) =
    (evaln (k' + 1) cg n).bind fun x ↦ evaln (k' + 1) cf x

Tactic:
obtain ⟨lf, lg⟩ := encode_lt_comp cf cg
        rw [hg (Nat.pair_lt_pair_right _ lg)]
        cases evaln k cg n
        · rfl
        simp [k, hg (Nat.pair_lt_pair_right _ lf)]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.prec.succ
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ : ℕ
⊢ ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n✝)).bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n✝)).bind fun i ↦
      evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))

Tactic:
cases evaln k' _ _

Goal state after:
case succ.prec.succ.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ : ℕ
⊢ (Option.none.bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    Option.none.bind fun i ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))

case succ.prec.succ.some
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ val✝ : ℕ
⊢ ((some val✝).bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    (some val✝).bind fun i ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : PosNum
⊢ ↑↑n = ↑n

Tactic:
cast_to_nat

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : PosNum
⊢ ↑n = ↑n
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ [] ∈ M.acceptsFrom S ↔ ∃ s ∈ S, s ∈ M.accept

Tactic:
by
  simp only [mem_acceptsFrom, evalFrom_nil]; tauto

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : Num
⊢ ↑↑n = ↑n

Tactic:
cast_to_nat

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : Num
⊢ ↑n = ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
m n : PosNum
⊢ ↑m + ↑↑n = ↑m + ↑n

Tactic:
cast_to_nat

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
m n : PosNum
⊢ ↑m + ↑n = ↑m + ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
n : PosNum
⊢ ↑n.succ = ↑n + 1

Tactic:
by
  rw [← add_one, cast_add, cast_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
m n : PosNum
⊢ ↑m * ↑↑n = ↑m * ↑n

Tactic:
cast_to_nat

Goal state after:
α : Type u_1
inst✝ : NonAssocSemiring α
m n : PosNum
⊢ ↑m * ↑n = ↑m * ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
n : Num
⊢ ↑↑n + 1 = ↑n + 1

Tactic:
cast_to_nat

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
n : Num
⊢ ↑n + 1 = ↑n + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
m n : Num
⊢ ↑m + ↑↑n = ↑m + ↑n

Tactic:
cast_to_nat

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
m n : Num
⊢ ↑m + ↑n = ↑m + ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero
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)
m : PosNum
⊢ ↑(f (pos m) 0) = Nat.bitwise g (↑(pos m)) 0

Tactic:
rw [fn0, Nat.bitwise_zero_right]

Goal state after:
case pos.zero
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)
m : PosNum
⊢ ↑(bif g true false then pos m else 0) = if g true false = true then ↑(pos m) else 0
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l l₁ l₂ : List Γ
⊢ BlankExtends l₁ l → BlankExtends l₂ l → l₁.length ≤ l₂.length → BlankExtends l₁ l₂

Tactic:
rintro ⟨i, rfl⟩ ⟨j, e⟩ h

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ BlankExtends l₁ l₂
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b : σ
⊢ b ∈ eval f a ↔ Reaches f a b ∧ f b = none

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩
  · refine evalInduction h fun a h IH ↦ ?_
    rcases e : f a with - | a'
    · rw [Part.mem_unique h
          (PFun.mem_fix_iff.2 <| Or.inl <| Part.mem_some_iff.2 <| by rw [e]; rfl)]
      exact ⟨ReflTransGen.refl, e⟩
    · rcases PFun.mem_fix_iff.1 h with (h | ⟨_, h, _⟩) <;> rw [e] at h <;>
        cases Part.mem_some_iff.1 h
      obtain ⟨h₁, h₂⟩ := IH a' e
      exact ⟨ReflTransGen.head e h₁, h₂⟩
  · refine ReflTransGen.head_induction_on h₁ ?_ fun h _ IH ↦ ?_
    · refine PFun.mem_fix_iff.2 (Or.inl ?_)
      rw [h₂]
      apply Part.mem_some
    · refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH⟩)
      rw [h]
      apply Part.mem_some

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
x✝ : REPred p ∧ REPred fun a ↦ ¬p a
h₁ : REPred p
h₂ : REPred fun a ↦ ¬p a
⊢ Computable fun a ↦ decide (p a)

Tactic:
by
      obtain ⟨k, pk, hk⟩ :=
        Partrec.merge (h₁.map (Computable.const true).to₂) (h₂.map (Computable.const false).to₂)
        (by
          intro a x hx y hy
          simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
            and_true, exists_const] at hx hy
          cases hy.1 hx.1)
      refine Partrec.of_eq pk fun n => Part.eq_some_iff.2 ?_
      rw [hk]
      simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
        true_eq_decide_iff, and_self, exists_const, false_eq_decide_iff]
      apply Decidable.em

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
g₁ : σ₁
eg : f₁ e₁ = some g₁
⊢ ∀ (x : σ₂), tr g₁ x → Reaches₁ f₂ b✝ x → ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
· intro g₂ gg cg
        rcases TransGen.head'_iff.1 cg with ⟨d', cd', dg⟩
        cases Option.mem_unique cd cd'
        exact ⟨_, _, dg, gg, ae.tail eg⟩

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

Goal state before:
pp: case zero
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), F.f (f x) = f' (F.f x)
L : ListBlank Γ
⊢ map F (modifyNth f 0 L) = modifyNth f' 0 (map F L)

Tactic:
simp only [*, ListBlank.head_map, ListBlank.modifyNth, ListBlank.map_cons, ListBlank.tail_map]

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

Goal state before:
pp: case succ
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), F.f (f x) = f' (F.f x)
n✝ : ℕ
a✝ : ∀ (L : ListBlank Γ), map F (modifyNth f n✝ L) = modifyNth f' n✝ (map F L)
L : ListBlank Γ
⊢ map F (modifyNth f (n✝ + 1) L) = modifyNth f' (n✝ + 1) (map F L)

Tactic:
simp only [*, ListBlank.head_map, ListBlank.modifyNth, ListBlank.map_cons, ListBlank.tail_map]

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: d : ManyOneDegree
⊢ d ≤ d

Tactic:
by
  induction d using ManyOneDegree.ind_on; simp; rfl

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
x : List α
⊢ (P + Q).rmatch x = true ↔ P.rmatch x = true ∨ Q.rmatch x = true

Tactic:
induction x generalizing P Q with

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
x : List α
⊢ (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
induction x generalizing P Q with

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
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' (?m.157 i) (?m.158 i) σ) σ) (L' R' : ListBlank Bool)
    (l₁ l₂ : List Bool) (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
⊢ ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v
        (Tape.mk' (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯)
          (ListBlank.append (enc a).toList (R.flatMap (fun x ↦ (enc x).toList) ⋯))) =
      stepAux (f (enc a)) 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:
intro f

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' (?m.157 i) (?m.158 i) σ) σ) (L' R' : ListBlank Bool)
    (l₁ l₂ : List Bool) (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux n f) v
      (Tape.mk' (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯)
        (ListBlank.append (enc a).toList (R.flatMap (fun x ↦ (enc x).toList) ⋯))) =
    stepAux (f (enc a)) v
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯))
        (R.flatMap (fun x ↦ (enc x).toList) ⋯))
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail) = L.tail

Tactic:
generalize ListBlank.tail L = L'

Goal state after:
K : Type u_1
Γ : K → Type u_2
L L' : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L') = L'
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L R : ListBlank Γ
⊢ stepAux (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R)

Tactic:
by
  suffices ∀ f, stepAux (readAux n f) v (trTape' enc0 L R) =
      stepAux (f (enc R.head)) v (trTape' enc0 (L.cons R.head) R.tail) by
    rw [read, this, stepAux_move, encdec, trTape'_move_left enc0]
    simp only [ListBlank.head_cons, ListBlank.cons_head_tail, ListBlank.tail_cons]
  obtain ⟨a, R, rfl⟩ := R.exists_cons
  simp only [ListBlank.head_cons, ListBlank.tail_cons, trTape', ListBlank.cons_flatMap]
  suffices ∀ i f L' R' l₁ l₂ h,
      stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R') by
    intro f
    exact this n f (L.flatMap (fun x => (enc x).1.reverse) _)
      (R.flatMap (fun x => (enc x).1) _) [] _ (enc a).2
  clear f L a R
  rintro _ f L' R' l₁ l₂ rfl
  induction l₂ generalizing l₁ with
  | nil => rfl
  | cons a l₂ IH =>
    trans stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
        (Tape.mk' ((L'.append l₁).cons a) (R'.append l₂))
    · dsimp [readAux, stepAux]
      simp only [ListBlank.head_cons, Tape.move_right_mk', ListBlank.tail_cons]
      cases a <;> rfl
    · rw [← ListBlank.append, IH]
      rfl

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

Goal state before:
pp: case prim.prec
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v).tail = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval ↑(v.head ::ᵥ v.tail) =
    pure <$> (↑fun v ↦ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head) (v.head ::ᵥ v.tail)

Tactic:
simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, PFun.coe_val, Vector.tail_val]

Goal state after:
case prim.prec
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v).tail = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval (v.head :: (↑v).tail) =
    Part.some
      (pure
        (Nat.rec (f (v.head ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (v.head ::ᵥ v.tail).tail))
          (v.head ::ᵥ v.tail).head))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m + 1).shiftRight (1 + n)

Tactic:
@Nat.shiftRight_eq _ (1 + n),

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m + 1) >>> (1 + n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m).shiftRight (1 + n)

Tactic:
@Nat.shiftRight_eq _ (1 + n),

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m) >>> (1 + n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.one
⊢ one.testBit 0 = (↑one).testBit 0

Tactic:
simp only [PosNum.testBit]

Goal state after:
case pos.zero.one
⊢ true = (↑one).testBit 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.bit1
m : PosNum
⊢ m.bit1.testBit 0 = (↑m.bit1).testBit 0

Tactic:
simp only [PosNum.testBit]

Goal state after:
case pos.zero.bit1
m : PosNum
⊢ true = (↑m.bit1).testBit 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.bit0
m : PosNum
⊢ m.bit0.testBit 0 = (↑m.bit0).testBit 0

Tactic:
simp only [PosNum.testBit]

Goal state after:
case pos.zero.bit0
m : PosNum
⊢ false = (↑m.bit0).testBit 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ one.testBit (n✝ + 1) = (↑one).testBit (n✝ + 1)

Tactic:
simp only [PosNum.testBit]

Goal state after:
case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ false = (↑one).testBit (n✝ + 1)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.bit1
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.bit1.testBit (n✝ + 1) = (↑m.bit1).testBit (n✝ + 1)

Tactic:
simp only [PosNum.testBit]

Goal state after:
case pos.succ.bit1
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit1).testBit (n✝ + 1)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.bit0.testBit (n✝ + 1) = (↑m.bit0).testBit (n✝ + 1)

Tactic:
simp only [PosNum.testBit]

Goal state after:
case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit0).testBit (n✝ + 1)