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
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
hxn : Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) < L + ε
have pos : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) <
  L + ε
Tactic: nth_rw 1 [← div_add_mod n m1]
-- 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
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) <
    L + ε
have hLε : 0 < L + ε
Tactic: have hLε : 0 < L + ε := add_pos_of_nonneg_of_pos hL0 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
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
hxn : Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hLε : 0 < L + ε
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) <
    L + ε
have apply : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
  0
Tactic: apply lt_of_le_of_lt _ hLε
-- 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
hxn : Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hLε : 0 < L + ε
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    0
have rw : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ))) * x ^ (n % (↑m1 : ℕ))) : ℝ)
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ)
      ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) ^
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: rw [pow_add, ← MulZeroClass.mul_zero (μ (x ^ ((m1 : ℕ) * (n / (m1 : ℕ)))) ^ (1 / (n : ℝ))),
      ← zero_rpow (one_div_cast_ne_zero (pos_iff_ne_zero.mp hn0)), ← hxn,
      ← mul_rpow (apply_nonneg μ _) (apply_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 : ℝ)
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
hxn : Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hLε : 0 < L + ε
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ))) * x ^ (n % (↑m1 : ℕ))) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ)
        ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have h₁ : (μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ))) * x ^ (n % (↑m1 : ℕ))) ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ)
    ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
Tactic: gcongr
-- 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
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
⊢ smoothingSeminormSeq μ x n < L + ε
have hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
Tactic: have hxn' : 0 < μ (x ^ (n % ↑m1)) := lt_of_le_of_ne (apply_nonneg _ _) (Ne.symm hxn)
-- 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
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) < L + ε
have neg : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) <
  L + ε
Tactic: nth_rw 1 [← div_add_mod n m1]
-- 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
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have h₁ : (μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) ≤
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ))
Tactic: gcongr
-- 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
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
⊢ (μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ))
have h₁ : (μ : (a : R) → ℝ) ((x ^ (↑m1 : ℕ)) ^ (n / (↑m1 : ℕ))) ≤
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ))
Tactic: rw [pow_mul]
-- 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
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) <
    L + ε
have h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: have h : μ (x ^ ((m1 : ℕ) * (n / (m1 : ℕ)))) ^ (1 / (n : ℝ)) ≤
        (μ (x ^ (m1 : ℕ)) ^ (n / (m1 : ℕ))) ^ (1 / (n : ℝ)) := by
      gcongr
      rw [pow_mul]
      exact map_pow_le_pow μ (x ^ (m1 : ℕ))
        (pos_iff_ne_zero.mp (Nat.div_pos (le_trans (le_max_left (m1 : ℕ) m2) hn) (PNat.pos m1)))
-- 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
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) <
    L + ε
have hL0' : 0 < L + ε / 2
Tactic: have hL0' : 0 < L + ε / 2 := add_pos_of_nonneg_of_pos hL0 (half_pos hε)
-- 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
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
have hm10 : Ne (α := ℝ) (↑(↑m1 : ℕ) : ℝ) 0
Tactic: have hm10 : (m1 : ℝ) ≠ 0 := cast_ne_zero.mpr (_root_.ne_of_gt (PNat.pos m1))
-- 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
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
hm10 : Ne (α := ℝ) (↑(↑m1 : ℕ) : ℝ) 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
have rw : ∀ (hm1 : (μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) < HPow.hPow (β := ℝ) (L + ε / 2) (↑(↑m1 : ℕ) : ℝ)) (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)
  (hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ))
  (hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ))
  (h :
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
  (hL0' : 0 < L + ε / 2) (hm10 : Ne (α := ℝ) (↑(↑m1 : ℕ) : ℝ) 0),
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
Tactic: rw [← rpow_lt_rpow_iff (rpow_nonneg (apply_nonneg μ _) _) (le_of_lt hL0')
        (cast_pos.mpr (PNat.pos m1)), ← rpow_mul (apply_nonneg μ _), one_div_mul_cancel hm10,
        rpow_one] at hm1
Cleared hypotheses: hm1, m2, hm2, n, hn, hn0, hL_le, hxn, hxn', h, hL0', hm10
-- 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 : (μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) < HPow.hPow (β := ℝ) (L + ε / 2) (↑(↑m1 : ℕ) : ℝ)
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
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
hm10 : Ne (α := ℝ) (↑(↑m1 : ℕ) : ℝ) 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
have nth_rw : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
  HPow.hPow (β := ℝ) (L + ε / 2) 1 * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
Tactic: nth_rw 1 [← rpow_one (L + ε / 2)]