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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
hε2 : 0 < ε / 2
hL2 :
  ∀ ε_1 > 0,
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist
            ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
            1 <
          ε_1
⊢ ∃ (m : ℕ),
    ∀ n ≥ m,
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
          1 ≤
        ε / (2 * (L + ε / 2))
have set : let δ := ε / (2 * (L + ε / 2));
∀ (hδ_def : δ = ε / (2 * (L + ε / 2))),
  ∃ (m : ℕ),
    ∀ n ≥ m,
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
          1 ≤
        δ
Tactic: set δ : ℝ := ε / (2 * (L + ε / 2)) with hδ_def
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
hε2 : 0 < ε / 2
hL2 :
  ∀ ε_1 > 0,
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist
            ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
            1 <
          ε_1
δ : ℝ := ε / (2 * (L + ε / 2))
hδ_def : δ = ε / (2 * (L + ε / 2))
⊢ 0 < δ
have rw : 0 < ε / 2 * (1 / (L + ε / 2))
Tactic: rw [hδ_def, div_mul_eq_div_mul_one_div]
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
hε2 : 0 < ε / 2
hL2 :
  ∀ ε_1 > 0,
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist
            ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
            1 <
          ε_1
δ : ℝ := ε / (2 * (L + ε / 2))
hδ_def : δ = ε / (2 * (L + ε / 2))
⊢ ∃ (m : ℕ),
    ∀ n ≥ m,
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
          1 ≤
        δ
have hδ : 0 < δ
Tactic: have hδ : 0 < δ := by
      rw [hδ_def, div_mul_eq_div_mul_one_div]
      exact mul_pos hε2
        ((one_div (L + ε / 2)).symm ▸ inv_pos_of_pos (add_pos_of_nonneg_of_pos hL0 hε2))
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
hε2 : 0 < ε / 2
hL2 :
  ∀ ε_1 > 0,
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist
            ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
            1 <
          ε_1
δ : ℝ := ε / (2 * (L + ε / 2))
hδ_def : δ = ε / (2 * (L + ε / 2))
hδ : 0 < δ
⊢ ∃ (m : ℕ),
    ∀ n ≥ m,
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
          1 ≤
        δ
have obtain : ∀ (N : ℕ)
  (hN :
    ∀ n ≥ N,
      dist
          ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
          1 <
        δ),
  ∃ (m : ℕ),
    ∀ n ≥ m,
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
          1 ≤
        δ
Tactic: obtain ⟨N, hN⟩ := hL2 δ hδ
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
hε2 : 0 < ε / 2
hL2 :
  ∀ ε_1 > 0,
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist
            ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
            1 <
          ε_1
δ : ℝ := ε / (2 * (L + ε / 2))
hδ_def : δ = ε / (2 * (L + ε / 2))
hδ : 0 < δ
N : ℕ
hN :
  ∀ n ≥ N,
    dist
        ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
        1 <
      δ
⊢ ∃ (m : ℕ),
    ∀ n ≥ m,
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
          1 ≤
        δ
have h : ∀ n ≥ N,
  (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
      1 ≤
    δ
Tactic: use N
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
hε2 : 0 < ε / 2
hL2 :
  ∀ ε_1 > 0,
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist
            ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
            1 <
          ε_1
δ : ℝ := ε / (2 * (L + ε / 2))
hδ_def : δ = ε / (2 * (L + ε / 2))
hδ : 0 < δ
N : ℕ
hN :
  ∀ n ≥ N,
    dist
        ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
        1 <
      δ
n : ℕ
hn : n ≥ N
⊢ (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
      1 ≤
    δ
have hN₁ : dist
    ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
    1 <
  δ
Tactic: specialize hN n hn
Cleared hypotheses: hN
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
hε2 : 0 < ε / 2
hL2 :
  ∀ ε_1 > 0,
    ∃ (N : ℕ),
      ∀ n ≥ N,
        dist
            ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
              HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
            1 <
          ε_1
δ : ℝ := ε / (2 * (L + ε / 2))
hδ_def : δ = ε / (2 * (L + ε / 2))
hδ : 0 < δ
N n : ℕ
hn : n ≥ N
hN :
  dist
      ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
      1 <
    δ
⊢ (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
      1 ≤
    δ
have hN₁ : -δ <
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
      1 ∧
  (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
      1 <
    δ
Tactic: rw [Real.dist_eq, abs_lt] at hN
Cleared hypotheses: hN
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
⊢ ∃ (N : ℕ), ∀ n ≥ N, dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε
have obtain : ∀ (m2 : ℕ)
  (hm2 :
    ∀ n ≥ m2,
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
          1 ≤
        ε / (2 * (L + ε / 2))),
  ∃ (N : ℕ), ∀ n ≥ N, dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε
Tactic: obtain ⟨m2, hm2⟩ : ∃ m : ℕ, ∀ n ≥ m,
      (L + ε / 2) ^ (-(((n % m1 : ℕ) : ℝ) / (n : ℝ))) * (μ x ^ (n % m1)) ^ (1 / (n : ℝ)) - 1 ≤
      ε / (2 * (L + ε / 2)) := by
    have hε2 : 0 < ε / 2 := half_pos hε
    have hL2 := smoothingSeminormSeq_tendsto_aux μ hL0 hε2 (PNat.pos m1) hx
    rw [Metric.tendsto_atTop] at hL2
    set δ : ℝ := ε / (2 * (L + ε / 2)) with hδ_def
    have hδ : 0 < δ := by
      rw [hδ_def, div_mul_eq_div_mul_one_div]
      exact mul_pos hε2
        ((one_div (L + ε / 2)).symm ▸ inv_pos_of_pos (add_pos_of_nonneg_of_pos hL0 hε2))
    obtain ⟨N, hN⟩ := hL2 δ hδ
    use N
    intro n hn
    specialize hN n hn
    rw [Real.dist_eq, abs_lt] at hN
    exact le_of_lt hN.right
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
⊢ ∃ (N : ℕ), ∀ n ≥ N, dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε
have h : ∀ n ≥ max (↑m1 : ℕ) m2, dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε
Tactic: use max (m1 : ℕ) m2
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
⊢ dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε
have hn0 : 0 < n
Tactic: have hn0 : 0 < n := lt_of_lt_of_le (lt_of_lt_of_le (PNat.pos m1) (le_max_left (m1 : ℕ) m2)) hn
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
⊢ dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε
have h : -ε < smoothingSeminormSeq μ x n - smoothingFun μ x ∧ smoothingSeminormSeq μ x n - smoothingFun μ x < ε
Tactic: rw [Real.dist_eq, abs_lt]
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
⊢ L ≤ smoothingSeminormSeq μ x n
have rw : L ≤ smoothingSeminormSeq μ x (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn0) : ℕ)
Tactic: rw [← PNat.mk_coe n hn0]
-- 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
⊢ -ε < smoothingSeminormSeq μ x n - smoothingFun μ x ∧ smoothingSeminormSeq μ x n - smoothingFun μ x < ε
have hL_le : L ≤ smoothingSeminormSeq μ x n
Tactic: have hL_le : L ≤ smoothingSeminormSeq μ x n := by
    rw [← PNat.mk_coe n hn0]
    apply ciInf_le (smoothingSeminormSeq_bddBelow μ 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
⊢ -ε < smoothingSeminormSeq μ x n - smoothingFun μ x ∧ smoothingSeminormSeq μ x n - smoothingFun μ x < ε
have h : smoothingSeminormSeq μ x n - smoothingFun μ x < ε
Tactic: refine ⟨lt_of_lt_of_le (neg_lt_zero.mpr hε) (sub_nonneg.mpr hL_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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
⊢ smoothingSeminormSeq μ x n - smoothingFun μ x < ε
have h : smoothingSeminormSeq μ x n < L + ε
Tactic: suffices h : smoothingSeminormSeq μ x n < L + ε by rwa [tsub_lt_iff_left hL_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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
⊢ smoothingSeminormSeq μ x n < L + ε
have pos : ∀ (hxn : Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)), smoothingSeminormSeq μ x n < L + ε
Tactic: by_cases hxn : μ (x ^ (n % m1)) = 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 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
pos : ∀ (hxn : Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)), smoothingSeminormSeq μ x n < L + ε
⊢ smoothingSeminormSeq μ x n < L + ε
have neg : ∀ (hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)), smoothingSeminormSeq μ x n < L + ε
Tactic: by_cases hxn : μ (x ^ (n % m1)) = 0