-- 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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
hlim :
  Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
    (𝓝 (smoothingFun μ x * smoothingFun μ y))
n : ℕ
hn1 : 1 ≤ n
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n * y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
h₁ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
h₂ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
h₃ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
h₄ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
h₅ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1 *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
h₆ h₇ :
  HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x * y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))

Tactic:
rw [mul_pow, pow_mul_apply_eq_pow_mul μ hx, mul_rpow (pow_nonneg (apply_nonneg μ _) _)
    (apply_nonneg μ _), ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0,
    rpow_one]

Premises used: pow_nonneg, Real.mul_rpow, pow_mul_apply_eq_pow_mul, Real.rpow_one, mul_one_div_cancel, NonnegHomClass.apply_nonneg, Real.rpow_mul, mul_pow, DFunLike.coe, Real.rpow_natCast