awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
hb : Ne (α := ℝ≥0∞) ∞ 0
h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n
⊢ expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ ∞) + expGrowthSup u

Tactic:
expGrowthInf_top ▸ le_add_of_nonneg_left le_top

Premises used: Eq.rec, le_top, ExpGrowth.expGrowthInf_top, Eq.symm, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
hb : Ne (α := ℝ≥0∞) ∞ 0
h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n
⊢ expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ ∞) + expGrowthSup u

Tactic:
exact expGrowthInf_top ▸ le_add_of_nonneg_left le_top
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
b_top : b < ∞
inr : expGrowthSup u ≤ 0 + expGrowthSup u
inr₁ inr₂ : expGrowthSup u ≤ expGrowthSup u
⊢ expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthSup u

Tactic:
rw [expGrowthInf_const hb b_top.ne, zero_add]

Premises used: zero_add, ExpGrowth.expGrowthInf_const, LT.lt.ne
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
rw :
  Eq (α := EReal) (liminf (fun (n : ℕ) ↦ ((u ⊓ v) n).log / (↑n : EReal)) atTop)
    (liminf (fun (a : ℕ) ↦ min ((u a).log / (↑a : EReal)) ((v a).log / (↑a : EReal))) atTop)
⊢ expGrowthInf (u ⊓ v) = min (expGrowthInf u) (expGrowthInf v)

Tactic:
rw [expGrowthInf, expGrowthInf, expGrowthInf, ← liminf_min]

Premises used: ExpGrowth.expGrowthInf, liminf_min
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
⊢ Eq (α := EReal) (liminf (fun (n : ℕ) ↦ ((u ⊓ v) n).log / (↑n : EReal)) atTop)
    (liminf (fun (a : ℕ) ↦ min ((u a).log / (↑a : EReal)) ((v a).log / (↑a : EReal))) atTop)

Tactic:
liminf_congr (Eventually.of_forall fun n ↦ ?_)

Premises used: Filter.Eventually.of_forall, Filter.liminf_congr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
refine : ∀ (n : ℕ), ((u ⊓ v) n).log / (↑n : EReal) = min ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))
⊢ Eq (α := EReal) (liminf (fun (n : ℕ) ↦ ((u ⊓ v) n).log / (↑n : EReal)) atTop)
    (liminf (fun (a : ℕ) ↦ min ((u a).log / (↑a : EReal)) ((v a).log / (↑a : EReal))) atTop)

Tactic:
refine liminf_congr (Eventually.of_forall fun n ↦ ?_)

Premises used: Filter.Eventually.of_forall, Filter.liminf_congr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
rw : min (u n).log (v n).log / (↑n : EReal) = min ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))
⊢ ((u ⊓ v) n).log / (↑n : EReal) = min ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))

Tactic:
rw [Pi.inf_apply, log_monotone.map_min]

Premises used: ENNReal.log_monotone, Monotone.map_min, Pi.inf_apply
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ min (u n).log (v n).log / (↑n : EReal) = min ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))

Tactic:
(monotone_div_right_of_nonneg n.cast_nonneg').map_min

Premises used: Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg, Monotone.map_min
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ min (u n).log (v n).log / (↑n : EReal) = min ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))

Tactic:
exact (monotone_div_right_of_nonneg n.cast_nonneg').map_min

Premises used: Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg, Monotone.map_min
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
⊢ Eq (α := EReal) ((expGrowthInfTopHom : (a : ℕ → ℝ≥0∞) → EReal) (hs.toFinset (s := s).inf u) : EReal)
    (hs.toFinset (s := s).inf ((⇑expGrowthInfTopHom : (a : ℕ → ℝ≥0∞) → EReal) ∘ u) : EReal)

Tactic:
have := map_finset_inf expGrowthInfTopHom hs.toFinset u
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
this :
  Eq (α := EReal) ((expGrowthInfTopHom : (a : ℕ → ℝ≥0∞) → EReal) (hs.toFinset (s := s).inf u) : EReal)
    (hs.toFinset (s := s).inf ((⇑expGrowthInfTopHom : (a : ℕ → ℝ≥0∞) → EReal) ∘ u) : EReal)
⊢ expGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, expGrowthInf (u x)

Tactic:
simpa only [expGrowthInfTopHom, InfTopHom.coe_mk, InfHom.coe_mk, Finset.inf_eq_iInf,
    hs.mem_toFinset, comp_apply]

Premises used: ExpGrowth.expGrowthInfTopHom, Set.Finite.mem_toFinset, InfHom.coe_mk, InfTopHom.coe_mk, Finset.inf_eq_iInf, Function.comp_apply
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → ℝ≥0∞
rw : expGrowthInf (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), u x) = ⨅ (i : ι), expGrowthInf (u i)
rw₁ :
  Eq (α := EReal) (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), expGrowthInf (u x))
    (⨅ (i : ι), expGrowthInf (u i))
