awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
h1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
h2 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h3 :
  (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
    L + ε
h4 : 0 < HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
h5 : 0 < (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ)
        ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
(mul_rpow (apply_nonneg μ _) (apply_nonneg μ _))

Premises used: Real.mul_rpow, 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 : ℝ)
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
h1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
h2 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h3 :
  (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
    L + ε
h4 : 0 < HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
h5 : 0 < (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
ha : 0 ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
h1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
h2 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h3 :
  (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
    L + ε
h4 : 0 < HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
h5 : 0 < (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
ha : 0 < HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
h1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
h2 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h3 :
  (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
    L + ε
h4 : 0 < HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
h5 : 0 < (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
ha : 0 ≤ (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
⊢ (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
h1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
h2 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h3 :
  (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
    L + ε
h4 : 0 < HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
h5 : 0 < (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
⊢ (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
    L + ε

Tactic:
h3
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
pos :
  ∀ (hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)),
    Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))
neg :
  ∀ (hx : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)),
    Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
by_cases hx : μ x = 0

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 : ℝ)
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
tendsto_smoothingFun_of_eq_zero μ hx

Premises used: tendsto_smoothingFun_of_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
exact tendsto_smoothingFun_of_eq_zero μ hx

Premises used: tendsto_smoothingFun_of_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
tendsto_smoothingFun_of_ne_zero μ hμ1 hx

Premises used: tendsto_smoothingFun_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
exact tendsto_smoothingFun_of_ne_zero μ hμ1 hx

Premises used: tendsto_smoothingFun_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
apply : ∀ᶠ (c : ℕ) in atTop, 0 ≤ smoothingSeminormSeq μ x c
⊢ 0 ≤ smoothingFun μ x

Tactic:
apply ge_of_tendsto (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)

Premises used: ge_of_tendsto, tendsto_smoothingFun_of_map_one_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
x_1 : ℕ
h : 1 ≤ x_1
⊢ 0 ≤ smoothingSeminormSeq μ x x_1

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
⊢ ∀ᶠ (c : ℕ) in atTop, 0 ≤ smoothingSeminormSeq μ x c

Tactic:
simpa [eventually_atTop, ge_iff_le] using ⟨1, fun _ _ ↦ by positivity⟩

Premises used: ge_iff_le, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
apply : ∀ᶠ (c : ℕ) in atTop, smoothingSeminormSeq μ 1 c ≤ 1
⊢ smoothingFun μ 1 ≤ 1

Tactic:
apply le_of_tendsto (tendsto_smoothingFun_of_map_one_le_one μ hμ1 (1 : R))

Premises used: le_of_tendsto, tendsto_smoothingFun_of_map_one_le_one, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ 1 b ≤ 1
⊢ ∀ᶠ (c : ℕ) in atTop, smoothingSeminormSeq μ 1 c ≤ 1

Tactic:
simp only [eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
h : ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ 1 b ≤ 1
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ 1 b ≤ 1

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 : ℝ)
n : ℕ
hn : 1 ≤ n
h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤ 1
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) 1 n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤ 1

Tactic:
rw [one_pow]

Premises used: one_pow
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
n : ℕ
hn : 1 ≤ n
rw : HPow.hPow (α := ℝ) 1 (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
| 1

Tactic:
rw [← one_rpow (1 / n : ℝ)]

Premises used: HDiv.hDiv, Real.one_rpow, Nat.cast, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
n : ℕ
hn : 1 ≤ n
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) 1 (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤ 1

Tactic:
conv_rhs => rw [← one_rpow (1 / n : ℝ)]

Premises used: HDiv.hDiv, Real.one_rpow, Nat.cast, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
n : ℕ
hn : 1 ≤ n
apply : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ 0 < HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
apply _root_.div_pos zero_lt_one

Premises used: zero_lt_one, div_pos
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
n : ℕ
hn : 1 ≤ n
rw : 0 < n
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
rw [← cast_zero, cast_lt]

Premises used: Nat.cast_zero, Nat.cast_lt
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ 0 < n

Tactic:
succ_le_iff.mp hn

Premises used: Iff.mp, Nat.succ_le_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 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ 0 < n

Tactic:
exact succ_le_iff.mp hn

Premises used: Iff.mp, Nat.succ_le_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 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ 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
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
n : ℕ
hn : 1 ≤ n
hn1 : 0 < HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) 1 (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
(rpow_le_rpow_iff (apply_nonneg μ _) zero_le_one hn1).mpr hμ1

Premises used: Iff.mpr, zero_le_one, Real.rpow_le_rpow_iff, 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 : ℝ)
n : ℕ
hn : 1 ≤ n
hn1 : 0 < HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) 1 (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
exact (rpow_le_rpow_iff (apply_nonneg μ _) zero_le_one hn1).mpr hμ1

Premises used: Iff.mpr, zero_le_one, Real.rpow_le_rpow_iff, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
n : ℕ+
⊢ smoothingFun μ x ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))

Tactic:
ciInf_le (smoothingSeminormSeq_bddBelow μ x) _

Premises used: ciInf_le, smoothingSeminormSeq_bddBelow
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
apply :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑1 : ℕ) : ℝ)) ≤ (μ : (a : R) → ℝ) x
⊢ smoothingFun μ x ≤ (μ : (a : R) → ℝ) x

Tactic:
apply (smoothingFun_le μ x 1).trans

Premises used: smoothingFun_le, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
rw₄ rw₅ : LE.le (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑1 : ℕ) : ℝ)) ≤ (μ : (a : R) → ℝ) x

Tactic:
rw [PNat.one_coe, pow_one, cast_one, div_one, rpow_one]

Premises used: PNat.one_coe, Real.rpow_one, pow_one, div_one, Nat.cast_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 : ℕ
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ mu μ hn n) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - mu μ hn n)) : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
(Classical.choose_spec (hn n)).2

Premises used: _private.0.mu, Classical.choose_spec, And.right
-- 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 : ℕ
⊢ mu μ hn n ≤ n

Tactic:
simpa [mu] using (Classical.choose_spec (hn n)).1

Premises used: _private.0.mu, Classical.choose_spec, And.left