mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
⊢ ∃ N ⊆ s, N.Finite ∧ IsCover ε s N

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
⊢ ∃ N ⊆ s, N.Finite ∧ IsCover ε s N
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
ε : ℝ≥0
s N : Set X
inst✝ : ProperSpace X
hN : IsClosed N
⊢ s ⊆ ⋃ y ∈ N, closedBall y ↑ε ↔ s ⊆ ⋃ x ∈ N, closedBall x ↑ε

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
hne : ¬x = y
⊢ ↑r + ↑r ≤ ↑(D.packingRadius / 2) + ↑(D.packingRadius / 2)

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
hne : ¬x = y
⊢ ↑r + ↑r ≤ ↑(D.packingRadius / 2) + ↑(D.packingRadius / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case bot
y : EReal
h : ⊥ < y
⊢ ¬y = ⊥

Tactic:
]

Goal state after:
case bot
y : EReal
h : ⊥ < y
⊢ ¬y = ⊥
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case neg
x : ℝ
h_nonpos : ¬x ≤ 0
⊢ ↑(Real.log x) = ↑(Real.log x)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ ↑(Real.log x) = ↑(Real.log x)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
h : ↑a✝ < y
⊢ (↑a✝).exp < y.exp

pp: case top
y : EReal
h : ⊤ < y
⊢ ⊤.exp < y.exp

Tactic:
· induction y
    · simp at h
    · simp_rw [exp_coe]
      exact ENNReal.ofReal_lt_ofReal_iff'.mpr ⟨Real.exp_strictMono (mod_cast h), Real.exp_pos _⟩
    · simp

Goal state after:
case top
y : EReal
h : ⊤ < y
⊢ ⊤.exp < y.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe
a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp a✝)⁻¹ = ENNReal.ofReal (Real.exp a✝)⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp a✝¹ * Real.exp a✝) = ENNReal.ofReal (Real.exp a✝¹ * Real.exp a✝)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe.top
a✝ : ℝ
⊢ ∞ = ∞

pp: case coe.top
a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp a✝) ≠ 0

Tactic:
]

Goal state after:
case coe.top
a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp a✝) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl
y : ℝ≥0∞
⊢ (∞ * y).log = ⊤ + y.log

Tactic:
]

Goal state after:
case inr.inl
y : ℝ≥0∞
⊢ (∞ * y).log = ⊤ + y.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ ∞ = ∞

pp: case top.coe
a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp a✝) ≠ 0

Tactic:
]

Goal state after:
case top.coe
a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp a✝) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl.inl
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case coe
a✝ : ℝ
⊢ ↑a✝ = ↑a✝

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case neg
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : ¬x = 0
hx_pos : 0 < x.toReal
⊢ ENNReal.ofReal x.toReal = ENNReal.ofReal x.toReal

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : EReal
y : ℝ
⊢ ↑y * x = ↑y * x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ x ^ y = x ^ y

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (if y = 0 then 0 else ∞) = ∞

Tactic:
]

Goal state after:
case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (if y = 0 then 0 else ∞) = ∞
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * y).log = ↑(Real.log x.toReal) + y.log

Tactic:
]

Goal state after:
case inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * y).log = ↑(Real.log x.toReal) + y.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case e'_5
b : ℝ≥0∞
hb : 1 < b
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case e'_5
b : ℝ≥0∞
hb : b < 1
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < x.toReal * y.toReal

Tactic:
]

Goal state after:
case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < x.toReal * y.toReal
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case e'_5
b : ℝ≥0∞
hb : 1 < b
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case e'_5
b : ℝ≥0∞
hb : b < 1
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inl.inr.inl
y : ℝ
y_neg : y < 0
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, u a / ↑a ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n

Tactic:
]

Goal state after:
u : ℕ → EReal
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, u a / ↑a ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : 1 ≤ n
⊢ u n ≤ b * ↑n ↔ u n ≤ b * ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ u a / ↑a) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * ↑n ≤ u n

Tactic:
]

Goal state after:
u : ℕ → EReal
a : EReal
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ u a / ↑a) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * ↑n ≤ u n
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ ⊥ = ⊥

pp: case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y

Tactic:
]

Goal state after:
case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : 1 ≤ n
⊢ b * ↑n ≤ u n ↔ b * ↑n ≤ u n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ ⊤ = ⊤

pp: case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y

Tactic:
]

Goal state after:
case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, u a / ↑a ≤ y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n

Tactic:
]

Goal state after:
u : ℕ → EReal
a : EReal
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, u a / ↑a ≤ y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ≥0∞
n : ℕ
⊢ ↑n * x.log = ↑n * x.log

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ u a / ↑a) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, b * ↑n ≤ u n

Tactic:
]

Goal state after:
u : ℕ → EReal
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ u a / ↑a) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, b * ↑n ≤ u n
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ⊢ linearGrowthSup ⊥ = limsup (fun x ↦ ⊥) atTop

Tactic:
]

