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μx : LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
h :
  Membership.mem (γ := Set ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
    1
⊢ Set.Nonempty (α := ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}

Tactic:
use 1
-- 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μx : LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
h :
  ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ 1
⊢ Membership.mem (γ := Set ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
    1

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

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
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
⊢ ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ 1

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

Premises used: Iff.mpr, mul_nonneg, Nat.cast_nonneg, le_of_lt, one_div_nonneg, Real.rpow_le_one, Exists.intro, NonnegHomClass.apply_nonneg, 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μx : LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
⊢ ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 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 _)))⟩
-- 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μx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
h :
  Membership.mem (α := ℝ) (γ := Set ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
    ((μ : (a : R) → ℝ) x : ℝ)
⊢ Set.Nonempty (α := ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}

Tactic:
use μ x

Premises used: DFunLike.coe
-- 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μx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
h :
  ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b →
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤
          (μ : (a : R) → ℝ) x
⊢ Membership.mem (α := ℝ) (γ := Set ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
    ((μ : (a : R) → ℝ) x : ℝ)

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

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
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
h :
  ∀ (b : ℕ),
    0 ≤ b →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤
        (μ : (a : R) → ℝ) x
⊢ ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b →
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤
          (μ : (a : R) → ℝ) x

Tactic:
use 0
-- 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μx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
b : ℕ
h :
  0 ≤ b →
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤
      (μ : (a : R) → ℝ) x
⊢ 0 ≤ b →
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤
      (μ : (a : R) → ℝ) x

Tactic:
_
-- 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μx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
b : ℕ
h_1 : 0 ≤ b
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤
    HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤
    (μ : (a : R) → ℝ) x

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

Premises used: Real.rpow_one, DFunLike.coe
-- 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μx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
b : ℕ
h_1 : 0 ≤ b
h : (↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ) ≤ 1
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤
    HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1

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

Premises used: not_lt, Iff.mp, Real.rpow_le_rpow_of_exponent_le
-- 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μx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
b : ℕ
h_1 : 0 ≤ b
h : HDiv.hDiv (α := ℝ) (↑(s (ψ b)) : ℝ) (↑(ψ b) : ℝ) ≤ 1
⊢ (↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ) ≤ 1

Tactic:
rw [mul_one_div]

Premises used: mul_one_div
-- 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μx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
b : ℕ
h : 0 ≤ b
⊢ HDiv.hDiv (α := ℝ) (↑(s (ψ b)) : ℝ) (↑(ψ b) : ℝ) ≤ 1

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

Premises used: div_le_one_of_le₀, Iff.mpr, Nat.cast_nonneg, Nat.cast_le
-- 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μx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
b : ℕ
h : 0 ≤ b
⊢ HDiv.hDiv (α := ℝ) (↑(s (ψ b)) : ℝ) (↑(ψ b) : ℝ) ≤ 1

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

Premises used: div_le_one_of_le₀, Iff.mpr, Nat.cast_le
-- 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)
rw :
  ∀ (b : ℝ),
    Membership.mem (γ := Set ℝ)
        (lowerBounds
          {a : ℝ |
            ∀ᶠ (n : ℝ) in
              map
                (fun (n : ℕ) ↦
                  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
                atTop,
              n ≤ a})
        b →
      b ≤ 1
⊢ LE.le (α := ℝ)
    (sInf
      {a : ℝ |
        ∀ᶠ (n : ℝ) in
          map
            (fun (n : ℕ) ↦
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
            atTop,
          n ≤ a})
    1

Tactic:
rw [csInf_le_iff (μ_bddBelow μ s ψ) (μ_nonempty μ hs_le ψ)]

Premises used: _private.0.μ_nonempty, _private.0.μ_bddBelow, csInf_le_iff
-- 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 :
  Membership.mem (γ := Set ℝ)
    (lowerBounds
      {a : ℝ |
        ∀ᶠ (n : ℝ) in
          map
            (fun (n : ℕ) ↦
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
            atTop,
          n ≤ a})
    c
⊢ ∀ (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

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

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
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
pos : ∀ (hμx : LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)), c ≤ 1
neg : ∀ (hμx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)), c ≤ 1
⊢ c ≤ 1

Tactic:
by_cases hμx : μ x < 1

Premises used: DFunLike.coe
-- 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 : ℝ)
pos :
  ∀ (b : ℕ),
    0 ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ 1
⊢ c ≤ 1

Tactic:
apply hc_bd (1 : ℝ) 0

Premises used: 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 : ℝ)
b : ℕ
pos : 0 ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ 1
⊢ 0 ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ 1

Tactic:
_
-- 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 : ℝ)
b : ℕ
h : 0 ≤ b
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ 1

