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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h1 : Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
neg : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n * 1) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
neg₁ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n) ((μ : (a : R) → ℝ) 1 : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₂ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ)) ((μ : (a : R) → ℝ) 1 : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₃ :
  (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) * 1) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have neg₄ : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
Tactic: rw [← mul_one (x ^ n), pow_mul_apply_eq_pow_mul μ hx, ← rpow_natCast, h1, mul_one,
      ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]
-- 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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h1 : Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
neg : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n * 1) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
neg₁ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n) ((μ : (a : R) → ℝ) 1 : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₂ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ)) ((μ : (a : R) → ℝ) 1 : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₃ :
  (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) * 1) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₄ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have neg₅ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
Tactic: rw [← mul_one (x ^ n), pow_mul_apply_eq_pow_mul μ hx, ← rpow_natCast, h1, mul_one,
      ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]
-- 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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h1 : Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
neg : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n * 1) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
neg₁ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n) ((μ : (a : R) → ℝ) 1 : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₂ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ)) ((μ : (a : R) → ℝ) 1 : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₃ :
  (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) * 1) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₄ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
neg₅ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have neg₆ : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1 = (μ : (a : R) → ℝ) x
Tactic: rw [← mul_one (x ^ n), pow_mul_apply_eq_pow_mul μ hx, ← rpow_natCast, h1, mul_one,
      ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]
-- 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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h1 : Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
neg : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n * 1) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
neg₁ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n) ((μ : (a : R) → ℝ) 1 : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₂ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ)) ((μ : (a : R) → ℝ) 1 : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₃ :
  (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) * 1) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₄ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
neg₅ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
neg₆ : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1 = (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have neg₇ : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
Tactic: rw [← mul_one (x ^ n), pow_mul_apply_eq_pow_mul μ hx, ← rpow_natCast, h1, mul_one,
      ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]
-- 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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
⊢ Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
    (𝓝 (smoothingFun μ x * smoothingFun μ y))
have rw : Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
  (𝓝 (HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingFun μ y)))
Tactic: rw [smoothingFun_apply_of_map_mul_eq_mul μ hμ1 hx]
-- 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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
⊢ smoothingFun μ (x * y) = smoothingFun μ x * smoothingFun μ y
have hlim : Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
  (𝓝 (smoothingFun μ x * smoothingFun μ y))
Tactic: have hlim : Tendsto (fun n => μ x * smoothingSeminormSeq μ y n) atTop
      (𝓝 (smoothingFun μ x * smoothingFun μ y)) := by
    rw [smoothingFun_apply_of_map_mul_eq_mul μ hμ1 hx]
    exact Tendsto.const_mul _ (tendsto_smoothingFun_of_map_one_le_one μ hμ1 y)
-- 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 :
  ∀ (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))
⊢ smoothingFun μ (x * y) = smoothingFun μ x * smoothingFun μ y
have apply : smoothingSeminormSeq μ (x * y) =ᶠ[atTop] fun (n : ℕ) ↦
  HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)
Tactic: apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 (x * y))
    hlim
-- 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 :
  ∀ (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))
⊢ smoothingSeminormSeq μ (x * y) =ᶠ[atTop] fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)
have simp : ∃ (a : ℕ),
  ∀ (b : ℕ),
    a ≤ b → smoothingSeminormSeq μ (x * y) b = HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y b)
Tactic: simp only [EventuallyEq, eventually_atTop, ge_iff_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 :
  ∀ (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))
⊢ ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b →
        smoothingSeminormSeq μ (x * y) b = HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y b)
have h : ∀ (b : ℕ),
  1 ≤ b → smoothingSeminormSeq μ (x * y) b = HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y b)
Tactic: use 1
-- 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 :
  ∀ (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
⊢ smoothingSeminormSeq μ (x * y) n = HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)
have hn0 : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (_root_.ne_of_gt (lt_of_lt_of_le zero_lt_one hn1))
-- 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 :
  ∀ (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
⊢ 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 : ℝ)))
have 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 : ℝ)))
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]
-- 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 :
  ∀ (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 : ℝ)))
⊢ 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 : ℝ)))
have 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 : ℝ)))
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]
-- 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 :
  ∀ (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 : ℝ)))
⊢ 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 : ℝ)))
have 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 : ℝ)))
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]
-- 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 :
  ∀ (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 : ℝ)))
⊢ 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 : ℝ)))
have 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 : ℝ)))
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]
-- 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 :
  ∀ (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 : ℝ)))
⊢ 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 : ℝ)))
have 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 : ℝ)))
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]
-- 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 :
  ∀ (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 : ℝ)))
⊢ 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 : ℝ)))
have 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 : ℝ)))
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]