Goal state after:
⊢ linearGrowthSup ⊥ = limsup (fun x ↦ ⊥) atTop
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ⊢ linearGrowthInf ⊥ ≤ linearGrowthSup ⊥

Tactic:
]

Goal state after:
⊢ linearGrowthInf ⊥ ≤ linearGrowthSup ⊥
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ⊢ linearGrowthInf ⊤ = liminf (fun x ↦ ⊤) atTop

Tactic:
]

Goal state after:
⊢ linearGrowthInf ⊤ = liminf (fun x ↦ ⊤) atTop
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ⊢ linearGrowthInf ⊤ ≤ linearGrowthSup ⊤

Tactic:
]

Goal state after:
⊢ linearGrowthInf ⊤ ≤ linearGrowthSup ⊤
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : ↑a < linearGrowthInf u
⊢ ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → ↑M < ↑a * ↑b

Tactic:
]

Goal state after:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : ↑a < linearGrowthInf u
⊢ ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → ↑M < ↑a * ↑b
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : ↑a < linearGrowthInf u
n : ℕ
hn : M / a ≤ ↑n
k : ℕ
k_n : n + 1 ≤ k
⊢ M < ↑k * a

Tactic:
]

Goal state after:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : ↑a < linearGrowthInf u
n : ℕ
hn : M / a ≤ ↑n
k : ℕ
k_n : n + 1 ≤ k
⊢ M < ↑k * a
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
n : ℕ
⊢ (u n + v n) / ↑n = (u n + v n) / ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf v ≠ ⊥
n : ℕ
⊢ (u n + v n) / ↑n = (u n + v n) / ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthInf (v + u) ≤ linearGrowthSup v + linearGrowthInf u

Tactic:
]

Goal state after:
u v : ℕ → EReal
h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthInf (v + u) ≤ linearGrowthSup v + linearGrowthInf u
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
n : ℕ
⊢ u n / ↑n + v n / ↑n = u n / ↑n + v n / ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ linearGrowthSup v + linearGrowthInf u ≤ linearGrowthSup (v + u)

Tactic:
]

Goal state after:
u v : ℕ → EReal
⊢ linearGrowthSup v + linearGrowthInf u ≤ linearGrowthSup (v + u)
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
n : ℕ
⊢ u n / ↑n + v n / ↑n = u n / ↑n + v n / ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
⊢ linearGrowthInf (-u) = liminf (-fun n ↦ u n / ↑n) atTop

Tactic:
]

Goal state after:
u : ℕ → EReal
⊢ linearGrowthInf (-u) = liminf (-fun n ↦ u n / ↑n) atTop
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
n : ℕ
⊢ -u n * (↑n)⁻¹ = -u n * (↑n)⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
⊢ linearGrowthSup (-u) = limsup (-fun n ↦ u n / ↑n) atTop

Tactic:
]

Goal state after:
u : ℕ → EReal
⊢ linearGrowthSup (-u) = limsup (-fun n ↦ u n / ↑n) atTop
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, (u a).log / ↑a ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * ↑n).exp

Tactic:
]

Goal state after:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, (u a).log / ↑a ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * ↑n).exp
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : 1 ≤ n
⊢ (u n).log ≤ (b * ↑n).exp.log ↔ u n ≤ (b * ↑n).exp

Tactic:
]

Goal state after:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : 1 ≤ n
⊢ (u n).log ≤ (b * ↑n).exp.log ↔ u n ≤ (b * ↑n).exp
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v + 0 = linearGrowthInf v

Tactic:
]

Goal state after:
case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v + 0 = linearGrowthInf v
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ 0 ≠ ⊤

Tactic:
]

Goal state after:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ 0 ≠ ⊤
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ 0 ≠ ⊥

Tactic:
]

Goal state after:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ 0 ≠ ⊥
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ (u a).log / ↑a) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * ↑n).exp ≤ u n

Tactic:
]

Goal state after:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ (u a).log / ↑a) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * ↑n).exp ≤ u n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : 1 ≤ n
⊢ (b * ↑n).exp.log ≤ (u n).log ↔ (b * ↑n).exp ≤ u n

Tactic:
]

Goal state after:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : 1 ≤ n
⊢ (b * ↑n).exp.log ≤ (u n).log ↔ (b * ↑n).exp ≤ u n
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst✝ : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
⊢ s ⊆ (s \ ⋃ p ∈ h.index, h.covering p) ∪ ⋃ p ∈ h.index, h.covering p

Tactic:
by simp only [subset_union_left, sdiff_union_self]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, (u a).log / ↑a ≤ y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ (b * ↑n).exp

Tactic:
]

Goal state after:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, (u a).log / ↑a ≤ y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ (b * ↑n).exp
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ ∀ (n : ℕ), Tendsto (fun a ↦ |k a ^ n * g a|) l (𝓝 0)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ ∀ (n : ℕ), Tendsto (fun a ↦ |k a ^ n * g a|) l (𝓝 0)
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst✝ : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
⊢ ∑' (p : ↑h.index), ρ (h.covering ↑p) = ∑' (p : ↑h.index), ρ (h.covering ↑p)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v + 0 = linearGrowthSup v

