-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem μ_limsup_le_one {s : ℕ → ℕ} (hs_le : ∀ n : ℕ, s n ≤ n) {x : R} {ψ : ℕ → ℕ}
    (hψ_lim : Tendsto ((fun n : ℕ => ↑(s n) / (n : ℝ)) ∘ ψ) atTop (𝓝 0)) :
    limsup (fun n : ℕ => μ x ^ ((s (ψ n) : ℝ) * (1 / (ψ n : ℝ)))) atTop ≤ 1

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
⊢ Tendsto (fun n => μ x ^ (↑(s (ψ n)) * (μ x ^ 0 / ↑(ψ n)))) atTop (𝓝 1)

Tactic:
convert Tendsto.rpow tendsto_const_nhds hψ_lim
    (Or.inl (ne_of_gt (lt_of_lt_of_le zero_lt_one (not_lt.mp hμx))))

Result:
case h.e'_3.h.h.e'_6
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
x✝ : ℕ
⊢ ↑(s (ψ x✝)) * (μ x ^ 0 / ↑(ψ x✝)) = ((fun n => ↑(s n) / ↑n) ∘ ψ) x✝

case h.e'_5.h.e'_3
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
⊢ 1 = μ x ^ 0

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
hμ_lim : ∀ (U : Set ℝ), 1 ∈ U → IsOpen U → ∃ N, ∀ (n : ℕ), N ≤ n → μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ∈ U
⊢ c ≤ 1

Tactic:
apply le_of_forall_pos_le_add

Result:
case neg.h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
hμ_lim : ∀ (U : Set ℝ), 1 ∈ U → IsOpen U → ∃ N, ∀ (n : ℕ), N ≤ n → μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ∈ U
⊢ ∀ (ε : ℝ), 0 < ε → c ≤ 1 + ε

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : μ x < 1
⊢ c ≤ 1

Tactic:
apply hc_bd (1 : ℝ) 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : μ x < 1
⊢ ∀ (b : ℕ), 0 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ 1

Proof state:
case neg.h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
hμ_lim : ∀ (U : Set ℝ), 1 ∈ U → IsOpen U → ∃ N, ∀ (n : ℕ), N ≤ n → μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ∈ U
ε : ℝ
hε : 0 < ε
⊢ c ≤ 1 + ε

Tactic:
have h1 : (1 : ℝ) ∈ Set.Ioo 0 (1 + ε) := by
  simp only [Set.mem_Ioo, zero_lt_one, lt_add_iff_pos_right, hε, and_self]

Result:
case neg.h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
hμ_lim : ∀ (U : Set ℝ), 1 ∈ U → IsOpen U → ∃ N, ∀ (n : ℕ), N ≤ n → μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ∈ U
ε : ℝ
hε : 0 < ε
h1 : 1 ∈ Set.Ioo 0 (1 + ε)
⊢ c ≤ 1 + ε

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
⊢ limsup (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop ≤ 1

Tactic:
simp only [limsup, limsSup]

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

Proof state:
case neg.h.intro
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
hμ_lim : ∀ (U : Set ℝ), 1 ∈ U → IsOpen U → ∃ N, ∀ (n : ℕ), N ≤ n → μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ∈ U
ε : ℝ
hε : 0 < ε
h1 : 1 ∈ Set.Ioo 0 (1 + ε)
k : ℕ
hk : ∀ (n : ℕ), k ≤ n → μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ∈ Set.Ioo 0 (1 + ε)
⊢ c ≤ 1 + ε

Tactic:
exact hc_bd (1 + ε) k fun b hb => le_of_lt (Set.mem_Ioo.mp (hk b hb)).2

Result:
no goals

Proof state:
case h.e'_3.h.h.e'_6
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
x✝ : ℕ
⊢ ↑(s (ψ x✝)) * (μ x ^ 0 / ↑(ψ x✝)) = ((fun n => ↑(s n) / ↑n) ∘ ψ) x✝

Tactic:
simp only [rpow_zero, mul_one_div, Function.comp_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
hμ_lim : ∀ (U : Set ℝ), 1 ∈ U → IsOpen U → ∃ N, ∀ (n : ℕ), N ≤ n → μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ∈ U
ε : ℝ
hε : 0 < ε
⊢ 1 ∈ Set.Ioo 0 (1 + ε)

Tactic:
simp only [Set.mem_Ioo, zero_lt_one, lt_add_iff_pos_right, hε, and_self]

Result:
no goals

Proof state:
case neg.h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
hμ_lim : ∀ (U : Set ℝ), 1 ∈ U → IsOpen U → ∃ N, ∀ (n : ℕ), N ≤ n → μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ∈ U
⊢ ∀ (ε : ℝ), 0 < ε → c ≤ 1 + ε

Tactic:
intro ε hε

Result:
case neg.h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
hμ_lim : ∀ (U : Set ℝ), 1 ∈ U → IsOpen U → ∃ N, ∀ (n : ℕ), N ≤ n → μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ∈ U
ε : ℝ
hε : 0 < ε
⊢ c ≤ 1 + ε