awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd :
  ∀ (x_1 : ℝ) (x_2 : ℕ)
    (h :
      ∀ (b : ℕ),
        x_2 ≤ b →
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ x_1),
    c ≤ x_1
hμx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
hμ_lim :
  ∀ (U : Set ℝ),
    1 ∈ U →
      IsOpen U →
        ∃ (N : ℕ),
          ∀ (n : ℕ),
            N ≤ n →
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) ∈ U
ε : ℝ
hε : 0 < ε
h1 : 1 ∈ Set.Ioo 0 (1 + ε)
neg :
  ∀ (k : ℕ)
    (hk :
      ∀ (n : ℕ),
        k ≤ n →
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) ∈
            Set.Ioo 0 (1 + ε)),
    c ≤ 1 + ε
⊢ c ≤ 1 + ε

Tactic:
obtain ⟨k, hk⟩ := hμ_lim (Set.Ioo (0 : ℝ) (1 + ε)) h1 isOpen_Ioo

Premises used: isOpen_Ioo, HAdd.hAdd, OfNat.ofNat, Set.Ioo
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd :
  ∀ (x_1 : ℝ) (x_2 : ℕ)
    (h :
      ∀ (b : ℕ),
        x_2 ≤ b →
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ x_1),
    c ≤ x_1
hμx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
hμ_lim :
  ∀ (U : Set ℝ),
    1 ∈ U →
      IsOpen U →
        ∃ (N : ℕ),
          ∀ (n : ℕ),
            N ≤ n →
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) ∈ U
ε : ℝ
hε : 0 < ε
h1 : 1 ∈ Set.Ioo 0 (1 + ε)
k : ℕ
hk :
  ∀ (n : ℕ),
    k ≤ n →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) ∈
        Set.Ioo 0 (1 + ε)
⊢ c ≤ 1 + ε

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

Premises used: Set.mem_Ioo, le_of_lt, And.right, HAdd.hAdd, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd :
  ∀ (x_1 : ℝ) (x_2 : ℕ)
    (h :
      ∀ (b : ℕ),
        x_2 ≤ b →
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ x_1),
    c ≤ x_1
hμx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
hμ_lim :
  ∀ (U : Set ℝ),
    1 ∈ U →
      IsOpen U →
        ∃ (N : ℕ),
          ∀ (n : ℕ),
            N ≤ n →
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) ∈ U
ε : ℝ
hε : 0 < ε
h1 : 1 ∈ Set.Ioo 0 (1 + ε)
k : ℕ
hk :
  ∀ (n : ℕ),
    k ≤ n →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 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

Premises used: Set.mem_Ioo, le_of_lt, And.right, HAdd.hAdd, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
pos :
  ∀ (ha : a = 0),
    limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
        atTop ≤
      smoothingFun μ x ^ a
neg :
  ∀ (ha : ¬a = 0),
    limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
        atTop ≤
      smoothingFun μ x ^ a
⊢ limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : a = 0
⊢ Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)

Tactic:
rw [ha] at hψ_lim
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : a = 0
hψ_lim₁ : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
⊢ a = 0

Tactic:
rw [ha] at hψ_lim
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
apply :
  Subset (α := Set ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
apply₁ :
  BddBelow (α := ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
⊢ LE.le (α := ℝ)
    (limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)
    (limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)

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

Premises used: _private.0.μ_nonempty, csInf_le_csInf
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
hb :
  Membership.mem (γ := Set ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
    b
simp :
  ∀
    (hb :
      ∃ (a : ℕ),
        ∀ (b_1 : ℕ),
          a ≤ b_1 →
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤
              b),
    ∃ (a : ℕ),
      ∀ (b_1 : ℕ),
        a ≤ b_1 → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
⊢ Membership.mem (γ := Set ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
    b

Tactic:
simp only [eventually_map, eventually_atTop, ge_iff_le, Set.mem_setOf_eq] at hb ⊢

Premises used: ge_iff_le, Set.mem_setOf_eq, Filter.eventually_map, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
hb :
  ∃ (a : ℕ),
    ∀ (b_1 : ℕ),
      a ≤ b_1 →
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
obtain :
  ∀ (m : ℕ)
    (hm :
      ∀ (b_1 : ℕ),
        m ≤ b_1 →
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b),
    ∃ (a : ℕ),
      ∀ (b_1 : ℕ),
        a ≤ b_1 → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
⊢ ∃ (a : ℕ),
    ∀ (b_1 : ℕ),
      a ≤ b_1 → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b

Tactic:
obtain ⟨m, hm⟩ := hb
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm :
  ∀ (b_1 : ℕ),
    m ≤ b_1 →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
h :
  ∀ (b_1 : ℕ),
    m ≤ b_1 → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
⊢ ∃ (a : ℕ),
    ∀ (b_1 : ℕ),
      a ≤ b_1 → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b_1)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b

Tactic:
use m
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm :
  ∀ (b_1 : ℕ),
    m ≤ b_1 →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
k : ℕ
hkm : m ≤ k
apply :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ k)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ k)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ k)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)) ≤ b

Tactic:
apply le_trans _ (hm k hkm)

