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

Goal state before:
pp: case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
x : List α
a : α
ih : M.evalFrom ∅ x = ∅
⊢ ∅ = ∅

Tactic:
]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ M.toDFA.eval x ∈ M.toDFA.accept ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Tactic:
]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ M.toDFA.eval x ∈ M.toDFA.accept ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ M.toDFA.accepts
hlen : Fintype.card (Set σ) ≤ x.length
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.toDFA.accepts

Tactic:
]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ M.toDFA.accepts
hlen : Fintype.card (Set σ) ≤ x.length
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.toDFA.accepts
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₂⁻¹ * c₃ * ‖f x‖ ≤ c₁ * c₂⁻¹ * c₃ * (c₂ * ‖g x‖)

Tactic:
]

Goal state after:
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₂⁻¹ * c₃ * ‖f x‖ ≤ c₁ * c₂⁻¹ * c₃ * (c₂ * ‖g x‖)
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:
]

Goal state after:
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}
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ (t = s ∧ [] = [] ∨ ∃ t_1 a x, t_1 ∈ M.step s a ∧ M.IsPath t_1 t x ∧ [] = a :: x) ↔ s = t

Tactic:
]

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ (t = s ∧ [] = [] ∨ ∃ t_1 a x, t_1 ∈ M.step s a ∧ M.IsPath t_1 t x ∧ [] = a :: x) ↔ s = t
Module: Mathlib.Computability.NFA

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

Tactic:
]

Goal state after:
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ (∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}) ↔ x ∈ M.accepts
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp
α : Type u
σ : Type v
M : DFA α σ
x : List α
S : σ
hS₁ : M.evalFrom M.start x ∈ M.toNFA.accept
hS₂ : S ∈ {M.evalFrom M.start x}
⊢ x ∈ M.accepts

Tactic:
]

Goal state after:
case mp
α : Type u
σ : Type v
M : DFA α σ
x : List α
S : σ
hS₁ : M.evalFrom M.start x ∈ M.toNFA.accept
hS₂ : S ∈ {M.evalFrom M.start x}
⊢ x ∈ M.accepts
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
⊢ ¬Disjoint S (M.reverse.stepSet S' a) ↔ ¬Disjoint S' (M.stepSet S a)

Tactic:
]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
⊢ ¬Disjoint S (M.reverse.stepSet S' a) ↔ ¬Disjoint S' (M.stepSet S a)
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:
]

Goal state after:
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
Module: Mathlib.Computability.NFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : NFA α σ
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' [])
⊢ Disjoint (List.foldr (fun x y ↦ M.stepSet y x) S []) S'

Tactic:
]

Goal state after:
case nil
α : Type u
σ : Type v
M : NFA α σ
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' [])
⊢ Disjoint (List.foldr (fun x y ↦ M.stepSet y x) S []) S'
Module: Mathlib.Computability.NFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ},
    Disjoint S (List.foldl M.reverse.stepSet S' xs) → Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)
⊢ Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S (x :: xs))

Tactic:
]

Goal state after:
case cons
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ},
    Disjoint S (List.foldl M.reverse.stepSet S' xs) → Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)
⊢ Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S (x :: xs))
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ},
    Disjoint S (List.foldl M.reverse.stepSet S' xs) → Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)
⊢ Disjoint (M.reverse.stepSet S' x) (List.foldr (fun x y ↦ M.stepSet y x) S xs)

Tactic:
]

Goal state after:
case cons
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ},
    Disjoint S (List.foldl M.reverse.stepSet S' xs) → Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)
⊢ Disjoint (M.reverse.stepSet S' x) (List.foldr (fun x y ↦ M.stepSet y x) S xs)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : PosNum
⊢ ¬↑n < ↑m ↔ m ≤ n

Tactic:
]

Goal state after:
m n : PosNum
⊢ ¬↑n < ↑m ↔ m ≤ n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: p : PosNum
⊢ pos p.succ = pos p.succ

Tactic:
]

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

Goal state before:
pp: case false
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif true then Num.bit1 else Num.bit0) (ofNat' n) = (bif false then Num.bit1 else Num.bit0) (ofNat' n) + 1

Tactic:
]

Goal state after:
case false
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif true then Num.bit1 else Num.bit0) (ofNat' n) = (bif false then Num.bit1 else Num.bit0) (ofNat' n) + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' n + 1) = (bif true then Num.bit1 else Num.bit0) (ofNat' n) + 1

Tactic:
]

Goal state after:
case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' n + 1) = (bif true then Num.bit1 else Num.bit0) (ofNat' n) + 1
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:
]

Goal state after:
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)
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ []
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
]

