-- 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 : ℝ))
calc :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ))) * x ^ (n % (↑m1 : ℕ))) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
calc₁ :
  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 : ℝ))
calc₂ :
  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 : ℝ))
calc₃ :
  (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 : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) <
    L + ε

Tactic:
calc μ (x ^ ((m1 : ℕ) * (n / (m1 : ℕ)) + n % m1)) ^ (1 / (n : ℝ)) =
          μ (x ^ ((m1 : ℕ) * (n / (m1 : ℕ))) * x ^ (n % m1)) ^ (1 / (n : ℝ)) := by rw [pow_add]
      _ ≤ (μ (x ^ ((m1 : ℕ) * (n / (m1 : ℕ)))) * μ (x ^ (n % m1))) ^ (1 / (n : ℝ)) :=
        (rpow_le_rpow (apply_nonneg μ _) (map_mul_le_mul μ _ _) (one_div_cast_nonneg _))
      _ = μ (x ^ ((m1 : ℕ) * (n / (m1 : ℕ)))) ^ (1 / (n : ℝ)) *
          μ (x ^ (n % m1)) ^ (1 / (n : ℝ)) :=
        (mul_rpow (apply_nonneg μ _) (apply_nonneg μ _))
      _ ≤ (μ (x ^ (m1 : ℕ)) ^ (n / (m1 : ℕ))) ^ (1 / (n : ℝ)) *
            μ (x ^ (n % m1)) ^ (1 / (n : ℝ)) := by gcongr
      _ < (L + ε / 2) * (L + ε / 2) ^ (-(((n % m1 : ℕ) : ℝ) / (n : ℝ))) *
            μ (x ^ (n % m1)) ^ (1 / (n : ℝ)) := by gcongr
      _ ≤ (L + ε / 2) * (L + ε / 2) ^ (-(((n % m1 : ℕ) : ℝ) / (n : ℝ))) *
            (μ x ^ (n % m1)) ^ (1 / (n : ℝ)) := by gcongr
      _ ≤ L + ε := h3

Premises used: PNat.val, HMul.hMul, Real.mul_rpow, HDiv.hDiv, Nat.cast, HMod.hMod, HPow.hPow, HAdd.hAdd, Nat.one_div_cast_nonneg, Real.rpow_le_rpow, NonnegHomClass.apply_nonneg, OfNat.ofNat, DFunLike.coe, Neg.neg, SubmultiplicativeHomClass.map_mul_le_mul