-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem limsup_mu_le (hμ1 : μ 1 ≤ 1) {s : ℕ → ℕ} (hs_le : ∀ n : ℕ, s n ≤ n) {x : R}
    {a : ℝ} (a_in : a ∈ Set.Icc (0 : ℝ) 1) {ψ : ℕ → ℕ} (hψ_mono : StrictMono ψ)
    (hψ_lim : Tendsto ((fun n : ℕ => (s n : ℝ) / ↑n) ∘ ψ) atTop (𝓝 a)) :
    limsup (fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤ smoothingFun μ x ^ a

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm : ∀ (b_1 : ℕ), m ≤ b_1 → μ x ^ (↑(s (ψ b_1)) * (1 / ↑(ψ b_1))) ≤ b
⊢ ∀ (b_1 : ℕ), m ≤ b_1 → μ (x ^ s (ψ b_1)) ^ (1 / ↑(ψ b_1)) ≤ b

Tactic:
intro k hkm

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm : ∀ (b_1 : ℕ), m ≤ b_1 → μ x ^ (↑(s (ψ b_1)) * (1 / ↑(ψ b_1))) ≤ b
k : ℕ
hkm : m ≤ k
⊢ μ (x ^ s (ψ k)) ^ (1 / ↑(ψ k)) ≤ b

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
⊢ limsup (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

Tactic:
by_cases ha : a = 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : a = 0
⊢ limsup (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
⊢ limsup (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ (x ^ s (ψ b)) ^ (1 / ↑(ψ b)) ≤ x_1) → 0 ≤ x_1

Tactic:
exact fun _ m hm ↦ le_trans (rpow_nonneg (apply_nonneg μ _) _) (hm m (le_refl _))

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ {a | ∀ᶠ (n : ℝ) in map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a} ⊆
    {a | ∀ᶠ (n : ℝ) in map (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop, n ≤ a}

Tactic:
intro b hb

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
hb : b ∈ {a | ∀ᶠ (n : ℝ) in map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}
⊢ b ∈ {a | ∀ᶠ (n : ℝ) in map (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop, n ≤ a}

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
hb : ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → μ x ^ (↑(s (ψ b_1)) * (1 / ↑(ψ b_1))) ≤ b
⊢ ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → μ (x ^ s (ψ b_1)) ^ (1 / ↑(ψ b_1)) ≤ b

Tactic:
obtain ⟨m, hm⟩ := hb

Result:
case intro
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm : ∀ (b_1 : ℕ), m ≤ b_1 → μ x ^ (↑(s (ψ b_1)) * (1 / ↑(ψ b_1))) ≤ b
⊢ ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → μ (x ^ s (ψ b_1)) ^ (1 / ↑(ψ b_1)) ≤ b

Proof state:
case hg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ Tendsto (fun x => ↑(s (ψ x))) atTop atTop

Tactic:
exact Tendsto.num (tendsto_natCast_atTop_atTop.comp hψ_mono.tendsto_atTop) ha_pos hψ_lim

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ limsup (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

Tactic:
have h_eq : (fun n : ℕ =>
    (μ (x ^ s (ψ n)) ^ (1 / (s (ψ n) : ℝ))) ^ ((s (ψ n) : ℝ) / (ψ n : ℝ))) =ᶠ[atTop]
    fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ)) := by
  have h : (fun n : ℕ => (1 : ℝ) / (s (ψ n) : ℝ) * (s (ψ n) : ℝ)) =ᶠ[atTop] 1 := by
    apply Filter.EventuallyEq.div_mul_cancel_atTop
    exact Tendsto.num (tendsto_natCast_atTop_atTop.comp hψ_mono.tendsto_atTop) ha_pos hψ_lim
  simp_rw [← rpow_mul (apply_nonneg μ _), mul_div]
  exact EventuallyEq.comp₂ EventuallyEq.rfl HPow.hPow (h.div EventuallyEq.rfl)

Result:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
h_eq :
  (fun n => (μ (x ^ s (ψ n)) ^ (1 / ↑(s (ψ n)))) ^ (↑(s (ψ n)) / ↑(ψ n))) =ᶠ[atTop] fun n =>
    μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))
⊢ limsup (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ 0 ∈ lowerBounds {a | ∀ᶠ (n : ℝ) in map (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop, n ≤ a}

Tactic:
simp only [mem_lowerBounds, eventually_map, eventually_atTop, ge_iff_le,
  Set.mem_setOf_eq, forall_exists_index]

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ (x ^ s (ψ b)) ^ (1 / ↑(ψ b)) ≤ x_1) → 0 ≤ x_1

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm : ∀ (b_1 : ℕ), m ≤ b_1 → μ x ^ (↑(s (ψ b_1)) * (1 / ↑(ψ b_1))) ≤ b
⊢ ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → μ (x ^ s (ψ b_1)) ^ (1 / ↑(ψ b_1)) ≤ b

Tactic:
use m

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm : ∀ (b_1 : ℕ), m ≤ b_1 → μ x ^ (↑(s (ψ b_1)) * (1 / ↑(ψ b_1))) ≤ b
⊢ ∀ (b_1 : ℕ), m ≤ b_1 → μ (x ^ s (ψ b_1)) ^ (1 / ↑(ψ b_1)) ≤ b