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

Tactic:
rw [ha] at hψ_lim

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 (𝓝 0)
ha : a = 0
⊢ limsup (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ 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 (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ (fun n => (μ (x ^ s (ψ n)) ^ (1 / ↑(s (ψ n)))) ^ (↑(s (ψ n)) / ↑(ψ n))) =ᶠ[atTop] fun n =>
    μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))

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

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 (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
h : (fun n => 1 / ↑(s (ψ n)) * ↑(s (ψ n))) =ᶠ[atTop] 1
⊢ (fun n => (μ (x ^ s (ψ n)) ^ (1 / ↑(s (ψ n)))) ^ (↑(s (ψ n)) / ↑(ψ n))) =ᶠ[atTop] fun n =>
    μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))

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

Tactic:
exact le_of_eq (Tendsto.limsup_eq (Tendsto.congr' h_eq
  ((((tendsto_smoothingFun_of_map_one_le_one μ hμ1 x).comp
  ((tendsto_natCast_atTop_iff (R := ℝ)).mp <|
    Tendsto.num (tendsto_natCast_atTop_atTop.comp hψ_mono.tendsto_atTop)
      ha_pos hψ_lim)).rpow hψ_lim (Or.inr ha_pos)))))

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 (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ (fun n => 1 / ↑(s (ψ n)) * ↑(s (ψ n))) =ᶠ[atTop] 1

Tactic:
apply Filter.EventuallyEq.div_mul_cancel_atTop

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

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 : ℝ
m : ℕ
hm : ∀ (b_1 : ℕ), m ≤ b_1 → μ x ^ (↑(s (ψ b_1)) * (1 / ↑(ψ b_1))) ≤ b
k : ℕ
hkm : m ≤ k
⊢ μ (x ^ s (ψ k)) ^ (1 / ↑(ψ k)) ≤ (μ x ^ s (ψ k)) ^ (1 / ↑(ψ k))

Tactic:
exact rpow_le_rpow (apply_nonneg μ _) (map_pow_le_pow' hμ1 x _)
  (one_div_nonneg.mpr (cast_nonneg _))

Result:
no goals