awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
pos :
  ∀ (hμx : LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)),
    Set.Nonempty (α := ℝ)
      {a : ℝ |
        ∀ᶠ (n : ℝ) in
          map
            (fun (n : ℕ) ↦
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
            atTop,
          n ≤ a}
⊢ Set.Nonempty (α := ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
have neg : ∀ (hμx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)),
  Set.Nonempty (α := ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
Tactic: by_cases hμx : μ x < 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 : ℝ)
⊢ Set.Nonempty (α := ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
have 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
Tactic: use 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 : ℝ)
⊢ Membership.mem (γ := Set ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
    1
have h : ∃ (a : ℕ),
  ∀ (b : ℕ),
    a ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ 1
Tactic: simp only [eventually_map, eventually_atTop, ge_iff_le, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 : ℝ)
⊢ Set.Nonempty (α := ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
have 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 : ℝ)
Tactic: use μ x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 : ℝ)
⊢ 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 : ℝ)
have h : ∃ (a : ℕ),
  ∀ (b : ℕ),
    a ≤ b →
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤
        (μ : (a : R) → ℝ) x
Tactic: simp only [eventually_map, eventually_atTop, ge_iff_le, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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) : ℝ)) ≤
          (μ : (a : R) → ℝ) x
have h : ∀ (b : ℕ),
  0 ≤ b →
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤
      (μ : (a : R) → ℝ) x
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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
have h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1
Tactic: nth_rw 2 [← rpow_one (μ x)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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) : ℝ)) ≤
    HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1
have h : (↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ) ≤ 1
Tactic: apply rpow_le_rpow_of_exponent_le (not_lt.mp hμx)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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
⊢ (↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ) ≤ 1
have h : HDiv.hDiv (α := ℝ) (↑(s (ψ b)) : ℝ) (↑(ψ b) : ℝ) ≤ 1
Tactic: rw [mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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)
⊢ LE.le (α := ℝ)
    (sInf
      {a : ℝ |
        ∀ᶠ (n : ℝ) in
          map
            (fun (n : ℕ) ↦
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
            atTop,
          n ≤ a})
    1
have 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
Tactic: rw [csInf_le_iff (μ_bddBelow μ s ψ) (μ_nonempty μ hs_le ψ)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
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
⊢ c ≤ 1
have 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
Tactic: simp only [mem_lowerBounds, eventually_map, eventually_atTop, ge_iff_le, Set.mem_setOf_eq,
      forall_exists_index] at hc_bd
Cleared hypotheses: hc_bd
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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
⊢ c ≤ 1
have pos : ∀ (hμx : LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)), c ≤ 1
Tactic: by_cases hμx : μ x < 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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
⊢ c ≤ 1
have neg : ∀ (hμx : ¬LT.lt (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)), c ≤ 1
Tactic: by_cases hμx : μ x < 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 : ℝ)
⊢ c ≤ 1
have pos : ∀ (b : ℕ),
  0 ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ 1
Tactic: apply hc_bd (1 : ℝ) 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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)
have nth_rw : Tendsto (β := ℝ)
  (fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      ((↑(s (ψ n)) : ℝ) * (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0 / (↑(ψ n) : ℝ))))
  atTop (𝓝 1)
Tactic: nth_rw 1 [← rpow_zero (μ x)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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)) : ℝ) * (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0 / (↑(ψ n) : ℝ))))
    atTop (𝓝 1)
have h : ∀ (x_1 : ℕ),
  (↑(s (ψ x_1)) : ℝ) * (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0 / (↑(ψ x_1) : ℝ)) =
    ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) x_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))))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
        ((↑(s (ψ n)) : ℝ) * (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0 / (↑(ψ n) : ℝ))))
    atTop (𝓝 1)
have h₁ : 1 = HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0
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))))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 : ℝ)
⊢ 1 = HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0
have h : Eq (α := ℝ) 1 1
Tactic: rw [rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
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 : ℝ)
⊢ c ≤ 1
have hμ_lim : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
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)
⊢ c ≤ 1
have hμ_lim₁ : ∀ (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
Cleared hypotheses: hμ_lim
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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
⊢ c ≤ 1
have neg : ∀ (ε : ℝ), 0 < ε → c ≤ 1 + ε
Tactic: apply le_of_forall_pos_le_add
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
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 < ε
⊢ c ≤ 1 + ε
have h1 : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 + ε)
⊢ c ≤ 1 + ε
have neg : ∀ (k : ℕ)
  (hk :
    ∀ (n : ℕ),
      k ≤ n →
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) ∈
          Set.Ioo 0 (1 + ε)),
  c ≤ 1 + ε
Tactic: obtain ⟨k, hk⟩ := hμ_lim (Set.Ioo (0 : ℝ) (1 + ε)) h1 isOpen_Ioo
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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)
⊢ limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
have pos : ∀ (ha : a = 0),
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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
⊢ limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
have neg : ∀ (ha : ¬a = 0),
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
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
⊢ limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
have hψ_lim₁ : Tendsto (β := ℝ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 0)
Tactic: rw [ha] at hψ_lim
Cleared hypotheses: hψ_lim, ha
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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)
    (limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop)
have 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}
Tactic: apply csInf_le_csInf _ (μ_nonempty μ hs_le ψ)