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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
h : ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ 0 b = 0
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ 0 b = 0

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

Tactic:
rw [zero_pow (pos_iff_ne_zero.mp hn), map_zero, zero_rpow]

Premises used: map_zero, Real.zero_rpow, Iff.mp, pos_iff_ne_zero, zero_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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n : ℕ
hn : 1 ≤ n
⊢ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≠ 0

Tactic:
one_div_ne_zero (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn))

Premises used: Iff.mpr, Iff.mp, Nat.one_le_iff_ne_zero, one_div_ne_zero, Nat.cast_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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n : ℕ
hn : 1 ≤ n
⊢ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≠ 0

Tactic:
exact one_div_ne_zero (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn))

Premises used: one_div_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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n : R
e_s :
  Eq (α := ℕ+ → ℝ)
    (fun (n_1 : ℕ+) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((-n) ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ)))
    fun (n_1 : ℕ+) ↦
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ))
⊢ Eq (α := ℝ)
    (⨅ (n_1 : ℕ+),
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((-n) ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ)))
    (⨅ (n_1 : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ)))

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : R
e_s :
  ∀ (n_1 : ℕ+),
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((-n) ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ)) =
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ))
⊢ Eq (α := ℕ+ → ℝ)
    (fun (n_1 : ℕ+) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((-n) ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ)))
    fun (n_1 : ℕ+) ↦
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ))

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ℕ+
e_s :
  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 : ℕ) : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((-n_1) ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))

Tactic:
rw [neg_pow]

Premises used: neg_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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n_1 : R
n : ℕ+
e_s :
  ∀ (hpos : HPow.hPow (α := R) (-1) (↑n : ℕ) = 1),
    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 : ℕ) : ℝ))
e_s₁ :
  ∀ (hneg : HPow.hPow (α := R) (-1) (↑n : ℕ) = -1),
    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 : ℕ) : ℝ))
⊢ 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 : ℕ) : ℝ))

Tactic:
rcases neg_one_pow_eq_or R n with hpos | hneg

Premises used: PNat.val, neg_one_pow_eq_or
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ℕ+
hpos : 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₁ 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 : ℕ) : ℝ))

Tactic:
rw [hpos, one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ℕ) : ℝ))
e_s₂ 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 : ℕ) : ℝ))

Tactic:
rw [hneg, neg_one_mul, map_neg_eq_map μ]

Premises used: neg_one_mul, AddGroupSeminormClass.map_neg_eq_map
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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
apply : ∀ (x_1 : ℕ), smoothingSeminormSeq μ (x * y) x_1 ≤ smoothingSeminormSeq μ x x_1 * smoothingSeminormSeq μ y x_1
⊢ smoothingFun μ (x * y) ≤ smoothingFun μ x * smoothingFun μ y

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))

Premises used: HMul.hMul, tendsto_smoothingFun_of_map_one_le_one, Filter.Tendsto.mul, le_of_tendsto_of_tendsto'
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ℕ
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
simp only [one_div, inv_nonneg, cast_nonneg]

Premises used: Nat.cast_nonneg, inv_nonneg, one_div
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ℕ
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
have hn : 0 ≤ 1 / (n : ℝ) := by simp only [one_div, inv_nonneg, cast_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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
n : ℕ
hn : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
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 : ℝ)
⊢ 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 : ℝ))

Tactic:
rw [← mul_rpow (apply_nonneg μ _) (apply_nonneg μ _), mul_pow]

Premises used: Real.mul_rpow, NonnegHomClass.apply_nonneg, mul_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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
n : ℕ
hn : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₁ :
  (μ : (a : R) → ℝ) (x ^ n * y ^ n) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) ((μ : (a : R) → ℝ) (y ^ 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 : ℝ)

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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
n : ℕ
hn : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ (μ : (a : R) → ℝ) (x ^ n * y ^ n) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ)

Tactic:
map_mul_le_mul μ _ _

Premises used: SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ℝ)
⊢ (μ : (a : R) → ℝ) (x ^ n * y ^ n) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ)

Tactic:
exact map_mul_le_mul μ _ _

Premises used: SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
⊢ LE.le (α := ℝ) ((smoothingSeminorm μ hμ1 hna : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
smoothingFun_one_le μ hμ1

Premises used: iInf, smoothingFun_one_le
-- 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
m : ℕ
hm : 1 ≤ m
⊢ 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⟩))
-- 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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
apply : Tendsto (fun (x_1 : ℕ) ↦ smoothingSeminormSeq μ x (m * x_1) ^ m) atTop (𝓝 (smoothingFun μ (x ^ m)))
⊢ smoothingFun μ (x ^ m) = smoothingFun μ x ^ m

Tactic:
apply tendsto_nhds_unique _ (Tendsto.pow hlim m)

Premises used: Filter.Tendsto.pow, tendsto_nhds_unique
-- 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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
⊢ 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))
-- 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
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 : ℝ))
rw₈ rw₉ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x ^ m) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    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 : ℝ))

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]

Premises used: mul_assoc, HDiv.hDiv, Nat.cast, pow_mul, Nat.cast_mul, mul_comm, one_div_mul_cancel, mul_one, NonnegHomClass.apply_nonneg, Real.rpow_mul, OfNat.ofNat, one_div_mul_one_div, Real.rpow_natCast
-- 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
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

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]
-- 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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
h_eq : ∀ (n : ℕ), smoothingSeminormSeq μ x (m * n) ^ m = smoothingSeminormSeq μ (x ^ m) n
⊢ Tendsto (fun (x_1 : ℕ) ↦ smoothingSeminormSeq μ x (m * x_1) ^ m) atTop (𝓝 (smoothingFun μ (x ^ m)))

Tactic:
simpa [h_eq] using tendsto_smoothingFun_of_map_one_le_one μ hμ1 _

Premises used: 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
hx : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
apply : smoothingSeminormSeq μ x =ᶠ[atTop] fun (x_1 : ℕ) ↦ (μ : (a : R) → ℝ) x
⊢ smoothingFun μ x = (μ : (a : R) → ℝ) x

Tactic:
apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)
    tendsto_const_nhds

Premises used: tendsto_const_nhds, tendsto_nhds_unique_of_eventuallyEq, 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
hx : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x
⊢ smoothingSeminormSeq μ x =ᶠ[atTop] fun (x_1 : ℕ) ↦ (μ : (a : R) → ℝ) x

Tactic:
simp only [EventuallyEq, eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.EventuallyEq, 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 : ℝ)
x : R
hx : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
h : ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x

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 : ℝ)
x : R
hx : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
n : ℕ
hn : 1 ≤ n
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
have hn0 : (n : ℝ) ≠ 0 := cast_ne_zero.mpr (one_le_iff_ne_zero.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 : ℝ)
x : R
hx : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
n : ℕ
hn : 1 ≤ n
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
h₁ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
h₂ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
h₃ : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1 = (μ : (a : R) → ℝ) x
h₄ h₅ : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x

Tactic:
rw [hx n hn, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]

Premises used: Real.rpow_one, mul_one_div_cancel, NonnegHomClass.apply_nonneg, Real.rpow_mul, Real.rpow_natCast
-- 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 : ℝ)
apply : smoothingSeminormSeq μ x =ᶠ[atTop] fun (x_1 : ℕ) ↦ (μ : (a : R) → ℝ) x
⊢ smoothingFun μ x = (μ : (a : R) → ℝ) x

Tactic:
apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)
    tendsto_const_nhds

Premises used: tendsto_const_nhds, tendsto_nhds_unique_of_eventuallyEq, 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
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x
⊢ smoothingSeminormSeq μ x =ᶠ[atTop] fun (x_1 : ℕ) ↦ (μ : (a : R) → ℝ) x

Tactic:
simp only [EventuallyEq, eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.EventuallyEq, 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 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
h : ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x

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 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
pos :
  ∀ (hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)),
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
neg :
  ∀ (hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)),
    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

Tactic:
by_cases hx0 : μ 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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
apply : LE.le (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)

Tactic:
apply le_antisymm _ (apply_nonneg μ _)

Premises used: le_antisymm, NonnegHomClass.apply_nonneg