rw₂ rw₃ : Eq (α := EReal) (⨅ (x : ι), expGrowthInf (u x)) (⨅ (i : ι), expGrowthInf (u i))
⊢ expGrowthInf (⨅ (i : ι), u i) = ⨅ (i : ι), expGrowthInf (u i)

Tactic:
rw [← iInf_univ, expGrowthInf_biInf u Set.finite_univ, iInf_univ]

Premises used: Set.finite_univ, ExpGrowth.expGrowthInf_biInf, iInf_univ
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
rw :
  Eq (α := EReal) (limsup (fun (n : ℕ) ↦ ((u ⊔ v) n).log / (↑n : EReal)) atTop)
    (limsup (fun (a : ℕ) ↦ max ((u a).log / (↑a : EReal)) ((v a).log / (↑a : EReal))) atTop)
⊢ expGrowthSup (u ⊔ v) = max (expGrowthSup u) (expGrowthSup v)

Tactic:
rw [expGrowthSup, expGrowthSup, expGrowthSup, ← limsup_max]

Premises used: limsup_max, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
⊢ Eq (α := EReal) (limsup (fun (n : ℕ) ↦ ((u ⊔ v) n).log / (↑n : EReal)) atTop)
    (limsup (fun (a : ℕ) ↦ max ((u a).log / (↑a : EReal)) ((v a).log / (↑a : EReal))) atTop)

Tactic:
limsup_congr (Eventually.of_forall fun n ↦ ?_)

Premises used: Filter.Eventually.of_forall, Filter.limsup_congr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
refine : ∀ (n : ℕ), ((u ⊔ v) n).log / (↑n : EReal) = max ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))
⊢ Eq (α := EReal) (limsup (fun (n : ℕ) ↦ ((u ⊔ v) n).log / (↑n : EReal)) atTop)
    (limsup (fun (a : ℕ) ↦ max ((u a).log / (↑a : EReal)) ((v a).log / (↑a : EReal))) atTop)

Tactic:
refine limsup_congr (Eventually.of_forall fun n ↦ ?_)

Premises used: Filter.Eventually.of_forall, Filter.limsup_congr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
rw : max (u n).log (v n).log / (↑n : EReal) = max ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))
⊢ ((u ⊔ v) n).log / (↑n : EReal) = max ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))

Tactic:
rw [Pi.sup_apply, log_monotone.map_max]

Premises used: Monotone.map_max, ENNReal.log_monotone, Pi.sup_apply
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ max (u n).log (v n).log / (↑n : EReal) = max ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))

Tactic:
(monotone_div_right_of_nonneg n.cast_nonneg').map_max

Premises used: Monotone.map_max, Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ max (u n).log (v n).log / (↑n : EReal) = max ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))

Tactic:
exact (monotone_div_right_of_nonneg n.cast_nonneg').map_max

Premises used: Monotone.map_max, Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
⊢ Eq (α := EReal) ((expGrowthSupBotHom : (a : ℕ → ℝ≥0∞) → EReal) (hs.toFinset (s := s).sup u) : EReal)
    (hs.toFinset (s := s).sup ((⇑expGrowthSupBotHom : (a : ℕ → ℝ≥0∞) → EReal) ∘ u) : EReal)

Tactic:
have := map_finset_sup expGrowthSupBotHom hs.toFinset u
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
this :
  Eq (α := EReal) ((expGrowthSupBotHom : (a : ℕ → ℝ≥0∞) → EReal) (hs.toFinset (s := s).sup u) : EReal)
    (hs.toFinset (s := s).sup ((⇑expGrowthSupBotHom : (a : ℕ → ℝ≥0∞) → EReal) ∘ u) : EReal)
⊢ expGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Tactic:
simpa only [expGrowthSupBotHom, SupBotHom.coe_mk, SupHom.coe_mk, Finset.sup_eq_iSup,
    hs.mem_toFinset, comp_apply]

Premises used: Set.Finite.mem_toFinset, Finset.sup_eq_iSup, ExpGrowth.expGrowthSupBotHom, SupHom.coe_mk, Function.comp_apply, SupBotHom.coe_mk
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → ℝ≥0∞
rw : expGrowthSup (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), u x) = ⨆ (i : ι), expGrowthSup (u i)
rw₁ :
  Eq (α := EReal) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), expGrowthSup (u x))
    (⨆ (i : ι), expGrowthSup (u i))
rw₂ rw₃ : Eq (α := EReal) (⨆ (x : ι), expGrowthSup (u x)) (⨆ (i : ι), expGrowthSup (u i))
⊢ expGrowthSup (⨆ (i : ι), u i) = ⨆ (i : ι), expGrowthSup (u i)

Tactic:
rw [← iSup_univ, expGrowthSup_biSup u Set.finite_univ, iSup_univ]

Premises used: ExpGrowth.expGrowthSup_biSup, iSup_univ, Set.finite_univ
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
⊢ max (expGrowthInf u) (expGrowthInf v) ≤ expGrowthInf (u + v)

Tactic:
sup_le (expGrowthInf_monotone le_self_add) (expGrowthInf_monotone le_add_self)

Premises used: ExpGrowth.expGrowthInf_monotone, sup_le, le_self_add, le_add_self
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
rw : expGrowthSup (u + v) = expGrowthSup (u ⊔ v)
⊢ expGrowthSup (u + v) = max (expGrowthSup u) (expGrowthSup v)

Tactic:
rw [← expGrowthSup_sup]

Premises used: ExpGrowth.expGrowthSup_sup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
a : expGrowthSup (u + v) ≤ expGrowthSup (u ⊔ v)
a₁ : expGrowthSup (u ⊔ v) ≤ expGrowthSup (u + v)
⊢ expGrowthSup (u + v) = expGrowthSup (u ⊔ v)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u + v) ≤ expGrowthSup (u ⊔ v)

Tactic:
expGrowthSup_le_of_eventually_le (b := 2) ofNat_ne_top (Eventually.of_forall fun n ↦ ?_)

Premises used: ENNReal.ofNat_ne_top, Filter.Eventually.of_forall, ExpGrowth.expGrowthSup_le_of_eventually_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
a : ∀ (n : ℕ), (u + v) n ≤ 2 * (u ⊔ v) n
⊢ expGrowthSup (u + v) ≤ expGrowthSup (u ⊔ v)

Tactic:
refine expGrowthSup_le_of_eventually_le (b := 2) ofNat_ne_top (Eventually.of_forall fun n ↦ ?_)

Premises used: ENNReal.ofNat_ne_top, Filter.Eventually.of_forall, ExpGrowth.expGrowthSup_le_of_eventually_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
a : u n + v n ≤ max (u n) (v n) + max (u n) (v n)
⊢ (u + v) n ≤ 2 * (u ⊔ v) n

Tactic:
rw [Pi.sup_apply u v n, Pi.add_apply u v n, two_mul]

Premises used: two_mul, Pi.add_apply, Pi.sup_apply
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ u n + v n ≤ max (u n) (v n) + max (u n) (v n)

Tactic:
add_le_add (le_max_left (u n) (v n)) (le_max_right (u n) (v n))

Premises used: le_max_right, add_le_add, le_max_left
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ u n + v n ≤ max (u n) (v n) + max (u n) (v n)

Tactic:
exact add_le_add (le_max_left (u n) (v n)) (le_max_right (u n) (v n))

Premises used: le_max_right, add_le_add, le_max_left
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u ⊔ v) ≤ expGrowthSup (u + v)

Tactic:
expGrowthSup_monotone fun n ↦ ?_

Premises used: ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
a : ∀ (n : ℕ), (u ⊔ v) n ≤ (u + v) n
⊢ expGrowthSup (u ⊔ v) ≤ expGrowthSup (u + v)

Tactic:
refine expGrowthSup_monotone fun n ↦ ?_

