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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n_1 : R
n : ℕ+
hneg : HPow.hPow (α := R) (-1) (↑n : ℕ) = -1
e_s :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (-1 * n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
e_s₁ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (-n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) (-1) (↑n : ℕ) * n_1 ^ (↑n : ℕ)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
have e_s₂ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
Tactic: rw [hneg, neg_one_mul, map_neg_eq_map μ]
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
⊢ smoothingFun μ (x * y) ≤ smoothingFun μ x * smoothingFun μ y
have apply : ∀ (x_1 : ℕ), smoothingSeminormSeq μ (x * y) x_1 ≤ smoothingSeminormSeq μ x x_1 * smoothingSeminormSeq μ y x_1
Tactic: apply le_of_tendsto_of_tendsto' (tendsto_smoothingFun_of_map_one_le_one μ hμ1 (x * y))
      (Tendsto.mul (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)
        (tendsto_smoothingFun_of_map_one_le_one μ hμ1 y))
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
n : ℕ
⊢ smoothingSeminormSeq μ (x * y) n ≤ smoothingSeminormSeq μ x n * smoothingSeminormSeq μ y n
have hn : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: have hn : 0 ≤ 1 / (n : ℝ) := by simp only [one_div, inv_nonneg, cast_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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
n : ℕ
hn : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x * y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n * y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) ^
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: rw [← mul_rpow (apply_nonneg μ _) (apply_nonneg μ _), mul_pow]
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
n : ℕ
hn : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n * y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have h₁ : (μ : (a : R) → ℝ) (x ^ n * y ^ n) ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ)
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
m : ℕ
hm : 1 ≤ m
⊢ smoothingFun μ (x ^ m) = smoothingFun μ x ^ m
have hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
Tactic: have hlim : Tendsto (fun n => smoothingSeminormSeq μ x (m * n)) atTop
      (𝓝 (smoothingFun μ x)) :=
    Tendsto.comp (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x) (tendsto_atTop_atTop_of_monotone
      (fun n k hnk ↦ mul_le_mul_right hnk m) (fun n ↦ ⟨n, le_mul_of_one_le_left' hm⟩))
-- 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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
⊢ smoothingFun μ (x ^ m) = smoothingFun μ x ^ m
have apply : Tendsto (fun (x_1 : ℕ) ↦ smoothingSeminormSeq μ x (m * x_1) ^ m) atTop (𝓝 (smoothingFun μ (x ^ m)))
Tactic: apply tendsto_nhds_unique _ (Tendsto.pow hlim m)
-- 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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
⊢ smoothingSeminormSeq μ x (m * n) ^ m = smoothingSeminormSeq μ (x ^ m) n
have hm' : Ne (α := ℝ) (↑m : ℝ) 0
Tactic: have hm' : (m : ℝ) ≠ 0 := cast_ne_zero.mpr (_root_.ne_of_gt (lt_of_lt_of_le zero_lt_one hm))
-- 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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : Ne (α := ℝ) (↑m : ℝ) 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (m * n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div,
      mul_comm (1 / (m : ℝ)), mul_assoc, one_div_mul_cancel hm', mul_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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (m * n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw₁ : HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)))
    (↑m : ℝ) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div,
      mul_comm (1 / (m : ℝ)), mul_assoc, one_div_mul_cancel hm', mul_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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₁ :
  HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)))
      (↑m : ℝ) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (m * n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw₂ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ) * (↑m : ℝ)) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div,
      mul_comm (1 / (m : ℝ)), mul_assoc, one_div_mul_cancel hm', mul_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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₁ :
  HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)))
      (↑m : ℝ) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₂ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (m * n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw₃ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (1 / HMul.hMul (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑m : ℝ)) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div,
      mul_comm (1 / (m : ℝ)), mul_assoc, one_div_mul_cancel hm', mul_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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₁ :
  HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)))
      (↑m : ℝ) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₂ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₃ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (1 / HMul.hMul (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (m * n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw₄ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
    (HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (↑m : ℝ)) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div,
      mul_comm (1 / (m : ℝ)), mul_assoc, one_div_mul_cancel hm', mul_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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₁ :
  HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)))
      (↑m : ℝ) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₂ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₃ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (1 / HMul.hMul (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₄ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (m * n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw₅ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * (↑m : ℝ)) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div,
      mul_comm (1 / (m : ℝ)), mul_assoc, one_div_mul_cancel hm', mul_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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₁ :
  HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)))
      (↑m : ℝ) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₂ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₃ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (1 / HMul.hMul (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₄ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₅ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (m * n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw₆ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * (↑m : ℝ))) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div,
      mul_comm (1 / (m : ℝ)), mul_assoc, one_div_mul_cancel hm', mul_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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₁ :
  HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)))
      (↑m : ℝ) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₂ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₃ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (1 / HMul.hMul (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₄ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₅ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₆ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * (↑m : ℝ))) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (m * n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw₇ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * 1) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div,
      mul_comm (1 / (m : ℝ)), mul_assoc, one_div_mul_cancel hm', mul_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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₁ :
  HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)))
      (↑m : ℝ) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₂ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₃ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (1 / HMul.hMul (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₄ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₅ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * (↑m : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₆ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * (↑m : ℝ))) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₇ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * 1) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (m * n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(m * n) : ℝ)) ^ m =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw₈ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div,
      mul_comm (1 / (m : ℝ)), mul_assoc, one_div_mul_cancel hm', mul_one]
-- 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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
⊢ Tendsto (fun (x_1 : ℕ) ↦ smoothingSeminormSeq μ x (m * x_1) ^ m) atTop (𝓝 (smoothingFun μ (x ^ m)))
have h_eq : ∀ (n : ℕ), smoothingSeminormSeq μ x (m * n) ^ m = smoothingSeminormSeq μ (x ^ m) n
Tactic: have h_eq (n : ℕ) : smoothingSeminormSeq μ x (m * n) ^ m = smoothingSeminormSeq μ (x ^ m) n := by
    have hm' : (m : ℝ) ≠ 0 := cast_ne_zero.mpr (_root_.ne_of_gt (lt_of_lt_of_le zero_lt_one hm))
    simp only [smoothingSeminormSeq]
    rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div,
      mul_comm (1 / (m : ℝ)), mul_assoc, one_div_mul_cancel hm', mul_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 : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
⊢ smoothingFun μ x = (μ : (a : R) → ℝ) x
have apply : smoothingSeminormSeq μ x =ᶠ[atTop] fun (x_1 : ℕ) ↦ (μ : (a : R) → ℝ) x
Tactic: apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)
    tendsto_const_nhds
-- 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 : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
⊢ smoothingSeminormSeq μ x =ᶠ[atTop] fun (x_1 : ℕ) ↦ (μ : (a : R) → ℝ) x
have simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x
Tactic: simp only [EventuallyEq, eventually_atTop, ge_iff_le]