Tactic:
rpow_le_one (apply_nonneg _ _) (le_of_lt hμx)
          (mul_nonneg (cast_nonneg _) (one_div_nonneg.mpr (cast_nonneg _)))

Premises used: Iff.mpr, mul_nonneg, Nat.cast_nonneg, le_of_lt, one_div_nonneg, Real.rpow_le_one, NonnegHomClass.apply_nonneg
-- 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 : ℝ)
b : ℕ
h : 0 ≤ b
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ 1

Tactic:
exact rpow_le_one (apply_nonneg _ _) (le_of_lt hμx)
          (mul_nonneg (cast_nonneg _) (one_div_nonneg.mpr (cast_nonneg _)))

Premises used: Iff.mpr, mul_nonneg, Nat.cast_nonneg, le_of_lt, one_div_nonneg, Real.rpow_le_one, NonnegHomClass.apply_nonneg
-- 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 : ℝ)
nth_rw :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
        ((↑(s (ψ n)) : ℝ) * (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0 / (↑(ψ n) : ℝ))))
    atTop (𝓝 1)
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
    atTop (𝓝 1)

Tactic:
nth_rw 1 [← rpow_zero (μ x)]

Premises used: Real.rpow_zero, DFunLike.coe
-- 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 : ℝ)
⊢ Tendsto
    (fun (t : ℕ) ↦
      HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
        (((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) t))
    atTop (𝓝 (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0))

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

Premises used: tendsto_const_nhds, ne_of_gt, Filter.Tendsto.rpow, zero_lt_one, not_lt, Iff.mp, Or.inl, lt_of_lt_of_le
-- 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 :
  ∀ (x_1 : ℕ),
    (↑(s (ψ x_1)) : ℝ) * (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0 / (↑(ψ x_1) : ℝ)) =
      ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) x_1
h₁ : 1 = HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
        ((↑(s (ψ n)) : ℝ) * (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) 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))))

Premises used: tendsto_const_nhds, ne_of_gt, Filter.Tendsto.rpow, zero_lt_one, not_lt, Iff.mp, Or.inl, lt_of_lt_of_le
-- 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_2 : ℝ) (x_3 : ℕ)
    (h :
      ∀ (b : ℕ),
        x_3 ≤ b →
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ x_2),
    c ≤ x_2
hμx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
x_1 : ℕ
⊢ (↑(s (ψ x_1)) : ℝ) * (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0 / (↑(ψ x_1) : ℝ)) =
    ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) x_1

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

Premises used: Real.rpow_zero, mul_one_div, Function.comp_apply
-- 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 h₁ : Eq (α := ℝ) 1 1
⊢ 1 = HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0

Tactic:
rw [rpow_zero]

Premises used: Real.rpow_zero
-- 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 : ℝ)
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
    atTop (𝓝 1)

Tactic:
have hμ_lim : Tendsto (fun n : ℕ => μ x ^ (↑(s (ψ n)) * (1 / (ψ n : ℝ)))) atTop (𝓝 1) := by
        nth_rw 1 [← rpow_zero (μ x)]
        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))))
        · simp only [rpow_zero, mul_one_div, Function.comp_apply]
        · rw [rpow_zero]
-- 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 :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
    atTop (𝓝 1)
⊢ ∀ (U : Set ℝ),
    1 ∈ U →
      IsOpen U →
        ∃ (N : ℕ),
          ∀ (n : ℕ),
            N ≤ n →
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) ∈ U

Tactic:
rw [tendsto_atTop_nhds] at hμ_lim

Premises used: tendsto_atTop_nhds
-- 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
neg : ∀ (ε : ℝ), 0 < ε → c ≤ 1 + ε
⊢ c ≤ 1

Tactic:
apply le_of_forall_pos_le_add

Premises used: le_of_forall_pos_le_add
-- 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 < ε
⊢ 1 ∈ Set.Ioo 0 (1 + ε)

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

Premises used: lt_add_iff_pos_right, Set.mem_Ioo, and_self, zero_lt_one
-- 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 < ε
⊢ 1 ∈ Set.Ioo 0 (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]