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

Goal state before:
pp: T : Type u_1
L : Language T
h : L.reverse.IsContextFree
⊢ L.IsContextFree

Tactic:
simpa using

Goal state after:
T : Type u_1
L : Language T
h : L.reverse.IsContextFree
⊢ L.IsContextFree
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (List.range k).length ≤ n

Tactic:
simpa using

Goal state after:
case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ k ≤ n
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: m n : ℕ
h : m < 2 ^ n
⊢ m.size ≤ n

Tactic:
by
    induction m using binaryRec' generalizing n with
    | zero => simp
    | bit b m e IH =>
      rw [← Nat.bit_ne_zero_iff] at e
      rw [size_bit e]
      cases n with
      | zero => exact (e (Nat.lt_one_iff.mp h)).elim
      | succ n => exact succ_le_succ (IH (bit_lt_two_pow_succ_iff.mp h))

Goal state after:
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: n : ℕ
⊢ n.size = 0 ↔ n = 0

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ n.size = 0 ↔ n = 0
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: n : ℕ
⊢ (2 ^ n).size = n + 1

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ (2 ^ n).size = 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
⊢ b = false

Tactic:
simpa using

Goal state after:
b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
⊢ b = false
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: m n : ℕ
⊢ Even (m ^^^ n) ↔ (Even m ↔ Even n)

Tactic:
simp only [even_iff, xor_mod_two_eq]

Goal state after:
m n : ℕ
⊢ (m + n) % 2 = 0 ↔ (m % 2 = 0 ↔ n % 2 = 0)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: x✝¹ x✝ : { f // Computable f }
h : (fun f ↦ ⟨↑↑f, ⋯⟩) x✝¹ = (fun f ↦ ⟨↑↑f, ⋯⟩) x✝
⊢ ↑↑x✝¹ = ↑↑x✝

Tactic:
simpa using

Goal state after:
x✝¹ x✝ : { f // Computable f }
h : (fun f ↦ ⟨↑↑f, ⋯⟩) x✝¹ = (fun f ↦ ⟨↑↑f, ⋯⟩) x✝
⊢ ↑↑x✝¹ = ↑↑x✝
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else ↑n) =
    Num.pos n

Tactic:
PosNum.cast_to_num

Goal state after:
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else Num.pos n) =
    Num.pos n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: b : PosNum
⊢ 1 + b.succ = (1 + b).succ

Tactic:
by simp [one_add]

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

Goal state before:
pp: case cons.none
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
⊢ (map (Option.map f) (none :: tl)).reduceOption = map f (none :: tl).reduceOption

Tactic:
simpa using

Goal state after:
case cons.none
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
⊢ (map (Option.map f) tl).reduceOption = map f tl.reduceOption
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons.some
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
val✝ : α
⊢ (map (Option.map f) (some val✝ :: tl)).reduceOption = map f (some val✝ :: tl).reduceOption

Tactic:
simpa using

Goal state after:
case cons.some
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
val✝ : α
⊢ (map (Option.map f) tl).reduceOption = map f tl.reduceOption
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption = [] ↔ ∃ n, l = replicate n none

Tactic:
dsimp [reduceOption]
  rw [filterMap_eq_nil_iff]
  constructor
  · intro h
    exact ⟨l.length, eq_replicate_of_mem h⟩
  · grind

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
· right; tauto

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

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

Tactic:
exact Nat.le_succ_of_le (Nat.add_lt_add this this)

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s✝ t✝ : σ
x✝ : List α
p : Nonempty (M.Path s✝ t✝ x✝)
t s s' : σ
a : α
x : List α
h₁ : s' ∈ M.step s a
h₂ : M.Path s' t x
⊢ t ∈ M.evalFrom (M.stepSet {s} a) x

Tactic:
stepSet_singleton,

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
s✝ t✝ : σ
x✝ : List α
p : Nonempty (M.Path s✝ t✝ x✝)
t s s' : σ
a : α
x : List α
h₁ : s' ∈ M.step s a
h₂ : M.Path s' t x
⊢ t ∈ M.evalFrom (M.step s a) x
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
exact Nat.le_succ_of_le (Nat.add_lt_add this this)

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a * (b + c) = a * b + a * c

