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

Tactic:
have ha_pos : 0 < a := lt_of_le_of_ne a_in.1 (Ne.symm ha)

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

Tactic:
exact EventuallyEq.comp₂ EventuallyEq.rfl HPow.hPow (h.div EventuallyEq.rfl)

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
⊢ BddBelow {a | ∀ᶠ (n : ℝ) in map (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop, n ≤ a}

Tactic:
use 0

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
⊢ 0 ∈ lowerBounds {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 : ℝ
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:
rw [rpow_mul (apply_nonneg μ x), rpow_natCast]

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 : ℝ
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))

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
k : ℕ
hkm : m ≤ k
⊢ μ (x ^ s (ψ k)) ^ (1 / ↑(ψ k)) ≤ b

Tactic:
apply le_trans _ (hm k hkm)

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 : ℝ
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)))

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
⊢ limsup (fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ limsup (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop

Tactic:
apply csInf_le_csInf _ (μ_nonempty μ hs_le ψ)

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
⊢ {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}

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
⊢ BddBelow {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 (𝓝 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))

Tactic:
simp_rw [← rpow_mul (apply_nonneg μ _), mul_div]

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:
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
⊢ 1 = smoothingFun μ x ^ a

Tactic:
rw [ha, rpow_zero]

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

Tactic:
simp only [eventually_map, eventually_atTop, ge_iff_le, Set.mem_setOf_eq] at 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 : ∃ 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