awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
⊢ expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthSup u
have inl : ∀ (hb : Ne (α := ℝ≥0∞) ∞ 0) (h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n),
  expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ ∞) + expGrowthSup u
Tactic: rcases eq_top_or_lt_top b with rfl | b_top
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
inl :
  ∀ (hb : Ne (α := ℝ≥0∞) ∞ 0) (h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n),
    expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ ∞) + expGrowthSup u
⊢ expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthSup u
have inr : ∀ (b_top : b < ∞), expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthSup u
Tactic: rcases eq_top_or_lt_top b with rfl | b_top
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
b_top : b < ∞
⊢ expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthSup u
have inr : expGrowthSup u ≤ 0 + expGrowthSup u
Tactic: rw [expGrowthInf_const hb b_top.ne, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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
⊢ expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthSup u
have inr₁ : expGrowthSup u ≤ expGrowthSup u
Tactic: rw [expGrowthInf_const hb b_top.ne, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthInf (u ⊓ v) = min (expGrowthInf u) (expGrowthInf v)
have 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)
Tactic: rw [expGrowthInf, expGrowthInf, expGrowthInf, ← liminf_min]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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)
have refine : ∀ (n : ℕ), ((u ⊓ v) n).log / (↑n : EReal) = min ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))
Tactic: refine liminf_congr (Eventually.of_forall fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u ⊓ v) n).log / (↑n : EReal) = min ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))
have rw : min (u n).log (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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (hypothesis)
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
⊢ expGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, expGrowthInf (u x)
have 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)
Tactic: have := map_finset_inf expGrowthInfTopHom hs.toFinset u
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → ℝ≥0∞
⊢ expGrowthInf (⨅ (i : ι), u i) = ⨅ (i : ι), expGrowthInf (u i)
have rw : expGrowthInf (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), u x) = ⨅ (i : ι), expGrowthInf (u i)
Tactic: rw [← iInf_univ, expGrowthInf_biInf u Set.finite_univ, iInf_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → ℝ≥0∞
rw : expGrowthInf (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), u x) = ⨅ (i : ι), expGrowthInf (u i)
⊢ expGrowthInf (⨅ (i : ι), u i) = ⨅ (i : ι), expGrowthInf (u i)
have rw₁ : Eq (α := EReal) (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), expGrowthInf (u x))
  (⨅ (i : ι), expGrowthInf (u i))
Tactic: rw [← iInf_univ, expGrowthInf_biInf u Set.finite_univ, iInf_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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))
⊢ expGrowthInf (⨅ (i : ι), u i) = ⨅ (i : ι), expGrowthInf (u i)
have rw₂ : Eq (α := EReal) (⨅ (x : ι), expGrowthInf (u x)) (⨅ (i : ι), expGrowthInf (u i))
Tactic: rw [← iInf_univ, expGrowthInf_biInf u Set.finite_univ, iInf_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u ⊔ v) = max (expGrowthSup u) (expGrowthSup v)
have 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)
Tactic: rw [expGrowthSup, expGrowthSup, expGrowthSup, ← limsup_max]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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)
have refine : ∀ (n : ℕ), ((u ⊔ v) n).log / (↑n : EReal) = max ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))
Tactic: refine limsup_congr (Eventually.of_forall fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u ⊔ v) n).log / (↑n : EReal) = max ((u n).log / (↑n : EReal)) ((v n).log / (↑n : EReal))
have rw : max (u n).log (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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (hypothesis)
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
⊢ expGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)
have 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)
Tactic: have := map_finset_sup expGrowthSupBotHom hs.toFinset u
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → ℝ≥0∞
⊢ expGrowthSup (⨆ (i : ι), u i) = ⨆ (i : ι), expGrowthSup (u i)
have rw : expGrowthSup (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), u x) = ⨆ (i : ι), expGrowthSup (u i)
Tactic: rw [← iSup_univ, expGrowthSup_biSup u Set.finite_univ, iSup_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → ℝ≥0∞
rw : expGrowthSup (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), u x) = ⨆ (i : ι), expGrowthSup (u i)
⊢ expGrowthSup (⨆ (i : ι), u i) = ⨆ (i : ι), expGrowthSup (u i)
have rw₁ : Eq (α := EReal) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), expGrowthSup (u x))
  (⨆ (i : ι), expGrowthSup (u i))