Tactic:
transfer; simp [mul_add]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left✝ : s₂ ∈ M.accept
h : ∃ t ∈ M.start, s₂ ∈ M.evalFrom {t} x
⊢ ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'

Tactic:
obtain ⟨s₁, _, h⟩ := h

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left✝¹ : s₂ ∈ M.accept
s₁ : σ
left✝ : s₁ ∈ M.start
h : s₂ ∈ M.evalFrom {s₁} x
⊢ ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound✝ : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
⊢ c₁ * (c₃ * ‖g x‖) ≤ c₁ * ‖g u‖

Tactic:
by gcongr; exact (hg_bound u hu).1

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
ext S s

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ x✝ ∈ M.toεNFA.stepSet S s ↔ x✝ ∈ M.stepSet S s
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : PosNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
by
  rw [← not_lt]; exact not_congr cast_lt

Goal state after:
Module: Mathlib.Computability.Halting

Goal state before:
pp: case inl
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ ∅ ↔ cg ∈ ∅)
hC : ∀ (f : Code), f ∈ ∅ ↔ f.eval ∈ eval '' ∅
⊢ ComputablePred fun c ↦ c ∈ ∅

Tactic:
simpa using

Goal state after:
case inl
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ ∅ ↔ cg ∈ ∅)
hC : ∀ (f : Code), f ∈ ∅ ↔ f.eval ∈ eval '' ∅
⊢ Computable fun a ↦ false
Module: Mathlib.Computability.Halting

Goal state before:
pp: case inr
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ Set.univ ↔ cg ∈ Set.univ)
hC : ∀ (f : Code), f ∈ Set.univ ↔ f.eval ∈ eval '' Set.univ
⊢ ComputablePred fun c ↦ c ∈ Set.univ

Tactic:
simpa using

Goal state after:
case inr
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ Set.univ ↔ cg ∈ Set.univ)
hC : ∀ (f : Code), f ∈ Set.univ ↔ f.eval ∈ eval '' Set.univ
⊢ Computable fun a ↦ true
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : Num
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
by
  rw [← not_lt]; exact not_congr cast_lt

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
⊢ (∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n) ∧
    ((rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n).Dom ↔ (cf.eval n).Dom ∨ (cg.eval n).Dom)

Tactic:
have : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n,
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n := by
    intro x h
    obtain ⟨k, e⟩ := Nat.rfindOpt_spec h
    rw [Option.mem_def, Option.orElse_eq_some, ← Option.mem_def, ← Option.mem_def] at e
    obtain e | ⟨-, e⟩ := e <;> simp [Code.evaln_sound e]

Goal state after:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this✝ : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
⊢ (∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n) ∧
    ((rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n).Dom ↔ (cf.eval n).Dom ∨ (cg.eval n).Dom)
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' f
hg : Partrec' ↑g
⊢ Partrec' fun v ↦ Part.map (fun a ↦ g (a ::ᵥ v)) (f v)

Tactic:
simpa using

Goal state after:
n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' f
hg : Partrec' ↑g
⊢ Partrec' fun v ↦ (f v).bind fun y ↦ Part.some (g (y ::ᵥ v))
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n : ℕ
f : ℕ →. ℕ
g : List.Vector ℕ n → ℕ
hf : Partrec' fun v ↦ f v.head
hg : Partrec' ↑g
⊢ Partrec' fun v ↦ f (g v)

Tactic:
simpa using

Goal state after:
n : ℕ
f : ℕ →. ℕ
g : List.Vector ℕ n → ℕ
hf : Partrec' fun v ↦ f v.head
hg : Partrec' ↑g
⊢ Partrec' fun v ↦ f (g v)
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: c : Partrec.Code
hf : Nat.Partrec c.eval
⊢ Partrec' fun v ↦ c.eval v.head

Tactic:
simpa using

