-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem tendsto_smoothingFun_of_eq_zero {x : R} (hx : μ x = 0) :
    Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
n : ℕ
hn : 1 ≤ n
⊢ μ (x ^ n) ^ (1 / ↑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)

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
n : ℕ
hn : 1 ≤ n
hμn : μ (x ^ n) = 0
⊢ μ (x ^ n) ^ (1 / ↑n) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
n : ℕ
hn : 1 ≤ n
⊢ μ (x ^ n) = 0

Tactic:
apply le_antisymm _ (apply_nonneg μ _)

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
n : ℕ
hn : 1 ≤ n
⊢ μ (x ^ n) ≤ 0

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

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

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
h0 : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) ^ (1 / ↑n) = 0
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
h0 : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) ^ (1 / ↑n) = 0
hL0 : ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n) = 0
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
simpa only [hL0] using tendsto_atTop_of_eventually_const h0

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
n : ℕ
hn : 1 ≤ n
hμn : μ (x ^ n) = 0
⊢ μ (x ^ n) ^ (1 / ↑n) = 0

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

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
h0 : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) ^ (1 / ↑n) = 0
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

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 => rpow_nonneg (apply_nonneg μ _) _)

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
h0 : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) ^ (1 / ↑n) = 0
hL0 : ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n) = 0
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
n : ℕ
hn : 1 ≤ n
⊢ μ (x ^ n) ≤ 0

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

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
n : ℕ
hn : 1 ≤ n
⊢ μ (x ^ n) ≤ μ x ^ n

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
n : ℕ
hn : 1 ≤ n
⊢ μ (x ^ n) ≤ μ x ^ n

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

Result:
no goals