Tactic:
]

Goal state after:
case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v + 0 = linearGrowthSup v
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊥ ∨ 0 ≠ ⊤

Tactic:
]

Goal state after:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊥ ∨ 0 ≠ ⊤
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊤ ∨ 0 ≠ ⊥

Tactic:
]

Goal state after:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊤ ∨ 0 ≠ ⊥
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a ↦ |k a ^ (z + 1) * f a|) l, (fun x1 x2 ↦ x1 ≤ x2) x m
h1 : Tendsto (fun x ↦ 0) l (𝓝 0)
h2 : Tendsto (fun a ↦ |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun x1 x2 ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|

Tactic:
← abs_mul,

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a ↦ |k a ^ (z + 1) * f a|) l, (fun x1 x2 ↦ x1 ≤ x2) x m
h1 : Tendsto (fun x ↦ 0) l (𝓝 0)
h2 : Tendsto (fun a ↦ |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun x1 x2 ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |(k x)⁻¹ * (k x ^ (z + 1) * f x)|
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ (u a).log / ↑a) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * ↑n).exp ≤ u n

Tactic:
]

Goal state after:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ (u a).log / ↑a) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * ↑n).exp ≤ u n
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a ↦ |k a ^ (z + 1) * f a|) l, (fun x1 x2 ↦ x1 ≤ x2) x m
h1 : Tendsto (fun x ↦ 0) l (𝓝 0)
h2 : Tendsto (fun a ↦ |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun x1 x2 ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |k x ^ z * f x|

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ ∀ (z_1 : ℤ), Tendsto (fun a ↦ k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ ∀ (z_1 : ℤ), Tendsto (fun a ↦ k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ liminf (fun n ↦ (u ⊓ v) n / ↑n) atTop = liminf (fun a ↦ min (u a / ↑a) (v a / ↑a)) atTop

Tactic:
]

Goal state after:
u v : ℕ → EReal
⊢ liminf (fun n ↦ (u ⊓ v) n / ↑n) atTop = liminf (fun a ↦ min (u a / ↑a) (v a / ↑a)) atTop
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → EReal
⊢ ⨅ x, linearGrowthInf (u x) = ⨅ i, linearGrowthInf (u i)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ limsup (fun n ↦ (u ⊔ v) n / ↑n) atTop = limsup (fun a ↦ max (u a / ↑a) (v a / ↑a)) atTop

Tactic:
]

Goal state after:
u v : ℕ → EReal
⊢ limsup (fun n ↦ (u ⊔ v) n / ↑n) atTop = limsup (fun a ↦ max (u a / ↑a) (v a / ↑a)) atTop
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → EReal
⊢ ⨆ x, linearGrowthSup (u x) = ⨆ i, linearGrowthSup (u i)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: a b : ℝ
h : a < b
x : ℝ
ab_x : a * x + 1 ≤ b * x
⊢ ∃ n, a * x ≤ ↑n ∧ ↑n ≤ b * x

Tactic:
]

Goal state after:
a b : ℝ
h : a < b
x : ℝ
ab_x : a * x + 1 ≤ b * x
⊢ ∃ n, a * x ≤ ↑n ∧ ↑n ≤ b * x
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case refine_1
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ ⊥ * ↑n ≤ 0

Tactic:
]

Goal state after:
case refine_1
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ ⊥ * ↑n ≤ 0
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case refine_2
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ 0 ≤ b * ↑n

Tactic:
]

Goal state after:
case refine_2
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ 0 ≤ b * ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: ⊢ linearGrowthSup (log ∘ 0) = linearGrowthSup ⊥

Tactic:
]

Goal state after:
⊢ linearGrowthSup (log ∘ 0) = linearGrowthSup ⊥
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a ↦ k a ^ z)⁻¹ = fun a ↦ k a ^ (-z)
⊢ Tendsto ((fun a ↦ k a ^ (-z)) * f) l (𝓝 0)

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a ↦ k a ^ z)⁻¹ = fun a ↦ k a ^ (-z)
⊢ Tendsto ((fun a ↦ k a ^ (-z)) * f) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: x✝ : ℕ
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: ⊢ expGrowthSup 0 = ⊥

Tactic:
rw [← linearGrowthSup_bot, expGrowthSup_def]
  congr 1
  ext _
  rw [comp_apply, Pi.zero_apply, Pi.bot_apply, log_zero]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: ⊢ expGrowthInf 0 ≤ expGrowthSup 0

Tactic:
]

Goal state after:
⊢ expGrowthInf 0 ≤ expGrowthSup 0
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ (linearGrowthInf fun x ↦ 0) ≤ linearGrowthInf (u ∘ v)

Tactic:
]

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ (linearGrowthInf fun x ↦ 0) ≤ linearGrowthInf (u ∘ v)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: ⊢ linearGrowthInf (log ∘ ⊤) = linearGrowthInf ⊤

Tactic:
]

Goal state after:
⊢ linearGrowthInf (log ∘ ⊤) = linearGrowthInf ⊤