awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
apply : ∀ (b : ℕ), ∃ (a : ℕ), b ≤ a + 1
⊢ Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))

Tactic:
apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).comp
      (tendsto_atTop_atTop_of_monotone add_left_mono _)

Premises used: Filter.tendsto_atTop_atTop_of_monotone, add_left_mono, Filter.Tendsto.comp, tendsto_seminormFromConst_seq_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
n : ℕ
h : n ≤ n + 1
⊢ ∃ (a : ℕ), n ≤ a + 1

Tactic:
use n
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
n : ℕ
⊢ n ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
⊢ Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))

Tactic:
have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f x (n + 1)) atTop
      (𝓝 (seminormFromConst' c f x)) := by
    apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).comp
      (tendsto_atTop_atTop_of_monotone add_left_mono _)
    rintro n; use n; lia
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
rw : seminormFromConst' c f (c * x) = HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (seminormFromConst' c f x)
⊢ seminormFromConst' c f (c * x) = seminormFromConst' c f c * seminormFromConst' c f x

Tactic:
rw [seminormFromConst_apply_c hf1 hc hpm]

Premises used: seminormFromConst_apply_c
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
apply :
  Tendsto (seminormFromConst_seq c f (c * x)) atTop
    (𝓝 (HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (seminormFromConst' c f x)))
⊢ seminormFromConst' c f (c * x) = HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (seminormFromConst' c f x)

Tactic:
apply tendsto_nhds_unique (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (c * x))

Premises used: HMul.hMul, tendsto_seminormFromConst_seq_atTop, tendsto_nhds_unique
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
h :
  ∀ (n : ℕ),
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
      HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ)
        (HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ (n + 1)) : ℝ)
          (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n + 1)))
⊢ Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n))
    fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ)
      (HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ (n + 1)) : ℝ)
        (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n + 1)))

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
n : ℕ
h :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n * x) : ℝ) (HPow.hPow (α := ℝ) (((f : (a : R) → ℝ) c)⁻¹ : ℝ) n) =
    HMul.hMul (β := ℝ) (HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (c * c ^ n * x) : ℝ) ((f : (a : R) → ℝ) c : ℝ))
        (((f : (a : R) → ℝ) c)⁻¹ : ℝ) *
      HPow.hPow (α := ℝ) (((f : (a : R) → ℝ) c)⁻¹ : ℝ) n
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ)
      (HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ (n + 1)) : ℝ)
        (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n + 1)))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
n : ℕ
h :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n * x) : ℝ) (HPow.hPow (α := ℝ) (((f : (a : R) → ℝ) c)⁻¹ : ℝ) n) =
    HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n * x) : ℝ)
        (HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) c : ℝ) (((f : (a : R) → ℝ) c)⁻¹ : ℝ)) *
      HPow.hPow (α := ℝ) (((f : (a : R) → ℝ) c)⁻¹ : ℝ) n
h₁ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n * x) : ℝ) (HPow.hPow (α := ℝ) (((f : (a : R) → ℝ) c)⁻¹ : ℝ) n) =
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (c * c ^ n * x) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) (((f : (a : R) → ℝ) c)⁻¹ : ℝ) n
h₂ h₃ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n * x) : ℝ) (HPow.hPow (α := ℝ) (((f : (a : R) → ℝ) c)⁻¹ : ℝ) n) =
    HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n * x) : ℝ) (HPow.hPow (α := ℝ) (((f : (a : R) → ℝ) c)⁻¹ : ℝ) n)
⊢ HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n * x) : ℝ) (HPow.hPow (α := ℝ) (((f : (a : R) → ℝ) c)⁻¹ : ℝ) n) =
    HMul.hMul (β := ℝ) (HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (c * c ^ n * x) : ℝ) ((f : (a : R) → ℝ) c : ℝ))
        (((f : (a : R) → ℝ) c)⁻¹ : ℝ) *
      HPow.hPow (α := ℝ) (((f : (a : R) → ℝ) c)⁻¹ : ℝ) n

Tactic:
rw [mul_assoc _ (f c), mul_inv_cancel₀ hc, mul_one]

Premises used: mul_inv_cancel₀, mul_assoc, mul_one, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
⊢ seminormFromConst_seq c f (c * x) = fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (seminormFromConst_seq c f x (n + 1))

Tactic:
have hterm : seminormFromConst_seq c f (c * x) =
      fun n ↦ f c * seminormFromConst_seq c f x (n + 1) := by
    simp only [seminormFromConst_seq_def]
    ext n
    ring_nf
    rw [mul_assoc _ (f c), mul_inv_cancel₀ hc, mul_one]
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
hterm :
  seminormFromConst_seq c f (c * x) = fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (seminormFromConst_seq c f x (n + 1))
⊢ Tendsto (seminormFromConst_seq c f (c * x)) atTop
    (𝓝 (HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (seminormFromConst' c f x)))

Tactic:
simpa [hterm] using tendsto_const_nhds.mul hlim

Premises used: tendsto_const_nhds, Filter.Tendsto.mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
K : Type u_1
inst : Field K
k : K
g : RingSeminorm K
hg1 : LE.le (α := ℝ) ((g : (a : K) → ℝ) 1 : ℝ) (1 : ℝ)
hg_k : Ne (α := ℝ) ((g : (a : K) → ℝ) k : ℝ) (0 : ℝ)
hg_pm : IsPowMul (R := K) (⇑g : (a : K) → ℝ)
rwa : seminormFromConst' k g k ≠ 0
rwa₁ rwa₂ rwa₃ rwa₄ : Ne (α := ℝ) ((g : (a : K) → ℝ) k : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ) ((seminormFromConst hg1 hg_k hg_pm : (a : K) → ℝ) k : ℝ) (0 : ℝ)

Tactic:
rwa [seminormFromConst_def hg1 hg_k, seminormFromConst_apply_c hg1 hg_k hg_pm]

Premises used: seminormFromConst_apply_c, seminormFromConst_def
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
Goal:
K : Type u_1
inst : Field K
k : K
g : RingSeminorm K
hg1 : LE.le (α := ℝ) ((g : (a : K) → ℝ) 1 : ℝ) (1 : ℝ)
hg_k : Ne (α := ℝ) ((g : (a : K) → ℝ) k : ℝ) (0 : ℝ)
hg_pm : IsPowMul (R := K) (⇑g : (a : K) → ℝ)
x : K
⊢ (normFromConst hg1 hg_k hg_pm : (a : K) → ℝ) x = seminormFromConst' k g x

Tactic:
rfl

Premises used: iInf, seminormFromConst', rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
ε : ℝ
hε : 0 < ε
⊢ ∃ (m : ℕ+),
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m : ℕ) : ℝ)) <
      (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
        ε / 2

Tactic:
exists_lt_of_ciInf_lt (lt_add_of_le_of_pos (le_refl _) (half_pos hε))

Premises used: le_refl, exists_lt_of_ciInf_lt, half_pos, lt_add_of_le_of_pos
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
rw :
  Tendsto
    (fun (n : ℕ) ↦
      (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % m1) ^ (HMul.hMul (α := ℝ) 1 1 / (↑n : ℝ)))
    atTop (𝓝 (HMul.hMul (α := ℝ) 1 1))
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % m1) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
    atTop (𝓝 1)

Tactic:
rw [← mul_one (1 : ℝ)]

Premises used: mul_one, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)

Tactic:
have h_exp : Tendsto (fun n : ℕ => ((n % m1 : ℕ) : ℝ) / (n : ℝ)) atTop (𝓝 0) :=
    tendsto_mod_div_atTop_nhds_zero_nat hm1
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
hf : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(x % m1) : ℝ) (↑x : ℝ))) atTop (𝓝 1)
hg :
  Tendsto (β := ℝ)
    (fun (x_1 : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (x_1 % m1) ^ (HMul.hMul (α := ℝ) 1 1 / (↑x_1 : ℝ)))
    atTop (𝓝 1)
⊢ Tendsto
    (fun (n : ℕ) ↦
      (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % m1) ^ (HMul.hMul (α := ℝ) 1 1 / (↑n : ℝ)))
    atTop (𝓝 (HMul.hMul (α := ℝ) 1 1))

Tactic:
apply Tendsto.mul

Premises used: Filter.Tendsto.mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
rw : Tendsto (β := ℝ) (fun (t : ℕ) ↦ -HDiv.hDiv (α := ℝ) (↑(t % m1) : ℝ) (↑t : ℝ)) atTop (𝓝 (-0))
⊢ Tendsto (β := ℝ) (fun (t : ℕ) ↦ -HDiv.hDiv (α := ℝ) (↑(t % m1) : ℝ) (↑t : ℝ)) atTop (𝓝 0)

Tactic:
rw [← neg_zero]

Premises used: neg_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (t : ℕ) ↦ -HDiv.hDiv (α := ℝ) (↑(t % m1) : ℝ) (↑t : ℝ)) atTop (𝓝 (-0))

Tactic:
Tendsto.neg h_exp

Premises used: Filter.Tendsto.neg
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (t : ℕ) ↦ -HDiv.hDiv (α := ℝ) (↑(t % m1) : ℝ) (↑t : ℝ)) atTop (𝓝 (-0))

Tactic:
exact Tendsto.neg h_exp

Premises used: Filter.Tendsto.neg
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (t : ℕ) ↦ -HDiv.hDiv (α := ℝ) (↑(t % m1) : ℝ) (↑t : ℝ)) atTop (𝓝 0)

Tactic:
have h0 : Tendsto (fun t : ℕ => -(((t % m1 : ℕ) : ℝ) / (t : ℝ))) atTop (𝓝 0) := by
      rw [← neg_zero]
      exact Tendsto.neg h_exp
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
h0 : Tendsto (β := ℝ) (fun (t : ℕ) ↦ -HDiv.hDiv (α := ℝ) (↑(t % m1) : ℝ) (↑t : ℝ)) atTop (𝓝 0)
hf :
  Tendsto (fun (x : ℕ) ↦ (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(x % m1) : ℝ) (↑x : ℝ))) atTop
    (𝓝 (HPow.hPow (β := ℝ) (L + ε) 0))
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(x % m1) : ℝ) (↑x : ℝ))) atTop (𝓝 1)

Tactic:
rw [← rpow_zero (L + ε)]

Premises used: Real.rpow_zero, HAdd.hAdd
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
h0 : Tendsto (β := ℝ) (fun (t : ℕ) ↦ -HDiv.hDiv (α := ℝ) (↑(t % m1) : ℝ) (↑t : ℝ)) atTop (𝓝 0)
hf : L + ε ≠ 0 ∨ LT.lt (α := ℝ) 0 0
⊢ Tendsto (fun (x : ℕ) ↦ (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(x % m1) : ℝ) (↑x : ℝ))) atTop
    (𝓝 (HPow.hPow (β := ℝ) (L + ε) 0))

Tactic:
apply Tendsto.rpow tendsto_const_nhds h0

Premises used: tendsto_const_nhds, Filter.Tendsto.rpow
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
h0 : Tendsto (β := ℝ) (fun (t : ℕ) ↦ -HDiv.hDiv (α := ℝ) (↑(t % m1) : ℝ) (↑t : ℝ)) atTop (𝓝 0)
hf : ¬(L = 0 ∧ ε = 0) ∨ LT.lt (α := ℝ) 0 0
⊢ L + ε ≠ 0 ∨ LT.lt (α := ℝ) 0 0

Tactic:
rw [ne_eq, add_eq_zero_iff_of_nonneg hL (le_of_lt hε)]

Premises used: add_eq_zero_iff_of_nonneg, le_of_lt, ne_eq
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
h0 : Tendsto (β := ℝ) (fun (t : ℕ) ↦ -HDiv.hDiv (α := ℝ) (↑(t % m1) : ℝ) (↑t : ℝ)) atTop (𝓝 0)
⊢ ¬(L = 0 ∧ ε = 0) ∨ LT.lt (α := ℝ) 0 0

Tactic:
Or.inl (not_and_of_not_right _ (ne_of_gt hε))

Premises used: ne_of_gt, not_and_of_not_right, Or.inl
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
h0 : Tendsto (β := ℝ) (fun (t : ℕ) ↦ -HDiv.hDiv (α := ℝ) (↑(t % m1) : ℝ) (↑t : ℝ)) atTop (𝓝 0)
⊢ ¬(L = 0 ∧ ε = 0) ∨ LT.lt (α := ℝ) 0 0

Tactic:
exact Or.inl (not_and_of_not_right _ (ne_of_gt hε))

Premises used: ne_of_gt, not_and_of_not_right, Or.inl
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
hg :
  Tendsto
    (fun (x_1 : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(x_1 % m1) : ℝ) (↑x_1 : ℝ)))
    atTop (𝓝 (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0))
⊢ Tendsto (β := ℝ)
    (fun (x_1 : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (x_1 % m1) ^ (HMul.hMul (α := ℝ) 1 1 / (↑x_1 : ℝ)))
    atTop (𝓝 1)

Tactic:
simp_rw [mul_one, ← rpow_natCast, ← rpow_mul (apply_nonneg μ x), ← mul_div_assoc, mul_one,
      ← rpow_zero (μ x)]

Premises used: mul_div_assoc, Real.rpow_zero, mul_one, NonnegHomClass.apply_nonneg, Real.rpow_mul, DFunLike.coe, Real.rpow_natCast
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
⊢ Tendsto
    (fun (x_1 : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(x_1 % m1) : ℝ) (↑x_1 : ℝ)))
    atTop (𝓝 (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0))

Tactic:
Tendsto.rpow tendsto_const_nhds h_exp (Or.inl hx)

Premises used: tendsto_const_nhds, Filter.Tendsto.rpow, Or.inl
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h_exp : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) atTop (𝓝 0)
⊢ Tendsto
    (fun (x_1 : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(x_1 % m1) : ℝ) (↑x_1 : ℝ)))
    atTop (𝓝 (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0))

Tactic:
exact Tendsto.rpow tendsto_const_nhds h_exp (Or.inl hx)

Premises used: tendsto_const_nhds, Filter.Tendsto.rpow, Or.inl
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
n : ℕ+
⊢ LE.le (α := ℝ) 0
    ((fun (n : ℕ+) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)))
      n)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
⊢ BddBelow (α := ℝ)
    (Set.range fun (n : ℕ+) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)))

Tactic:
⟨0, zero_mem_lowerBounds_smoothingSeminormSeq_range μ x⟩

Premises used: Set.Nonempty, zero_mem_lowerBounds_smoothingSeminormSeq_range, BddBelow, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
n : ℕ
hn : 1 ≤ n
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
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
n : ℕ
hn : 1 ≤ n
rw : (μ : (a : R) → ℝ) (x ^ n) ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
⊢ LE.le (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)

Tactic:
rw [← zero_pow (pos_iff_ne_zero.mp hn), ← hx]

Premises used: Iff.mp, pos_iff_ne_zero, zero_pow
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ (μ : (a : R) → ℝ) (x ^ n) ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n

Tactic:
map_pow_le_pow _ x (one_le_iff_ne_zero.mp hn)

Premises used: map_pow_le_pow, Iff.mp, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ (μ : (a : R) → ℝ) (x ^ n) ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n

Tactic:
exact map_pow_le_pow _ x (one_le_iff_ne_zero.mp hn)

Premises used: map_pow_le_pow, Iff.mp, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)

Tactic:
have hμn : μ (x ^ n) = 0 := by
      apply le_antisymm _ (apply_nonneg μ _)
      rw [← zero_pow (pos_iff_ne_zero.mp hn), ← hx]
      exact map_pow_le_pow _ x (one_le_iff_ne_zero.mp hn)
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
n : ℕ
hn : 1 ≤ n
hμn : Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)
rw : HPow.hPow (α := ℝ) 0 (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0

Tactic:
rw [hμn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]

Premises used: Nat.one_div_cast_ne_zero, Real.zero_rpow, Iff.mp, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∀ (n : ℕ) (hn : 1 ≤ n), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0

Tactic:
have h0 (n : ℕ) (hn : 1 ≤ n) : μ (x ^ n) ^ (1 / (n : ℝ)) = 0 := by
    have hμn : μ (x ^ n) = 0 := by
      apply le_antisymm _ (apply_nonneg μ _)
      rw [← zero_pow (pos_iff_ne_zero.mp hn), ← hx]
      exact map_pow_le_pow _ x (one_le_iff_ne_zero.mp hn)
    rw [hμn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]