-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem smoothingFun_one_le (hμ1 : μ 1 ≤ 1) : smoothingFun μ 1 ≤ 1

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ smoothingSeminormSeq μ 1 n ≤ 1

Tactic:
simp only [smoothingSeminormSeq]

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

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
⊢ ∀ᶠ (c : ℕ) in atTop, smoothingSeminormSeq μ 1 c ≤ 1

Tactic:
simp only [eventually_atTop, ge_iff_le]

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ 1 b ≤ 1

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ 0 < ↑n

Tactic:
rw [← cast_zero, cast_lt]

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ 0 < n

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

Tactic:
conv_rhs => rw [← one_rpow (1 / n : ℝ)]

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

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ 1 b ≤ 1

Tactic:
use 1

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
⊢ ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ 1 b ≤ 1

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ 0 < n

Tactic:
exact succ_le_iff.mp hn

Result:
no goals

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

Tactic:
have hn1 : 0 < (1 / n : ℝ) := by
  apply _root_.div_pos zero_lt_one
  rw [← cast_zero, cast_lt]
  exact succ_le_iff.mp hn

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
hn1 : 0 < 1 / ↑n
⊢ μ 1 ^ (1 / ↑n) ≤ 1 ^ (1 / ↑n)

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
⊢ smoothingFun μ 1 ≤ 1

Tactic:
apply le_of_tendsto (tendsto_smoothingFun_of_map_one_le_one μ hμ1 (1 : R))

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
⊢ ∀ᶠ (c : ℕ) in atTop, smoothingSeminormSeq μ 1 c ≤ 1

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ 0 < 1 / ↑n

Tactic:
apply _root_.div_pos zero_lt_one

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ 0 < ↑n

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

Tactic:
rw [one_pow]

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

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
⊢ ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ 1 b ≤ 1

Tactic:
rintro n hn

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ smoothingSeminormSeq μ 1 n ≤ 1

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

Tactic:
exact (rpow_le_rpow_iff (apply_nonneg μ _) zero_le_one hn1).mpr hμ1

Result:
no goals