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
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
⊢ ∀ᶠ (c : ℕ) in atTop, smoothingSeminormSeq μ 1 c ≤ 1
have simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ 1 b ≤ 1
Tactic: simp only [eventually_atTop, ge_iff_le]
-- 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 : ℝ)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ 1 b ≤ 1
have h : ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ 1 b ≤ 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
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) 1 n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤ 1
have h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤ 1
Tactic: rw [one_pow]
-- 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 : ℝ)
n : ℕ
hn : 1 ≤ n
| 1
have rw : HPow.hPow (α := ℝ) 1 (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [← one_rpow (1 / n : ℝ)]
-- 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 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤ 1
have h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
  HPow.hPow (α := ℝ) 1 (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: conv_rhs => rw [← one_rpow (1 / n : ℝ)]
-- 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 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ 0 < HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have apply : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: apply _root_.div_pos zero_lt_one
-- 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 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)
have rw : 0 < n
Tactic: rw [← cast_zero, cast_lt]
-- 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 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) 1 (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have hn1 : 0 < HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: have hn1 : 0 < (1 / n : ℝ) := by
    apply _root_.div_pos zero_lt_one
    rw [← cast_zero, cast_lt]
    exact succ_le_iff.mp hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
⊢ smoothingFun μ x ≤ (μ : (a : R) → ℝ) x
have apply : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑1 : ℕ) : ℝ)) ≤ (μ : (a : R) → ℝ) x
Tactic: apply (smoothingFun_le μ x 1).trans
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑1 : ℕ) : ℝ)) ≤ (μ : (a : R) → ℝ) x
have rw : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (β := ℕ) x 1) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) ≤
  (μ : (a : R) → ℝ) x
Tactic: rw [PNat.one_coe, pow_one, cast_one, div_one, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (β := ℕ) x 1) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) ≤
    (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑1 : ℕ) : ℝ)) ≤ (μ : (a : R) → ℝ) x
have rw₁ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) ≤ (μ : (a : R) → ℝ) x
Tactic: rw [PNat.one_coe, pow_one, cast_one, div_one, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (β := ℕ) x 1) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) ≤
    (μ : (a : R) → ℝ) x
rw₁ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) ≤ (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑1 : ℕ) : ℝ)) ≤ (μ : (a : R) → ℝ) x
have rw₂ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 / 1) ≤ (μ : (a : R) → ℝ) x
Tactic: rw [PNat.one_coe, pow_one, cast_one, div_one, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (β := ℕ) x 1) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) ≤
    (μ : (a : R) → ℝ) x
rw₁ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) ≤ (μ : (a : R) → ℝ) x
rw₂ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 / 1) ≤ (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑1 : ℕ) : ℝ)) ≤ (μ : (a : R) → ℝ) x
have rw₃ : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1 ≤ (μ : (a : R) → ℝ) x
Tactic: rw [PNat.one_coe, pow_one, cast_one, div_one, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (β := ℕ) x 1) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) ≤
    (μ : (a : R) → ℝ) x
rw₁ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) ≤ (μ : (a : R) → ℝ) x
rw₂ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 / 1) ≤ (μ : (a : R) → ℝ) x
rw₃ : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1 ≤ (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑1 : ℕ) : ℝ)) ≤ (μ : (a : R) → ℝ) x
have rw₄ : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
Tactic: rw [PNat.one_coe, pow_one, cast_one, div_one, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
n : ℕ
⊢ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ))
have refine : HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1
Tactic: refine Set.mem_Icc.mpr ⟨div_nonneg (cast_nonneg (mu μ hn n)) (cast_nonneg n), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1
have pos : ∀ (hn0 : n = 0), HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
n : ℕ
pos : ∀ (hn0 : n = 0), HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1
⊢ HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1
have neg : ∀ (hn0 : ¬n = 0), HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
n : ℕ
hn0 : n = 0
⊢ HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1
have pos : LE.le (α := ℝ) 0 1
Tactic: rw [hn0, cast_zero, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
n : ℕ
hn0 : ¬n = 0
⊢ HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1
have neg : mu μ hn n ≤ n
Tactic: rw [div_le_one (cast_pos.mpr (Nat.pos_of_ne_zero hn0)), cast_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
⊢ BddBelow (α := ℝ)
    {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 ℝ)
  (lowerBounds
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a})
  0
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 : ℕ → ℕ
x : R
ψ : ℕ → ℕ
⊢ 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
have 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
Tactic: simp only [mem_lowerBounds, eventually_map, eventually_atTop, ge_iff_le, Set.mem_setOf_eq,
    forall_exists_index]
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ BddAbove (α := ℝ)
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
have hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
Tactic: have hψ : ∀ n, 0 ≤ 1 / (ψ n : ℝ) := fun _ ↦ by simp only [one_div, inv_nonneg, cast_nonneg]
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
⊢ BddAbove (α := ℝ)
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
have pos : ∀ (hx : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)),
  BddAbove (α := ℝ)
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
Tactic: by_cases! hx : μ x ≤ 1
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
pos :
  ∀ (hx : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)),
    BddAbove (α := ℝ)
      (Set.range fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
⊢ BddAbove (α := ℝ)
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
have neg : ∀ (hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)),
  BddAbove (α := ℝ)
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
Tactic: by_cases! hx : μ x ≤ 1
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
⊢ BddAbove (α := ℝ)
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
have h : Membership.mem (γ := Set ℝ)
  (upperBounds
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))))
  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
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
⊢ Membership.mem (γ := Set ℝ)
    (upperBounds
      (Set.range fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))))
    1
have h : ∀ (x_1 : ℝ) (x_2 : ℕ)
  (h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ x_2)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_2) : ℝ)) = x_1), x_1 ≤ 1
Tactic: simp only [mem_upperBounds, Set.mem_range, forall_exists_index]
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
n : ℕ
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) ≤ 1
have h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ n)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ) ≤ 1
Tactic: apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
n : ℕ
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ n)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ) ≤ 1
have h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤ 1
Tactic: rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
⊢ BddAbove (α := ℝ)
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
have h : Membership.mem (α := ℝ) (γ := Set ℝ)
  (upperBounds
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))))
  ((μ : (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
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
⊢ Membership.mem (α := ℝ) (γ := Set ℝ)
    (upperBounds
      (Set.range fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))))
    ((μ : (a : R) → ℝ) x : ℝ)
have h : ∀ (x_1 : ℝ) (x_2 : ℕ)
  (h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ x_2)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_2) : ℝ)) = x_1),
  x_1 ≤ (μ : (a : R) → ℝ) x
Tactic: simp only [mem_upperBounds, Set.mem_range, forall_exists_index]
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
n : ℕ
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) ≤ (μ : (a : R) → ℝ) x
have h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ n)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ) ≤ (μ : (a : R) → ℝ) x
Tactic: apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
n : ℕ
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ n)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ) ≤ (μ : (a : R) → ℝ) x
have h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤ (μ : (a : R) → ℝ) x
Tactic: rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
n : ℕ
| (μ : (a : R) → ℝ) x
have rw : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1
Tactic: rw [← rpow_one (μ x)]
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
n : ℕ
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤ (μ : (a : R) → ℝ) x
have h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1
Tactic: conv_rhs => rw [← rpow_one (μ x)]
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
n : ℕ
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤
    HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1
have h : HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ) ≤ 1
Tactic: rw [rpow_le_rpow_left_iff hx]
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ BddAbove (α := ℝ)
    ((fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))) ''
      Set.univ)
have rw : BddAbove (α := ℝ)
  (Set.range fun (x_1 : (↑Set.univ : Type)) ↦
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ (↑x_1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑x_1 : ℕ)) : ℝ)))
Tactic: rw [Set.image_eq_range]
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ BddAbove (α := ℝ)
    (Set.range fun (x_1 : (↑Set.univ : Type)) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ (↑x_1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑x_1 : ℕ)) : ℝ)))
have h : Eq (α := Set ℝ)
  (Set.range fun (x_1 : (↑Set.univ : Type)) ↦
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ (↑x_1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑x_1 : ℕ)) : ℝ)))
  (Set.range fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
Tactic: convert! μ_bddAbove μ hμ1 hs x ψ
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ Eq (α := Set ℝ)
    (Set.range fun (x_1 : (↑Set.univ : Type)) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ (↑x_1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑x_1 : ℕ)) : ℝ)))
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
have h : ∀ (x_1 : ℝ),
  Membership.mem (γ := Set ℝ)
      (Set.range fun (x_2 : (↑Set.univ : Type)) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ (↑x_2 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑x_2 : ℕ)) : ℝ)))
      x_1 ↔
    Membership.mem (γ := Set ℝ)
      (Set.range fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      x_1
Tactic: ext
-- 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
ψ : ℕ → ℕ
⊢ Set.Nonempty (α := ℝ)
    {a : ℝ |
      ∀ᶠ (n : ℝ) in
        map
          (fun (n : ℕ) ↦
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ n)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
          atTop,
        n ≤ a}
have 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}
Tactic: by_cases hμx : μ x < 1