Premises used: ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u ⊔ v) n ≤ (u + v) n

Tactic:
sup_le (self_le_add_right (u n) (v n)) (self_le_add_left (v n) (u n))

Premises used: self_le_add_right, self_le_add_left, sup_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u ⊔ v) n ≤ (u + v) n

Tactic:
exact sup_le (self_le_add_right (u n) (v n)) (self_le_add_left (v n) (u n))

Premises used: self_le_add_right, self_le_add_left, sup_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
empty : expGrowthSup 0 = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
empty₁ : expGrowthSup 0 = ⨆ x ∈ (↑∅ : Set α), expGrowthSup (u x)
empty₂ : expGrowthSup 0 = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ x), expGrowthSup (u x)
empty₃ : expGrowthSup 0 = ⊥
empty₄ empty₅ : Eq (α := EReal) ⊥ ⊥
⊢ expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)

Tactic:
rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
    expGrowthSup_zero]

Premises used: Finset.coe_empty, Finset.iSup_coe, ExpGrowth.expGrowthSup_zero, iSup_emptyset, Finset.sum_empty
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
a : α
t : Finset α
a_t : a ∉ t
ha : expGrowthSup (∑ x ∈ t, u x) = ⨆ x ∈ t, expGrowthSup (u x)
insert : expGrowthSup (u a + ∑ x ∈ t, u x) = ⨆ x ∈ Insert.insert a t, expGrowthSup (u x)
insert₁ : max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ t, u x)) = ⨆ x ∈ Insert.insert a t, expGrowthSup (u x)
insert₂ :
  max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ t, u x)) = ⨆ x ∈ (↑(Insert.insert a t) : Set α), expGrowthSup (u x)
insert₃ :
  max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ t, u x)) = ⨆ x ∈ Insert.insert a (↑t : Set α), expGrowthSup (u x)
insert₄ :
  max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ t, u x)) =
    max (expGrowthSup (u a)) (⨆ x ∈ (↑t : Set α), expGrowthSup (u x))
insert₅ :
  max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ t, u x)) = max (expGrowthSup (u a)) (⨆ x ∈ t, expGrowthSup (u x))
insert₆ insert₇ :
  max (expGrowthSup (u a)) (⨆ x ∈ t, expGrowthSup (u x)) = max (expGrowthSup (u a)) (⨆ x ∈ t, expGrowthSup (u x))
⊢ expGrowthSup (∑ x ∈ Insert.insert a t, u x) = ⨆ x ∈ Insert.insert a t, expGrowthSup (u x)

Tactic:
rw [Finset.sum_insert a_t, expGrowthSup_add, ← Finset.iSup_coe,
    Finset.coe_insert a t, iSup_insert, Finset.iSup_coe, ha]

Premises used: iSup_insert, ExpGrowth.expGrowthSup_add, Finset.iSup_coe, Finset.sum_insert, Finset.coe_insert
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Finset α
empty : expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
insert :
  ∀ (a : α) (t : Finset α) (a_t : a ∉ t) (ha : expGrowthSup (∑ x ∈ t, u x) = ⨆ x ∈ t, expGrowthSup (u x)),
    expGrowthSup (∑ x ∈ Insert.insert a t, u x) = ⨆ x ∈ Insert.insert a t, expGrowthSup (u x)
⊢ expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Tactic:
induction s using Finset.induction_on with
  | empty => rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
    expGrowthSup_zero]
  | insert a t a_t ha => rw [Finset.sum_insert a_t, expGrowthSup_add, ← Finset.iSup_coe,
    Finset.coe_insert a t, iSup_insert, Finset.iSup_coe, ha]

Premises used: iSup_insert, Finset.coe_empty, ExpGrowth.expGrowthSup_add, Finset.iSup_coe, Insert.insert, ExpGrowth.expGrowthSup_zero, iSup_emptyset, Finset.sum_empty
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Finset α
empty : expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
insert :
  ∀ (a : α) (t : Finset α) (a_t : a ∉ t) (ha : expGrowthSup (∑ x ∈ t, u x) = ⨆ x ∈ t, expGrowthSup (u x)),
    expGrowthSup (∑ x ∈ Insert.insert a t, u x) = ⨆ x ∈ Insert.insert a t, expGrowthSup (u x)
⊢ expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
    expGrowthSup_zero]
  | insert a t a_t ha => rw [Finset.sum_insert a_t, expGrowthSup_add, ← Finset.iSup_coe,
    Finset.coe_insert a t, iSup_insert, Finset.iSup_coe, ha]

Premises used: iSup_insert, Finset.coe_empty, ExpGrowth.expGrowthSup_add, Finset.iSup_coe, Insert.insert, ExpGrowth.expGrowthSup_zero, iSup_emptyset, Finset.sum_empty
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : 1 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
apply : ∀ (n : ℕ) (h : 1 n ≤ u n), 0 n ≤ (u n).log
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * expGrowthInf u ≤ expGrowthInf (u ∘ v)

Tactic:
apply le_linearGrowthInf_comp (hu.mono fun n h ↦ ?_) hv

Premises used: Filter.Eventually.mono, LinearGrowth.le_linearGrowthInf_comp
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : 1 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
n : ℕ
h : 1 n ≤ u n
⊢ 1 ≤ u n

Tactic:
rw [Pi.one_apply] at h

Premises used: Pi.one_apply
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : 1 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
n : ℕ
h : 1 ≤ u n
rwa : 0 ≤ (u n).log
rwa₁ rwa₂ rwa₃ rwa₄ : 1 ≤ u n
⊢ 0 n ≤ (u n).log

Tactic:
rwa [Pi.zero_apply, zero_le_log_iff]

Premises used: Pi.zero_apply, ENNReal.zero_le_log_iff
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 1 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
apply : ∀ (n : ℕ) (h : 1 ≤ u n), 0 ≤ (log ∘ u) n
⊢ expGrowthSup (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * expGrowthSup u

Tactic:
apply linearGrowthSup_comp_le (u := log ∘ u) (hu.mono fun n h ↦ ?_) hv₀ hv₁ hv₂

Premises used: Filter.Frequently.mono, LinearGrowth.linearGrowthSup_comp_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 1 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
n : ℕ
h : 1 ≤ u n
rwa : 0 ≤ (u n).log
rwa₁ rwa₂ rwa₃ rwa₄ : 1 ≤ u n
⊢ 0 ≤ (log ∘ u) n

Tactic:
rwa [comp_apply, zero_le_log_iff]

Premises used: ENNReal.zero_le_log_iff, Function.comp_apply
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
h : Monotone u
h' : u ≠ 0
apply : log ∘ u ≠ ⊥
⊢ 0 ≤ expGrowthInf u

Tactic:
apply (log_monotone.comp h).linearGrowthInf_nonneg

Premises used: Monotone.comp, ENNReal.log_monotone, Monotone.linearGrowthInf_nonneg
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
h : Monotone u
h' : u ≠ 0
simp : ∀ (h' : ¬∀ (x : ℕ), u x = 0), ¬∀ (x : ℕ), u x = 0
⊢ log ∘ u ≠ ⊥

Tactic:
simp only [ne_eq, funext_iff, comp_apply, Pi.bot_apply, log_eq_bot_iff, Pi.zero_apply] at h' ⊢

Premises used: ENNReal.log_eq_bot_iff, funext_iff, Pi.zero_apply, Pi.bot_apply, ne_eq, Function.comp_apply
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
h : Monotone u
h' : ¬∀ (x : ℕ), u x = 0
⊢ ¬∀ (x : ℕ), u x = 0

Tactic:
h'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
h : Monotone u
h' : ¬∀ (x : ℕ), u x = 0
⊢ ¬∀ (x : ℕ), u x = 0

Tactic:
exact h'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
h : Monotone u
h' : u ≠ 0
⊢ 0 ≤ expGrowthSup u

Tactic:
(h.expGrowthInf_nonneg h').trans expGrowthInf_le_expGrowthSup

Premises used: Monotone.expGrowthInf_nonneg, LE.le.trans, ExpGrowth.expGrowthInf_le_expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
h : Monotone u
h' : u ≠ 0
hv : Tendsto v atTop atTop
apply : log ∘ u ≠ ⊥
⊢ 0 ≤ expGrowthInf (u ∘ v)

Tactic:
apply linearGrowthInf_comp_nonneg (u := log ∘ u) (log_monotone.comp h) _ hv

Premises used: Monotone.comp, ENNReal.log_monotone, LinearGrowth.linearGrowthInf_comp_nonneg
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
h : Monotone u
h' : u ≠ 0
hv : Tendsto v atTop atTop
simp : ∀ (h' : ¬∀ (x : ℕ), u x = 0), ¬∀ (x : ℕ), u x = 0
⊢ log ∘ u ≠ ⊥

Tactic:
simp only [ne_eq, funext_iff, comp_apply, Pi.bot_apply, log_eq_bot_iff, Pi.zero_apply] at h' ⊢

Premises used: ENNReal.log_eq_bot_iff, funext_iff, Pi.zero_apply, Pi.bot_apply, ne_eq, Function.comp_apply
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
h' : ¬∀ (x : ℕ), u x = 0
⊢ ¬∀ (x : ℕ), u x = 0

Tactic:
h'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
h' : ¬∀ (x : ℕ), u x = 0
⊢ ¬∀ (x : ℕ), u x = 0

Tactic:
exact h'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
h : Monotone u
h' : u ≠ 0
hv : Tendsto v atTop atTop
⊢ 0 ≤ expGrowthSup (u ∘ v)

Tactic:
(expGrowthInf_comp_nonneg h h' hv).trans expGrowthInf_le_expGrowthSup

Premises used: ExpGrowth.expGrowthInf_comp_nonneg, LE.le.trans, ExpGrowth.expGrowthInf_le_expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
⊢ expGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * expGrowthInf u

Tactic:
(log_monotone.comp h).linearGrowthInf_comp_le hv₀ hv₁

Premises used: ExpGrowth.expGrowthInf, ENNReal.log, Monotone.comp, ENNReal.log_monotone, LinearGrowth.linearGrowthInf, Monotone.linearGrowthInf_comp_le, ite
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * expGrowthSup u ≤ expGrowthSup (u ∘ v)

Tactic:
(log_monotone.comp h).le_linearGrowthSup_comp hv

Premises used: ENNReal.log, Monotone.comp, ENNReal.log_monotone, LinearGrowth.linearGrowthSup, Monotone.le_linearGrowthSup_comp, ExpGrowth.expGrowthSup, ite
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ expGrowthInf (u ∘ v) = a * expGrowthInf u

Tactic:
(log_monotone.comp h).linearGrowthInf_comp hv ha ha'

Premises used: ExpGrowth.expGrowthInf, ENNReal.log, Monotone.comp, ENNReal.log_monotone, LinearGrowth.linearGrowthInf, Monotone.linearGrowthInf_comp, ite
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ expGrowthSup (u ∘ v) = a * expGrowthSup u

Tactic:
(log_monotone.comp h).linearGrowthSup_comp hv ha ha'

Premises used: ENNReal.log, Monotone.comp, ENNReal.log_monotone, LinearGrowth.linearGrowthSup, Monotone.linearGrowthSup_comp, ExpGrowth.expGrowthSup, ite
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
m : ℕ
h : Monotone u
hm : m ≠ 0
⊢ (expGrowthInf fun (n : ℕ) ↦ u (m * n)) = (↑m : EReal) * expGrowthInf u

Tactic:
(log_monotone.comp h).linearGrowthInf_comp_mul hm

Premises used: ExpGrowth.expGrowthInf, ENNReal.log, Monotone.comp, ENNReal.log_monotone, LinearGrowth.linearGrowthInf, Monotone.linearGrowthInf_comp_mul, ite
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
m : ℕ
h : Monotone u
hm : m ≠ 0
⊢ (expGrowthSup fun (n : ℕ) ↦ u (m * n)) = (↑m : EReal) * expGrowthSup u

Tactic:
(log_monotone.comp h).linearGrowthSup_comp_mul hm

Premises used: ENNReal.log, Monotone.comp, ENNReal.log_monotone, LinearGrowth.linearGrowthSup, Monotone.linearGrowthSup_comp_mul, ExpGrowth.expGrowthSup, ite
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
s : Set α
rw : (∀ᶠ (x : α) in 𝓟 s, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
rw₁ rw₂ : (∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
⊢ IsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [IsBigOWith_def, eventually_principal]

Premises used: Asymptotics.IsBigOWith_def, Filter.eventually_principal