Tactic: rw [← iSup_univ, expGrowthSup_biSup u Set.finite_univ, iSup_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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))
⊢ expGrowthSup (⨆ (i : ι), u i) = ⨆ (i : ι), expGrowthSup (u i)
have rw₂ : Eq (α := EReal) (⨆ (x : ι), expGrowthSup (u x)) (⨆ (i : ι), expGrowthSup (u i))
Tactic: rw [← iSup_univ, expGrowthSup_biSup u Set.finite_univ, iSup_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u + v) = max (expGrowthSup u) (expGrowthSup v)
have rw : expGrowthSup (u + v) = expGrowthSup (u ⊔ v)
Tactic: rw [← expGrowthSup_sup]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u + v) = expGrowthSup (u ⊔ v)
have a : expGrowthSup (u + v) ≤ expGrowthSup (u ⊔ v)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
a : expGrowthSup (u + v) ≤ expGrowthSup (u ⊔ v)
⊢ expGrowthSup (u + v) = expGrowthSup (u ⊔ v)
have a₁ : expGrowthSup (u ⊔ v) ≤ expGrowthSup (u + v)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u + v) ≤ expGrowthSup (u ⊔ v)
have a : ∀ (n : ℕ), (u + v) n ≤ 2 * (u ⊔ v) n
Tactic: refine expGrowthSup_le_of_eventually_le (b := 2) ofNat_ne_top (Eventually.of_forall fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u + v) n ≤ 2 * (u ⊔ v) n
have a : u n + v n ≤ max (u n) (v n) + max (u n) (v n)
Tactic: rw [Pi.sup_apply u v n, Pi.add_apply u v n, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u ⊔ v) ≤ expGrowthSup (u + v)
have a : ∀ (n : ℕ), (u ⊔ v) n ≤ (u + v) n
Tactic: refine expGrowthSup_monotone fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
⊢ expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
have empty : expGrowthSup 0 = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
Tactic: rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
    expGrowthSup_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
empty : expGrowthSup 0 = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
⊢ expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
have empty₁ : expGrowthSup 0 = ⨆ x ∈ (↑∅ : Set α), expGrowthSup (u x)
Tactic: rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
    expGrowthSup_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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)
⊢ expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
have empty₂ : expGrowthSup 0 = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ x), expGrowthSup (u x)
Tactic: rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
    expGrowthSup_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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)
⊢ expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
have empty₃ : expGrowthSup 0 = ⊥
Tactic: rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
    expGrowthSup_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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 = ⊥
⊢ expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
have empty₄ : Eq (α := EReal) ⊥ ⊥
Tactic: rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
    expGrowthSup_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
a : α
t : Finset α
a_t : a ∉ t
ha : expGrowthSup (∑ x ∈ t, u x) = ⨆ x ∈ t, expGrowthSup (u x)
⊢ expGrowthSup (∑ x ∈ insert a t, u x) = ⨆ x ∈ insert a t, expGrowthSup (u x)
have insert : expGrowthSup (u a + ∑ x ∈ t, u x) = ⨆ x ∈ 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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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)
⊢ expGrowthSup (∑ x ∈ Insert.insert a t, u x) = ⨆ x ∈ Insert.insert a t, expGrowthSup (u x)
have insert₁ : max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ 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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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)
⊢ expGrowthSup (∑ x ∈ Insert.insert a t, u x) = ⨆ x ∈ Insert.insert a t, expGrowthSup (u x)
have insert₂ : max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ t, u x)) = ⨆ x ∈ (↑(Insert.insert a t) : Set α), 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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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)
⊢ expGrowthSup (∑ x ∈ Insert.insert a t, u x) = ⨆ x ∈ Insert.insert a t, expGrowthSup (u x)
have insert₃ : max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ t, u x)) = ⨆ x ∈ Insert.insert a (↑t : Set α), 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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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)
⊢ expGrowthSup (∑ x ∈ Insert.insert a t, u x) = ⨆ x ∈ Insert.insert a t, expGrowthSup (u x)
have insert₄ : max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ t, u x)) =
  max (expGrowthSup (u a)) (⨆ x ∈ (↑t : Set α), 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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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))
