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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu✝ : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
⊢ 0 ≤ (c₂ - c₁) * f x

Tactic:
linarith

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu✝ : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
hu' : 0 ≤ (c₂ - c₁) * f x
⊢ 0 < c₂ - c₁

Tactic:
linarith

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 + ε ↑n

Tactic:
filter_upwards [eventually_one_add_smoothingFn_pos] with n hn; exact le_of_lt hn

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 3 / 4 * x ≤ x

Tactic:
linarith

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu✝ : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
⊢ (c₁ - c₂) * f x ≤ 0

Tactic:
linarith

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu✝ : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
hu' : (c₁ - c₂) * f x ≤ 0
⊢ 0 < c₁ - c₂

Tactic:
linarith

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁ : ∑ x, 0 = 0
i : α
x✝ : i ∈ univ
this : 0 < b i
⊢ -1 < b i

Tactic:
linarith

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
this : 0 < b (max_bi b)
⊢ 0 < b (max_bi b)

Tactic:
linarith

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)

Tactic:
filter_upwards [hf] with x hx

Goal state after:
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inr.inr
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
hmain : (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ |f x| * |g x|
⊢ GrowsPolynomially fun x ↦ f x * g x

Tactic:
simp only [iff_eventuallyEq hmain]

Goal state after:
case inr.inr
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
hmain : (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ |f x| * |g x|
⊢ GrowsPolynomially fun x ↦ |f x| * |g x|
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
this : c₃ < 1
⊢ 0 < 1 - c₃

Tactic:
linarith

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k + 1) cf a) fun y ↦ do
                let i ← evaln k (cf.prec cg) (Nat.pair a y)
                evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
⊢ evaln (k + 1) cf (unpair n).1 = some x → evaln (k₂ + 1) cf (unpair n).1 = some x

Tactic:
apply hf

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
x : ℕ
⊢ evaln (k + 1) cf (unpair n).1 = some x → x ∈ cf.eval (unpair n).1

Tactic:
apply hf

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
⊢ l∗ = ⨆ i, l ^ i

Tactic:
ext x
  simp only [mem_kstar, mem_iSup, mem_pow]
  grind

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case cons
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
q : List (Symbol T N)
d : Symbol T N
l : List (Symbol T N)
ih : r.Rewrites (l ++ [Symbol.nonterminal r.input] ++ q) (l ++ r.output ++ q)
⊢ r.Rewrites (d :: l ++ [Symbol.nonterminal r.input] ++ q) (d :: l ++ r.output ++ q)

Tactic:
exact Rewrites.cons d ih

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
x✝ : List (Symbol T g.NT)
hx : g.Produces [Symbol.nonterminal t] x✝
hxr : ∃ r ∈ g.rules, r.input = t
⊢ ¬g.Derives x✝ s

Tactic:
tauto

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

Goal state before:
pp: case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ bit b✝ n✝ ≠ 0

Tactic:
simpa [bit_eq_zero_iff]

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ (c₁ * f x) ^ p ≤ f u ^ p

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

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

Goal state before:
pp: n m i : ℕ
hn : n.testBit i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j
⊢ n < m

Tactic:
induction n using Nat.binaryRec generalizing i m with

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hneg : ∀ᶠ (x : ℝ) in atTop, f x < 0
x : ℝ
hx : 0 ≤ f x
hx' : f x < 0
⊢ False

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑↑p.bit0 = ↑p.bit0

Tactic:
dsimp; rw [Nat.cast_add, p.cast_to_nat]

Goal state after:
Module: Mathlib.Computability.NFA

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

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.NFA

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

Tactic:
tauto

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 T

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mpr.inl
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mpr.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.NFA

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

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : NFA α σ
p : Prop
S : Set σ
⊢ (∃ s, (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
s : σ
⊢ (∃ i, (i ∈ S ∧ p) ∧ s ∈ M.step i a) ↔ (∃ i ∈ S, s ∈ M.step i a) ∧ p

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s t : σ
x : List α
h : t = s
⊢ s = t

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case base
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s✝ : σ
a✝ : s✝ ∈ S
⊢ ∃ t ∈ S, s✝ ∈ M.εClosure {t}

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : DFA α σ
start : σ
⊢ List.foldl M.toNFA.stepSet {start} [] = {List.foldl M.step start []}

Tactic:
tauto

Goal state after:
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 : σ
⊢ (∃ t, (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l✝) ∧ s ∈ M.εClosure (M.step t (some a✝))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l✝, s ∈ M.εClosure (M.step t_1 (some a✝))

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl M.toNFA.stepSet {M.step start a} s = {List.foldl M.step (M.step start a) s}

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s t : σ
a : Option α
⊢ t ∈ M.step s a → M.IsPath s t [a]

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
s : σ
⊢ M.IsPath s u y → ∃ t, M.IsPath s t [] ∧ M.IsPath t u y

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case cons.cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ t, M.IsPath s t a ∧ M.IsPath t u y
s t : σ
a✝ : t ∈ M.step s x
h : ∃ t_1, M.IsPath t t_1 a ∧ M.IsPath t_1 u y
⊢ ∃ t, M.IsPath s t (x :: a) ∧ M.IsPath t u y

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil.nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right✝ : M.IsPath t u y
⊢ M.IsPath t u ([] ++ y)

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case cons.cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right✝ : M.IsPath t u y
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : ∀ {s : σ}, M.IsPath s t tail✝ → M.IsPath s u (tail✝ ++ y)
s t✝ : σ
a✝¹ : t✝ ∈ M.step s head✝
a✝ : M.IsPath t✝ t tail✝
⊢ M.IsPath s u (head✝ :: tail✝ ++ y)

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
tauto

Goal state after:
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₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
x' : List (Option α)
left✝¹ : x'.reduceOption = x
right✝ : M.IsPath s₁ t x'
u : σ
left✝ : u ∈ M.step t (some a)
n : ℕ
h✝ : M.IsPath u s₂ (List.replicate n none)
⊢ x'.reduceOption ++ [a] = x ++ [a] ∧ ∃ t, M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)

Tactic:
tauto

Goal state after:
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), ∃ n, M.IsPath t_1 s₂ (List.replicate n none)

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case step
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a s✝ : σ
a✝ : M.toεNFA.εClosure S s✝
h : a ∈ M.toεNFA.step s✝ none
⊢ a ∈ S

Tactic:
cases h

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

Goal state before:
pp: m n : PosNum
⊢ m.cmp n = Ordering.eq ↔ m = n

Tactic:
have := cmp_to_nat m n

Goal state after:
m n : PosNum
this : Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ m.cmp n = Ordering.eq ↔ m = n
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
x : List α
this : ↑(L.toDFA.eval x) = L.leftQuotient x
⊢ L.toDFA.eval x ∈ L.toDFA.accept ↔ x ∈ L

Tactic:
simp [this]

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

Goal state before:
pp: b : Bool
n : ℕ
IH : ofNat' n = ↑n
⊢ ofNat' (Nat.bit b n) = ↑(Nat.bit b n)

Tactic:
tauto

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

Goal state before:
pp: case zero.zero
h : zero.toZNum = zero.toZNum
⊢ zero = zero

Tactic:
cases h

Goal state after:
case zero.zero.refl
⊢ zero = zero
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero.pos
a✝ : PosNum
h : zero.toZNum = (pos a✝).toZNum
⊢ zero = pos a✝

Tactic:
cases h

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

Goal state before:
pp: case pos.zero
a✝ : PosNum
h : (pos a✝).toZNum = zero.toZNum
⊢ pos a✝ = zero

Tactic:
cases h

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

Goal state before:
pp: case pos.pos
a✝¹ a✝ : PosNum
h : (pos a✝¹).toZNum = (pos a✝).toZNum
⊢ pos a✝¹ = pos a✝

Tactic:
cases h

Goal state after:
case pos.pos.refl
a✝ : PosNum
⊢ pos a✝ = pos a✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : Num
⊢ m.cmp n = Ordering.eq ↔ m = n

Tactic:
have := cmp_to_nat m n

Goal state after:
m n : Num
this : Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ m.cmp n = Ordering.eq ↔ m = n
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_1.e_a
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = ↑(some (ofNat (Option ℕ) (f (n ::ᵥ v))).isSome)

Tactic:
cases f (n ::ᵥ v) <;> simp <;> rfl

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

Goal state before:
pp: case nil.succ
Γ : Type ?u.5
inst✝ : Inhabited Γ
l : ListBlank Γ
i : ℕ
⊢ BlankExtends [].tail ([] ++ List.replicate (i + 1) default).tail

Tactic:
exact ⟨i, rfl⟩

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

Goal state before:
pp: case cons
Γ : Type ?u.5
inst✝ : Inhabited Γ
l : ListBlank Γ
i : ℕ
head✝ : Γ
tail✝ : List Γ
⊢ BlankExtends (head✝ :: tail✝).tail (head✝ :: tail✝ ++ List.replicate i default).tail

Tactic:
exact ⟨i, rfl⟩

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

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

Tactic:
induction n generalizing i L with

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.nil.isTrue
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
h✝ : a = head✝
⊢ rmatch 1 [] = true ↔ head✝ = a

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.nil.isFalse
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
h✝ : ¬a = head✝
⊢ rmatch 0 [] = true ↔ head✝ = a

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case nil.mp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ ∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
refine ⟨[], [], rfl, ?_⟩

Goal state after:
case nil.mp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ P.rmatch [] = true ∧ Q.rmatch [] = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : 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
t u : List α
h✝ : x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
⊢ a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : 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
t u : List α
h : x = t ++ u
hP : (P.deriv a).rmatch t = true
hQ : Q.rmatch u = true
⊢ a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true

Tactic:
tauto

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

Goal state before:
pp: case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
v✝ : List.Vector Bool i
⊢ SupportsStmt S (f (true ::ᵥ v✝))

Tactic:
apply hf

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

Goal state before:
pp: case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
v✝ : List.Vector Bool i
⊢ SupportsStmt S (f (false ::ᵥ v✝))

Tactic:
apply hf

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case h
α : 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)
_h : P.star.rmatch [] = true
⊢ [] = [] ∧ ∀ t ∈ [], ¬t = [] ∧ P.rmatch t = true

Tactic:
tauto

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✝
⊢ (Tape.move Dir.right)^[i + 1] ((Tape.move Dir.left)^[i + 1] L✝) = L✝

Tactic:
iterate_succ_apply,

Goal state after:
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✝
⊢ (Tape.move Dir.right)^[i] (Tape.move Dir.right ((Tape.move Dir.left)^[i + 1] L✝)) = L✝
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)
helem : ∀ t ∈ [], t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = [].flatten
⊢ x = [] ++ [] ∧ (P.deriv a).rmatch [] = true ∧ P.star.rmatch [] = true

Tactic:
tauto

Goal state after: