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

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 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 _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
⊢ smoothingFun μ (x ^ m) = smoothingFun μ x ^ m

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_left' hnk m) (fun n ↦ ⟨n, le_mul_of_one_le_left' hm⟩))

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n => smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
⊢ smoothingFun μ (x ^ m) = smoothingFun μ x ^ m

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n => smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
⊢ Tendsto (fun x_1 => smoothingSeminormSeq μ x (m * x_1) ^ m) atTop (𝓝 (smoothingFun μ (x ^ m)))

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]

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 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)))

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

Tactic:
intro x m hm

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
⊢ smoothingFun μ (x ^ m) = smoothingFun μ x ^ m

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 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 hm' : (m : ℝ) ≠ 0 := cast_ne_zero.mpr (_root_.ne_of_gt (lt_of_lt_of_le zero_lt_one hm))

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n => smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : ↑m ≠ 0
⊢ smoothingSeminormSeq μ x (m * n) ^ m = smoothingSeminormSeq μ (x ^ m) n

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n => smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
⊢ smoothingFun μ (x ^ m) = smoothingFun μ x ^ m

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

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n => smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
⊢ Tendsto (fun x_1 => smoothingSeminormSeq μ x (m * x_1) ^ m) atTop (𝓝 (smoothingFun μ (x ^ m)))

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n => smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : ↑m ≠ 0
⊢ (μ (x ^ (m * n)) ^ (1 / ↑(m * n))) ^ m = μ ((x ^ m) ^ n) ^ (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]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n => smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : ↑m ≠ 0
⊢ smoothingSeminormSeq μ x (m * n) ^ m = smoothingSeminormSeq μ (x ^ m) n

Tactic:
simp only [smoothingSeminormSeq]

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n => smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : ↑m ≠ 0
⊢ (μ (x ^ (m * n)) ^ (1 / ↑(m * n))) ^ m = μ ((x ^ m) ^ n) ^ (1 / ↑n)