⊢ expGrowthSup (∑ x ∈ Insert.insert a t, u x) = ⨆ x ∈ Insert.insert a t, expGrowthSup (u x)
have insert₅ : max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ t, u x)) = max (expGrowthSup (u a)) (⨆ x ∈ 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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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))
⊢ expGrowthSup (∑ x ∈ Insert.insert a t, u x) = ⨆ x ∈ Insert.insert a t, expGrowthSup (u x)
have insert₆ : max (expGrowthSup (u a)) (⨆ x ∈ t, expGrowthSup (u x)) = max (expGrowthSup (u a)) (⨆ x ∈ 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]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Finset α
⊢ expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)
have empty : expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Finset α
empty : expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
⊢ expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)
have insert : ∀ (a : α) (t : Finset α) (a_t : a ∉ t) (ha : expGrowthSup (∑ x ∈ t, u x) = ⨆ x ∈ t, expGrowthSup (u x)),
  expGrowthSup (∑ x ∈ insert a t, u x) = ⨆ x ∈ insert a t, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Finset α
⊢ expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)
have empty : expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Finset α
empty : expGrowthSup (∑ x ∈ ∅, u x) = ⨆ (x : α), ⨆ (_ : Membership.mem (γ := Finset α) ∅ x), expGrowthSup (u x)
⊢ expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)
have insert : ∀ (a : α) (t : Finset α) (a_t : a ∉ t) (ha : expGrowthSup (∑ x ∈ t, u x) = ⨆ x ∈ t, expGrowthSup (u x)),
  expGrowthSup (∑ x ∈ insert a t, u x) = ⨆ x ∈ insert a t, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : 1 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * expGrowthInf u ≤ expGrowthInf (u ∘ v)
have apply : ∀ (n : ℕ) (h : 1 n ≤ u n), 0 n ≤ (u n).log
Tactic: apply le_linearGrowthInf_comp (hu.mono fun n h ↦ ?_) hv
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (hypothesis)
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : 1 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
n : ℕ
h : 1 n ≤ u n
⊢ 0 n ≤ (u n).log
have h₁ : 1 ≤ u n
Tactic: rw [Pi.one_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : 1 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
n : ℕ
h : 1 ≤ u n
⊢ 0 n ≤ (u n).log
have rwa : 0 ≤ (u n).log
Tactic: rwa [Pi.zero_apply, zero_le_log_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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
⊢ expGrowthSup (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * expGrowthSup u
have apply : ∀ (n : ℕ) (h : 1 ≤ u n), 0 ≤ (log ∘ u) n
Tactic: apply linearGrowthSup_comp_le (u := log ∘ u) (hu.mono fun n h ↦ ?_) hv₀ hv₁ hv₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
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
⊢ 0 ≤ (log ∘ u) n
have rwa : 0 ≤ (u n).log
Tactic: rwa [comp_apply, zero_le_log_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
h : Monotone u
h' : u ≠ 0
⊢ 0 ≤ expGrowthInf u
have apply : log ∘ u ≠ ⊥
Tactic: apply (log_monotone.comp h).linearGrowthInf_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
h : Monotone u
h' : u ≠ 0
⊢ log ∘ u ≠ ⊥
have simp : ∀ (h' : ¬∀ (x : ℕ), u x = 0), ¬∀ (x : ℕ), u x = 0
Tactic: simp only [ne_eq, funext_iff, comp_apply, Pi.bot_apply, log_eq_bot_iff, Pi.zero_apply] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
h : Monotone u
h' : u ≠ 0
hv : Tendsto v atTop atTop
⊢ 0 ≤ expGrowthInf (u ∘ v)
have apply : log ∘ u ≠ ⊥
Tactic: apply linearGrowthInf_comp_nonneg (u := log ∘ u) (log_monotone.comp h) _ hv
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
h : Monotone u
h' : u ≠ 0
hv : Tendsto v atTop atTop
⊢ log ∘ u ≠ ⊥
have simp : ∀ (h' : ¬∀ (x : ℕ), u x = 0), ¬∀ (x : ℕ), u x = 0
Tactic: simp only [ne_eq, funext_iff, comp_apply, Pi.bot_apply, log_eq_bot_iff, Pi.zero_apply] at h' ⊢
Cleared hypotheses: h'