Goal state after:
case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ []
⊢ s₂ ∈ M.εClosure {s₁}
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : Num
⊢ ¬↑n < ↑m ↔ m ≤ n

Tactic:
]

Goal state after:
m n : Num
⊢ ¬↑n < ↑m ↔ m ≤ n
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
]

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

Goal state before:
pp: x✝ : Num
⊢ ↑x✝ = ↑x✝

Tactic:
]

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

Goal state before:
pp: x✝ : Num
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h✝ : M.IsPath s₁ s₂ (List.replicate n none)
⊢ [] = [] ∧ M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
]

Goal state after:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h✝ : M.IsPath s₁ s₂ (List.replicate n none)
⊢ [] = [] ∧ M.IsPath s₁ s₂ (List.replicate n none)
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton
α : 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 ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) ↔ ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
]

Goal state after:
case append_singleton
α : 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 ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) ↔ ∃ x', x'.reduceOption = x ++ [a] ∧ 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₂⁻¹ * c₃ * (c₂ * ‖g x‖) = c₂⁻¹ * c₂ * c₁ * (c₃ * ‖g x‖)

Tactic:
by ring

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

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

Tactic:
]

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

Goal state before:
pp: ⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ n + 1 = n + 1

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n = ↑n

Tactic:
]

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

Goal state before:
pp: m n : Num
x✝ : ↑m ∣ ↑n
k : ℕ
e : ↑n = ↑m * k
⊢ ↑(↑m * k) = m * ↑k

Tactic:
]

Goal state after:
m n : Num
x✝ : ↑m ∣ ↑n
k : ℕ
e : ↑n = ↑m * k
⊢ ↑(↑m * k) = m * ↑k
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : PosNum
h : ↑m = ↑n
⊢ ↑↑n = ↑↑n

Tactic:
]

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

Goal state before:
pp: n : PosNum
⊢ ↑n = ↑n

Tactic:
]

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

Goal state before:
pp: n : PosNum
this : (↑n.pred').succ = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = (↑1 + ↑1).pred

Tactic:
]

Goal state after:
n : PosNum
this : (↑n.pred').succ = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = (↑1 + ↑1).pred
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.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
this : (↑n.pred').succ = ↑n
p : PosNum
h : (↑p).succ = ↑n
⊢ ↑(Num.casesOn (pos p) 1 bit1) = ((↑p).succ + (↑p).succ).pred

Tactic:
]

Goal state after:
n : PosNum
this : (↑n.pred').succ = ↑n
p : PosNum
h : (↑p).succ = ↑n
⊢ ↑(Num.casesOn (pos p) 1 bit1) = ((↑p).succ + (↑p).succ).pred
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : Num
⊢ ↑n = ↑n

Tactic:
]

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

Goal state before:
pp: n : PosNum
⊢ (↑n).size + 1 = (↑n).size.succ

pp: n : PosNum
⊢ Nat.bit false ↑n ≠ 0

Tactic:
]

Goal state after:
n : PosNum
⊢ Nat.bit false ↑n ≠ 0
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:
]

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₂ 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)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ (↑n).size + 1 = (↑n).size.succ

pp: n : PosNum
⊢ Nat.bit true ↑n ≠ 0

Tactic:
]

Goal state after:
n : PosNum
⊢ Nat.bit true ↑n ≠ 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ n.natSize + 1 = n.natSize.succ

Tactic:
]

Goal state after:
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' : List (Option α)
left✝ : x'.reduceOption = x
n : ℕ
h : ∃ t, M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
⊢ ∃ 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' : List (Option α)
left✝ : x'.reduceOption = x
n : ℕ
h : ∃ t, M.IsPath s₁ t x' ∧ M.IsPath t s₂ (some a :: List.replicate n none)
⊢ ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ (↑n).size = (↑n).size

Tactic:
]

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), 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 α σ
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:
]

Goal state after:
α : 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'
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:
]

Goal state after:
α : 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'
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ ↑↑n = ↑↑n

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
toεNFA_εClosure

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

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

Tactic:
]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
m n : PosNum
⊢ m = n ↔ m = n

Tactic:
]

Goal state after:
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.stepSet start = List.foldl M.stepSet start

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
n : PosNum
⊢ 1 ≤ ↑n

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
n : PosNum
⊢ 1 ≤ ↑n
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₁ * ‖g u‖ ≤ ‖f u‖

Tactic:
]

Goal state after:
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₁ * ‖g u‖ ≤ ‖f u‖
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : PosNum
⊢ m < n ↔ m < n

Tactic:
]

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

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

Tactic:
]

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