Goal state after:
c : Partrec.Code
hf : Nat.Partrec c.eval
⊢ Partrec' fun v ↦ Nat.rfindOpt fun k ↦ evaln k c v.head
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ m → List.Vector ℕ n
h : Vec f
⊢ Computable f

Tactic:
simpa using

Goal state after:
m n : ℕ
f : List.Vector ℕ m → List.Vector ℕ n
h : Vec f
⊢ Computable f
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : α → Bool
h : Computable f
⊢ Computable fun a ↦ decide ((fun a ↦ f a = true) a)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
h : Computable f
⊢ Computable fun a ↦ f a
Module: Mathlib.Computability.RE

Goal state before:
pp: f₁ f₂ : ℕ → ℕ
hf₁ : Computable f₁
hf₂ : Computable f₂
c : ℕ → Prop
inst✝ : DecidablePred c
hc : ComputablePred c
⊢ Computable fun k ↦ if c k then f₁ k else f₂ k

Tactic:
simpa using

Goal state after:
f₁ f₂ : ℕ → ℕ
hf₁ : Computable f₁
hf₂ : Computable f₂
c : ℕ → Prop
inst✝ : DecidablePred c
hc : ComputablePred c
⊢ Computable fun k ↦ if c k then f₁ k else f₂ k
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i : ℕ
L : ListBlank Γ
⊢ (modifyNth f 0 L).nth i = if i = 0 then f (L.nth i) else L.nth i

Tactic:
cases i <;> simp only [ListBlank.nth_zero, if_true, ListBlank.head_cons, ListBlank.modifyNth,
      ListBlank.nth_succ, if_false, ListBlank.tail_cons, reduceCtorEq]

Goal state after:
Module: Mathlib.Computability.RecursiveIn

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

Tactic:
by
  simp [RecursiveIn, Part.map_id']

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
n : ℕ
⊢ T.right₀.nth n = T.nth ↑n

Tactic:
cases n <;> simp only [Tape.nth, Tape.right₀, ListBlank.nth_zero,
    ListBlank.nth_succ, ListBlank.head_cons, ListBlank.tail_cons]

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
O O' : Set (ℕ →. ℕ)
f : α →. σ
hf : RecursiveIn O f
hO : ∀ g ∈ O, RecursiveIn O' g
⊢ ∀ g ∈ O, Nat.RecursiveIn O' g

Tactic:
simpa using

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
O O' : Set (ℕ →. ℕ)
f : α →. σ
hf : RecursiveIn O f
hO : ∀ g ∈ O, RecursiveIn O' g
⊢ ∀ g ∈ O, Nat.RecursiveIn O' g
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Partrec g
hf : RecursiveIn O f
⊢ ∀ g ∈ O, Nat.Partrec g

Tactic:
simpa using

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Partrec g
hf : RecursiveIn O f
⊢ ∀ g ∈ O, Nat.Partrec g
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a ↦ g a = true
hf : ∀ (a : α), p a ↔ (fun a ↦ g a = true) (f a)
⊢ Computable fun a ↦ decide ((fun a ↦ (fun a ↦ g a = true) (f a)) a)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a ↦ g a = true
hf : ∀ (a : α), p a ↔ (fun a ↦ g a = true) (f a)
⊢ Computable fun a ↦ g (f a)
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 hq

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

Goal state before:
pp: case h.h.h
p✝² p✝¹ p✝ : Set ℕ
⊢ of p✝² + of p✝¹ ≤ of p✝ ↔ of p✝² ≤ of p✝ ∧ of p✝¹ ≤ of p✝

Tactic:
simpa using

Goal state after:
case h.h.h
p✝² p✝¹ p✝ : Set ℕ
⊢ p✝² ⊕' p✝¹ ≤₀ p✝ ↔ p✝² ≤₀ p✝ ∧ p✝¹ ≤₀ p✝
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
refine TM1.stmts_trans ?_ h₂

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

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

Tactic:
refine TM1.stmts_trans ?_ h₂

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

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

Tactic:
intro _h
        use []; dsimp; tauto

Goal state after:
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)

Tactic:
simp only [addBottom, ListBlank.head_cons, ListBlank.modifyNth, ListBlank.tail_cons]

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

Goal state before:
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:
simp only [addBottom, ListBlank.head_cons, ListBlank.modifyNth, ListBlank.tail_cons]

Goal state after:
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.cons (true, L.head)
      (ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)) =
    ListBlank.cons (true, L.head) (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail))
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mpr.cons.cons.cons.refine_1
α : 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)
U : List (List α)
b : α
t : List α
helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ (P.deriv a).rmatch t = true

Tactic:
specialize helem (b :: t) (by simp)

Goal state after:
case mpr.cons.cons.cons.refine_1
α : 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)
U : List (List α)
b : α
t : List α
helem : b :: t ≠ [] ∧ P.rmatch (b :: t) = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ (P.deriv a).rmatch t = true
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

Tactic:
simp only [trStmts₁, stRun]

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
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trStmts₁ (stRun (StAct.peek a✝) q) = {go k (StAct.peek a✝) q, ret q} ∪ trStmts₁ q

Tactic:
simp only [trStmts₁, stRun]

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

Goal state before:
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:
simp only [trStmts₁, stRun]

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

Goal state before:
pp: ⊢ ∀ (m n : Num), ↑(m &&& n) = ↑m &&& ↑n

Tactic:
apply castNum_eq_bitwise PosNum.land <;> intros <;> (try cases_type* Bool) <;> rfl

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

Goal state before:
pp: n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i✝ : Fin n✝
n : ℕ
i : Fin n
c : Code
h : ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> (↑fun v ↦ v.get i) v
v : List.Vector ℕ n.succ
⊢ (c.comp tail).eval ↑v = pure <$> (↑fun v ↦ v.get i.succ) v

Tactic:
simpa using

Goal state after:
n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i✝ : Fin n✝
n : ℕ
i : Fin n
c : Code
h : ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> (↑fun v ↦ v.get i) v
v : List.Vector ℕ n.succ
⊢ c.eval (↑v).tail = pure <$> Part.some (v.get i.succ)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.comp
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ → ℕ
m✝ n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
g : Fin n✝ → List.Vector ℕ m✝ → ℕ
hf : Nat.Primrec' f✝
hg : ∀ (i : Fin n✝), Nat.Primrec' (g i)
IHf : ∃ c, ∀ (v : List.Vector ℕ n✝), c.eval ↑v = pure <$> ↑f✝ v
IHg : ∀ (i : Fin n✝), ∃ c, ∀ (v : List.Vector ℕ m✝), c.eval ↑v = pure <$> ↑(g i) v
⊢ ∃ c, ∀ (v : List.Vector ℕ m✝), c.eval ↑v = pure <$> (↑fun a ↦ f✝ (List.Vector.ofFn fun i ↦ g i a)) v

Tactic:
simpa using

Goal state after:
case prim.comp
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ → ℕ
m✝ n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
g : Fin n✝ → List.Vector ℕ m✝ → ℕ
hf : Nat.Primrec' f✝
hg : ∀ (i : Fin n✝), Nat.Primrec' (g i)
IHf : ∃ c, ∀ (v : List.Vector ℕ n✝), c.eval ↑v = pure <$> ↑f✝ v
IHg : ∀ (i : Fin n✝), ∃ c, ∀ (v : List.Vector ℕ m✝), c.eval ↑v = pure <$> ↑(g i) v
⊢ ∃ c, ∀ (v : List.Vector ℕ m✝), c.eval ↑v = pure <$> Part.some (f✝ (List.Vector.ofFn fun i ↦ g i v))
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg.inl.h
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))
i : ℕ
h✝ : ¬i = (S k).length
h : i < (S k).length
⊢ i < (List.map some (S k)).reverse.length

Tactic:
simpa using

Goal state after:
case neg.inl.h
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))
i : ℕ
h✝ : ¬i = (S k).length
h : i < (S k).length
⊢ i < (S k).length