awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ℝ))

Tactic:
Set.mem_Icc.mpr ⟨div_nonneg (cast_nonneg (mu μ hn n)) (cast_nonneg n), ?_⟩

Premises used: Iff.mpr, Nat.cast_nonneg, _private.0.mu, And.intro, Set.mem_Icc, div_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ℕ
refine : HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1
⊢ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ))

Tactic:
refine Set.mem_Icc.mpr ⟨div_nonneg (cast_nonneg (mu μ hn n)) (cast_nonneg n), ?_⟩

Premises used: Iff.mpr, And.intro, Set.mem_Icc, div_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
neg : ∀ (hn0 : ¬n = 0), HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1
⊢ HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1

Tactic:
by_cases hn0 : n = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
pos : LE.le (α := ℝ) 0 1
⊢ HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1

Tactic:
rw [hn0, cast_zero, div_zero]

Premises used: Nat.cast_zero, div_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
⊢ LE.le (α := ℝ) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
neg : mu μ hn n ≤ n
⊢ HDiv.hDiv (α := ℝ) (↑(mu μ hn n) : ℝ) (↑n : ℝ) ≤ 1

Tactic:
rw [div_le_one (cast_pos.mpr (Nat.pos_of_ne_zero hn0)), cast_le]

Premises used: Iff.mpr, Nat.cast_pos, div_le_one, Nat.pos_of_ne_zero, Nat.cast_le
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
⊢ mu μ hn n ≤ n

Tactic:
mu_le _ _ _

Premises used: _private.0.mu_le
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
⊢ mu μ hn n ≤ n

Tactic:
exact mu_le _ _ _

Premises used: _private.0.mu_le
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
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
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
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
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
r : ℝ
m : ℕ
hm :
  ∀ (b : ℕ),
    m ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ r
⊢ 0 ≤ r

Tactic:
le_trans (rpow_nonneg (apply_nonneg μ _) _) (hm m (le_refl _))

Premises used: le_refl, Real.rpow_nonneg, NonnegHomClass.apply_nonneg, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
r : ℝ
m : ℕ
hm :
  ∀ (b : ℕ),
    m ≤ b → HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑(s (ψ b)) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(ψ b) : ℝ)) ≤ r
⊢ 0 ≤ r

Tactic:
exact le_trans (rpow_nonneg (apply_nonneg μ _) _) (hm m (le_refl _))

Premises used: le_refl, Real.rpow_nonneg, NonnegHomClass.apply_nonneg, 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
x_1 : ℕ
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ x_1) : ℝ)

Tactic:
simp only [one_div, inv_nonneg, cast_nonneg]

Premises used: Nat.cast_nonneg, inv_nonneg, one_div
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)

Tactic:
have hψ : ∀ n, 0 ≤ 1 / (ψ n : ℝ) := fun _ ↦ by simp only [one_div, inv_nonneg, cast_nonneg]
-- 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 : ∀ (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) : ℝ)))
neg :
  ∀ (hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)),
    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) : ℝ)))

Tactic:
by_cases! hx : μ x ≤ 1

Premises used: 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
h :
  Membership.mem (γ := Set ℝ)
    (upperBounds
      (Set.range fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))))
    1
⊢ BddAbove (α := ℝ)
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))

Tactic:
use 1
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
h :
  ∀ (x_1 : ℝ) (x_2 : ℕ)
    (h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ x_2)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ x_2) : ℝ)) = x_1),
    x_1 ≤ 1
⊢ Membership.mem (γ := Set ℝ)
    (upperBounds
      (Set.range fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))))
    1

Tactic:
simp only [mem_upperBounds, Set.mem_range, forall_exists_index]

Premises used: Set.mem_range, forall_exists_index, mem_upperBounds
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
n : ℕ
h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ n)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ) ≤ 1
⊢ 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))