Premises used: le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm :
  ∀ (b_1 : ℕ),
    m ≤ b_1 →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
k : ℕ
hkm : m ≤ k
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ k)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ k)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ k)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ k)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ))

Tactic:
rw [rpow_mul (apply_nonneg μ x), rpow_natCast]

Premises used: NonnegHomClass.apply_nonneg, Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm :
  ∀ (b_1 : ℕ),
    m ≤ b_1 →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
k : ℕ
hkm : m ≤ k
h₁ : (μ : (a : R) → ℝ) (x ^ s (ψ k)) ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ k))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ k)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ k)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ k) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm :
  ∀ (b_1 : ℕ),
    m ≤ b_1 →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
k : ℕ
hkm : m ≤ k
⊢ (μ : (a : R) → ℝ) (x ^ s (ψ k)) ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ k))

Tactic:
map_pow_le_pow' hμ1 x _

Premises used: map_pow_le_pow'
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm :
  ∀ (b_1 : ℕ),
    m ≤ b_1 →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b_1)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b_1) : ℝ)) ≤ b
k : ℕ
hkm : m ≤ k
⊢ (μ : (a : R) → ℝ) (x ^ s (ψ k)) ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ k))

Tactic:
exact map_pow_le_pow' hμ1 x _

Premises used: map_pow_le_pow'
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
h :
  Membership.mem (γ := Set ℝ)
    (lowerBounds
      {a : ℝ |
        ∀ᶠ (n : ℝ) in
          map
            (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
            atTop,
          n ≤ a})
    0
⊢ BddBelow (α := ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}

Tactic:
use 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
h :
  ∀ (x_1 : ℝ) (x_2 : ℕ)
    (h :
      ∀ (b : ℕ),
        x_2 ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ x_1),
    0 ≤ x_1
⊢ Membership.mem (γ := Set ℝ)
    (lowerBounds
      {a : ℝ |
        ∀ᶠ (n : ℝ) in
          map
            (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
            atTop,
          n ≤ a})
    0

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

Premises used: ge_iff_le, forall_exists_index, mem_lowerBounds, Set.mem_setOf_eq, Filter.eventually_map, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
x_1 : ℝ
m : ℕ
hm :
  ∀ (b : ℕ), m ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ x_1
⊢ 0 ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ m)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ m) : ℝ))

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ)
    (h :
      ∀ (b : ℕ),
        x_2 ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ b)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ x_1),
    0 ≤ x_1

Tactic:
exact fun _ m hm ↦ le_trans (by positivity) (hm m (le_refl _))

Premises used: le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ LE.le (α := ℝ)
    (limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)
    1

Tactic:
(μ_limsup_le_one μ hs_le hψ_lim)

Premises used: _private.0.μ_limsup_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
rw : 1 = HPow.hPow (β := ℝ) (smoothingFun μ x) 0
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ 1 = smoothingFun μ x ^ a

Tactic:
rw [ha, rpow_zero]

Premises used: Real.rpow_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
ha : a = 0
calc :
  LE.le (α := ℝ)
    (limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)
    (limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)
calc₁ : 1 = smoothingFun μ x ^ a
⊢ limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a

Tactic:
calc limsup (fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤
          limsup (fun n : ℕ => μ x ^ ((s (ψ n) : ℝ) * (1 / (ψ n : ℝ)))) atTop := by
          apply csInf_le_csInf _ (μ_nonempty μ hs_le ψ)
          · intro b hb
            simp only [eventually_map, eventually_atTop, ge_iff_le, Set.mem_setOf_eq] at hb ⊢
            obtain ⟨m, hm⟩ := hb
            use m
            intro k hkm
            apply le_trans _ (hm k hkm)
            rw [rpow_mul (apply_nonneg μ x), rpow_natCast]
            gcongr
            exact map_pow_le_pow' hμ1 x _
          · use 0
            simp only [mem_lowerBounds, eventually_map, eventually_atTop, ge_iff_le,
              Set.mem_setOf_eq, forall_exists_index]
            exact fun _ m hm ↦ le_trans (by positivity) (hm m (le_refl _))
      _ ≤ 1 := (μ_limsup_le_one μ hs_le hψ_lim)
      _ = smoothingFun μ x ^ a := by rw [ha, rpow_zero]

Premises used: HMul.hMul, smoothingFun, HDiv.hDiv, Nat.cast, Filter.limsup, Filter.atTop, HPow.hPow, _private.0.μ_limsup_le_one, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
⊢ 0 < a

Tactic:
have ha_pos : 0 < a := lt_of_le_of_ne a_in.1 (Ne.symm ha)
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
hg : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑(s (ψ x)) : ℝ)) atTop atTop
⊢ EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ)) 1

Tactic:
apply Filter.EventuallyEq.div_mul_cancel_atTop

Premises used: Filter.EventuallyEq.div_mul_cancel_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑(s (ψ x)) : ℝ)) atTop atTop

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

Premises used: StrictMono.tendsto_atTop, Filter.Tendsto.num, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑(s (ψ x)) : ℝ)) atTop atTop

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

Premises used: StrictMono.tendsto_atTop, Filter.Tendsto.num, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp