awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
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))
⊢ 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)))
have 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)))
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
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 : ℕ
⊢ 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)))
have 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
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
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 : ℕ
⊢ 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
have 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
Tactic: rw [mul_assoc _ (f c), mul_inv_cancel₀ hc, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
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
⊢ 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
have 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
Tactic: rw [mul_assoc _ (f c), mul_inv_cancel₀ hc, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
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
⊢ 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
have 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)
Tactic: rw [mul_assoc _ (f c), mul_inv_cancel₀ hc, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (hypothesis)
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))
⊢ Tendsto (seminormFromConst_seq c f (c * x)) atTop
    (𝓝 (HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (seminormFromConst' c f x)))
have hterm : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
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) → ℝ)
⊢ Ne (α := ℝ) ((seminormFromConst hg1 hg_k hg_pm : (a : K) → ℝ) k : ℝ) (0 : ℝ)
have rwa : seminormFromConst' k g k ≠ 0
Tactic: rwa [seminormFromConst_def hg1 hg_k, seminormFromConst_apply_c hg1 hg_k hg_pm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 : ℕ) ↦
      (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % m1) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
    atTop (𝓝 1)
have 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))
Tactic: rw [← mul_one (1 : ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
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 : ℕ) ↦
      (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % m1) ^ (HMul.hMul (α := ℝ) 1 1 / (↑n : ℝ)))
    atTop (𝓝 (HMul.hMul (α := ℝ) 1 1))
have h_exp : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 (n : ℕ) ↦
      (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(n % m1) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % m1) ^ (HMul.hMul (α := ℝ) 1 1 / (↑n : ℝ)))
    atTop (𝓝 (HMul.hMul (α := ℝ) 1 1))
have hf : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(x % m1) : ℝ) (↑x : ℝ))) atTop (𝓝 1)
Tactic: apply Tendsto.mul
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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)
⊢ 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))
have hg : Tendsto (β := ℝ)
  (fun (x_1 : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (x_1 % m1) ^ (HMul.hMul (α := ℝ) 1 1 / (↑x_1 : ℝ)))
  atTop (𝓝 1)
Tactic: apply Tendsto.mul
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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)
have rw : Tendsto (β := ℝ) (fun (t : ℕ) ↦ -HDiv.hDiv (α := ℝ) (↑(t % m1) : ℝ) (↑t : ℝ)) atTop (𝓝 (-0))
Tactic: rw [← neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
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 : ℕ) ↦ (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(x % m1) : ℝ) (↑x : ℝ))) atTop (𝓝 1)
have h0 : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(x % m1) : ℝ) (↑x : ℝ))) atTop (𝓝 1)
have hf : Tendsto (fun (x : ℕ) ↦ (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(x % m1) : ℝ) (↑x : ℝ))) atTop
  (𝓝 (HPow.hPow (β := ℝ) (L + ε) 0))
Tactic: rw [← rpow_zero (L + ε)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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)
⊢ Tendsto (fun (x : ℕ) ↦ (L + ε) ^ (-HDiv.hDiv (α := ℝ) (↑(x % m1) : ℝ) (↑x : ℝ))) atTop
    (𝓝 (HPow.hPow (β := ℝ) (L + ε) 0))
have hf : L + ε ≠ 0 ∨ LT.lt (α := ℝ) 0 0
Tactic: apply Tendsto.rpow tendsto_const_nhds h0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 ∨ LT.lt (α := ℝ) 0 0
have hf : ¬(L = 0 ∧ ε = 0) ∨ LT.lt (α := ℝ) 0 0
Tactic: rw [ne_eq, add_eq_zero_iff_of_nonneg hL (le_of_lt hε)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 : ℝ) (x_1 % m1) ^ (HMul.hMul (α := ℝ) 1 1 / (↑x_1 : ℝ)))
    atTop (𝓝 1)
have hg : Tendsto (fun (x_1 : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (HDiv.hDiv (α := ℝ) (↑(x_1 % m1) : ℝ) (↑x_1 : ℝ)))
  atTop (𝓝 (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 0))
Tactic: simp_rw [mul_one, ← rpow_natCast, ← rpow_mul (apply_nonneg μ x), ← mul_div_assoc, mul_one,
      ← rpow_zero (μ x)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 : ℝ)
have apply : LE.le (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)
Tactic: apply le_antisymm _ (apply_nonneg μ _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ LE.le (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)
have rw : (μ : (a : R) → ℝ) (x ^ n) ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
Tactic: rw [← zero_pow (pos_iff_ne_zero.mp hn), ← hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
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
have hμ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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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 : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0
have rw : HPow.hPow (α := ℝ) 0 (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0
Tactic: rw [hμn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [hμn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))
have h0 : ∀ (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))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
x : R
hx : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h0 : ∀ (n : ℕ) (hn : 1 ≤ n), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))
have hL0 : Eq (α := ℝ)
  (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) 0
Tactic: have hL0 : (iInf fun n : PNat => μ (x ^ (n : ℕ)) ^ (1 / (n : ℝ))) = 0 :=
    le_antisymm
      (ciInf_le_of_le (smoothingSeminormSeq_bddBelow μ x) (1 : PNat) (le_of_eq (h0 1 (le_refl _))))
      (le_ciInf fun n ↦ by positivity)
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))
have hL0 : 0 ≤ L
Tactic: have hL0 : 0 ≤ L := le_ciInf fun x ↦ by positivity
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))
have rw : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε
Tactic: rw [Metric.tendsto_atTop]
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
⊢ ∃ (N : ℕ), ∀ n ≥ N, dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε
have obtain : ∀ (m1 : ℕ+)
  (hm1 :
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
      (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
        ε / 2),
  ∃ (N : ℕ), ∀ n ≥ N, dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε
Tactic: obtain ⟨m1, hm1⟩ := smoothingSeminormSeq_exists_pnat μ x hε
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
⊢ ∃ (m : ℕ),
    ∀ n ≥ m,
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
          1 ≤
        ε / (2 * (L + ε / 2))
have hε2 : 0 < ε / 2
Tactic: have hε2 : 0 < ε / 2 := half_pos hε
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
hε2 : 0 < ε / 2
⊢ ∃ (m : ℕ),
    ∀ n ≥ m,
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
          1 ≤
        ε / (2 * (L + ε / 2))
have hL2 : Tendsto (β := ℝ)
  (fun (n : ℕ) ↦
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
  atTop (𝓝 1)
Tactic: have hL2 := smoothingSeminormSeq_tendsto_aux μ hL0 hε2 (PNat.pos m1) 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
hε2 : 0 < ε / 2
hL2 :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
    atTop (𝓝 1)
⊢ ∃ (m : ℕ),
    ∀ n ≥ m,
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
          1 ≤
        ε / (2 * (L + ε / 2))
have hL2₁ : ∀ ε_1 > 0,
  ∃ (N : ℕ),
    ∀ n ≥ N,
      dist
          ((L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
            HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
          1 <
        ε_1
Tactic: rw [Metric.tendsto_atTop] at hL2
Cleared hypotheses: hL2