Premises used: map_pow_le_pow', Real.rpow_le_rpow, NonnegHomClass.apply_nonneg, 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
n : ℕ
h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤ 1
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ n)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ) ≤ 1

Tactic:
rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]

Premises used: mul_one_div, 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 : ∀ (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 : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤ 1

Tactic:
rpow_le_one (apply_nonneg _ _) hx (div_nonneg (cast_nonneg _) (cast_nonneg _))

Premises used: Nat.cast_nonneg, Real.rpow_le_one, div_nonneg, NonnegHomClass.apply_nonneg
-- 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 : ∀ (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 : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤ 1

Tactic:
exact rpow_le_one (apply_nonneg _ _) hx (div_nonneg (cast_nonneg _) (cast_nonneg _))

Premises used: Nat.cast_nonneg, Real.rpow_le_one, div_nonneg, NonnegHomClass.apply_nonneg
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
h :
  Membership.mem (α := ℝ) (γ := Set ℝ)
    (upperBounds
      (Set.range fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))))
    ((μ : (a : R) → ℝ) x : ℝ)
⊢ BddAbove (α := ℝ)
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))

Tactic:
use μ x

Premises used: 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
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
⊢ Membership.mem (α := ℝ) (γ := Set ℝ)
    (upperBounds
      (Set.range fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))))
    ((μ : (a : R) → ℝ) x : ℝ)

Tactic:
simp only [mem_upperBounds, Set.mem_range, forall_exists_index]

Premises used: Set.mem_range, forall_exists_index, mem_upperBounds
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
n : ℕ
h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ n)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ) ≤ (μ : (a : R) → ℝ) x
⊢ 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))

Premises used: map_pow_le_pow', Real.rpow_le_rpow, NonnegHomClass.apply_nonneg, 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
n : ℕ
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤ (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (s (ψ n)) ^ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ) ≤ (μ : (a : R) → ℝ) x

Tactic:
rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]

Premises used: mul_one_div, 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
n : ℕ
rw : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1
| (μ : (a : R) → ℝ) x

Tactic:
rw [← 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
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 : ℕ
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤
    HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤ (μ : (a : R) → ℝ) x

Tactic:
conv_rhs => rw [← 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
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 : ℕ
h : HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ) ≤ 1
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ)) ≤
    HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1

Tactic:
rw [rpow_le_rpow_left_iff hx]

Premises used: Real.rpow_le_rpow_left_iff
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)
hx : LT.lt (α := ℝ) (1 : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ) ≤ 1

Tactic:
div_le_one_of_le₀ (cast_le.mpr (hs (ψ n))) (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
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 : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ) ≤ 1

Tactic:
exact div_le_one_of_le₀ (cast_le.mpr (hs (ψ n))) (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
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
rw :
  BddAbove (α := ℝ)
    (Set.range fun (x_1 : (↑Set.univ : Type)) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ (↑x_1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑x_1 : ℕ)) : ℝ)))
⊢ BddAbove (α := ℝ)
    ((fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))) ''
      Set.univ)

Tactic:
rw [Set.image_eq_range]

Premises used: Set.image_eq_range
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ BddAbove (α := ℝ)
    (Set.range fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))

Tactic:
μ_bddAbove μ hμ1 hs x ψ

Premises used: _private.0.μ_bddAbove
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
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) : ℝ)))
⊢ BddAbove (α := ℝ)
    (Set.range fun (x_1 : (↑Set.univ : Type)) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ (↑x_1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑x_1 : ℕ)) : ℝ)))

Tactic:
convert! μ_bddAbove μ hμ1 hs x ψ

Premises used: _private.0.μ_bddAbove
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
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
⊢ 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:
ext
-- 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 : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
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:
simp [one_div, Set.mem_range, Subtype.exists, Set.mem_univ, exists_const]

Premises used: Set.mem_range, Subtype.exists, one_div, exists_const, Set.mem_univ
-- 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
ψ : ℕ → ℕ
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}
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}
⊢ 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

Premises used: DFunLike.coe