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

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

Tactic:
by

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

Goal state before:
pp: b : Bool
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit b n + 1) = ofNat' (Nat.bit b n) + 1

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ ofNat' (m + n) = ofNat' m + ofNat' n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : s₂ ∈ M.εClosure {s₁}
⊢ ∃ n, M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
by

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

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Tactic:
by

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

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

Goal state before:
pp: m n : Num
h : Ordering.casesOn Ordering.lt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
by

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

Goal state before:
pp: m n : Num
h : Ordering.casesOn Ordering.eq (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
by

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

Goal state before:
pp: m n : Num
h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.gt = Ordering.lt

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ Num.ofNat' ↑1 = Num.pos 1

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ (∃ n, M.IsPath s₁ s₂ (List.replicate n none)) → s₂ ∈ M.εClosure {s₁}

Tactic:
by

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

Goal state before:
pp: p : PosNum
⊢ Num.ofNat' ↑p.bit0 = Num.pos p.bit0

Tactic:
by

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

Goal state before:
pp: p : PosNum
⊢ Num.ofNat' ↑p.bit1 = Num.pos p.bit1

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b c : Num), a + b + c = a + (b + c)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by rw [← to_nat_inj, mul_to_nat, cast_zero, zero_mul]

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a : Num), a ≤ a

Tactic:
by

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

Goal state before:
pp: a b c : Num
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
by

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

Goal state before:
pp: a b : Num
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by

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

Goal state before:
pp: a b : Num
⊢ a ≤ b → b ≤ a → a = b

Tactic:
by

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

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

Goal state before:
pp: a b : Num
h : a ≤ b
c : Num
⊢ a + c ≤ b + c

Tactic:
by

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

Goal state before:
pp: a b c : Num
⊢ a + b ≤ a + c → b ≤ c

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : Num), a ≤ b ∨ b ≤ a

Tactic:
by

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

Goal state before:
pp: ⊢ 0 ≤ 1

Tactic:
by

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
by

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

Goal state before:
pp: a : Num
ha : 0 < a
b c : Num
⊢ b < c → a * b < a * c

Tactic:
by

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

Goal state before:
pp: a : Num
ha : 0 < a
b c : Num
⊢ b < c → b * a < c * a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ ↑↑0 = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑↑(n + 1) = n + 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : PosNum
⊢ (↑n.pred').succ = ↑n

Tactic:
by

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) = (↑n + ↑n).pred

Tactic:
by

Goal state after:
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₃ * ‖g x‖)

Tactic:
by

Goal state after:
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) = (↑n + ↑n).pred

Tactic:
by

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

Goal state before:
pp: n : Num
⊢ ↑n.succ'.pred' = ↑n

Tactic:
by

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

Goal state before:
pp: n : PosNum
⊢ ↑n.pred'.succ' = ↑n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : PosNum
⊢ ↑n.bit0.size = n.bit0.natSize

Tactic:
by

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

Goal state before:
pp: n : PosNum
⊢ ↑n.bit1.size = n.bit1.natSize

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : PosNum
⊢ 0 < n.natSize

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), a ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a ≤ b → b ≤ c → a ≤ c

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a ≤ b → b ≤ a → a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a ≤ b ∨ b ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ DecidableLE PosNum

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ DecidableEq PosNum

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ DecidableLT PosNum

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: b : Bool
n : PosNum
⊢ ↑(bit b n) = Nat.bit b ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
x : List α
⊢ (∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x') → x ∈ M.accepts

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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:
by

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.toεNFA.stepSet start = List.foldl M.stepSet start

Tactic:
by

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:
by

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

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

Tactic:
by

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:
by

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

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
by

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

Goal state before:
pp: b : Bool
n : Num
⊢ ↑(bit b n) = Nat.bit b ↑n

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Halting

Goal state before:
pp: C : Set (ℕ →. ℕ)
h : ComputablePred fun c ↦ c.eval ∈ C
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
⊢ g ∈ C

Tactic:
by

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

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Halting

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Halting

Goal state before:
pp: C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
⊢ (ComputablePred fun c ↦ c ∈ C) ↔ C = ∅ ∨ C = Set.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
n : Num
⊢ ↑n.bit0 = 2 * ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
n : Num
⊢ ↑n.bit1 = 2 * ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
x y : List α
⊢ L.leftQuotient (x ++ y) = (L.leftQuotient x).leftQuotient y

Tactic:
by

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ M.accepts.leftQuotient x = M.acceptsFrom (M.eval x)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
h : L.IsRegular
⊢ (Set.range L.leftQuotient).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
σ : Type v
L : Language α
s : ↑(Set.range L.leftQuotient)
a : α
⊢ ↑(Set.range L.leftQuotient)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
σ : Type v
L : Language α
⊢ L ∈ Set.range L.leftQuotient

Tactic:
by

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

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
⊢ L.toDFA.accepts = L

Tactic:
by

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
h : (Set.range L.leftQuotient).Finite
⊢ L.toDFA.accepts = L

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ ofNat' 0 = ↑0

Tactic:
by

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:
by

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

Goal state before:
pp: n : Num
⊢ -n.toZNum = n.toZNumNeg

Tactic:
by

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

Goal state before:
pp: n : Num
⊢ -n.toZNumNeg = n.toZNum

Tactic:
by

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

Goal state before:
pp: m n : Num
h : m.toZNum = n.toZNum
⊢ m = n

Tactic:
by

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

Goal state before:
pp: m n : Num
⊢ (m + n).toZNum = m.toZNum + n.toZNum

Tactic:
by

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

Goal state before:
pp: n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ ↑zero
⊢ ¬1 ≤ ↑zero

Tactic:
by

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

Goal state before:
pp: n : PosNum
h : 1 < n
⊢ ↑n.pred = (↑n).pred

Tactic:
unfold pred
  cases e : pred' n
  · have : (1 : ℕ) ≤ Nat.pred n := Nat.pred_le_pred ((@cast_lt ℕ _ _ _).2 h)
    rw [← pred'_to_nat, e] at this
    exact absurd this (by decide)
  · rw [← pred'_to_nat, e]
    rfl

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

Goal state before:
pp: n : PosNum
h : 1 < n
⊢ ↑n.pred = (↑n).pred

Tactic:
by

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

Goal state before:
pp: a : PosNum
⊢ a.sub' 1 = a.pred'.toZNum

Tactic:
by

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

Goal state before:
pp: a : PosNum
⊢ sub' 1 a = a.pred'.toZNumNeg

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : PosNum
⊢ ↑(pos p).pred = (↑(pos p)).pred

Tactic:
by

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

Goal state before:
pp: p : PosNum
⊢ castNum <$> (pos p).ppred = (↑(pos p)).ppred

Tactic:
by

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

Goal state before:
pp: m n : Num
⊢ (m.cmp n).swap = n.cmp m

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

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

Tactic:
by

Goal state after: