-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem μ_nonempty {s : ℕ → ℕ} (hs_le : ∀ n : ℕ, s n ≤ n) {x : R} (ψ : ℕ → ℕ) :
    {a : ℝ | ∀ᶠ n : ℝ in map (fun n : ℕ => μ x ^ (↑(s (ψ n)) * (1 / (ψ n : ℝ)))) atTop,
      n ≤ a}.Nonempty

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
b : ℕ
a✝ : 0 ≤ b
⊢ μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x ^ 1

Tactic:
apply rpow_le_rpow_of_exponent_le (not_lt.mp hμx)

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
b : ℕ
a✝ : 0 ≤ b
⊢ ↑(s (ψ b)) * (1 / ↑(ψ b)) ≤ 1

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
b : ℕ
a✝ : 0 ≤ b
⊢ ↑(s (ψ b)) * (1 / ↑(ψ b)) ≤ 1

Tactic:
rw [mul_one_div]

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
b : ℕ
a✝ : 0 ≤ b
⊢ ↑(s (ψ b)) / ↑(ψ b) ≤ 1

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : μ x < 1
⊢ {a | ∀ᶠ (n : ℝ) in map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}.Nonempty

Tactic:
use 1

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

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
⊢ {a | ∀ᶠ (n : ℝ) in map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}.Nonempty

Tactic:
use μ x

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

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x

Tactic:
use 0

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
⊢ ∀ (b : ℕ), 0 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : μ x < 1
⊢ 1 ∈ {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]

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : μ x < 1
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ 1

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
b : ℕ
a✝ : 0 ≤ b
⊢ μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x

Tactic:
nth_rw 2 [← rpow_one (μ x)]

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
b : ℕ
a✝ : 0 ≤ b
⊢ μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x ^ 1

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
⊢ ∀ (b : ℕ), 0 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x

Tactic:
intro b _

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
b : ℕ
a✝ : 0 ≤ b
⊢ μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : μ x < 1
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ 1

Tactic:
exact ⟨0, fun _ _ ↦ rpow_le_one (apply_nonneg _ _) (le_of_lt hμx)
  (mul_nonneg (cast_nonneg _) (one_div_nonneg.mpr (cast_nonneg _)))⟩

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
⊢ μ x ∈ {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]

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ {a | ∀ᶠ (n : ℝ) in map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}.Nonempty

Tactic:
by_cases hμx : μ x < 1

Result:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : μ x < 1
⊢ {a | ∀ᶠ (n : ℝ) in map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}.Nonempty

case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
⊢ {a | ∀ᶠ (n : ℝ) in map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}.Nonempty

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
b : ℕ
a✝ : 0 ≤ b
⊢ ↑(s (ψ b)) / ↑(ψ b) ≤ 1

Tactic:
exact div_le_one_of_le₀ (cast_le.mpr (hs_le (ψ b))) (cast_nonneg _)

Result:
no goals