-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem smoothingSeminormSeq_tendsto_aux {L : ℝ} (hL : 0 ≤ L) {ε : ℝ} (hε : 0 < ε)
    {m1 : ℕ} (hm1 : 0 < m1) {x : R} (hx : μ x ≠ 0) :
    Tendsto
      (fun n : ℕ => (L + ε) ^ (-(((n % m1 : ℕ) : ℝ) / (n : ℝ))) * (μ x ^ (n % m1)) ^ (1 / (n : ℝ)))
      atTop (𝓝 1)

Proof state:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
h0 : Tendsto (fun t => -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ Tendsto (fun x => (L + ε) ^ (-(↑(x % m1) / ↑x))) atTop (𝓝 ((L + ε) ^ 0))

Tactic:
apply Tendsto.rpow tendsto_const_nhds h0

Result:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
h0 : Tendsto (fun t => -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ L + ε ≠ 0 ∨ 0 < 0

Proof state:
case hg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun x_1 => (μ x ^ (x_1 % m1)) ^ (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)]

Result:
case hg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun x_1 => μ x ^ (↑(x_1 % m1) / ↑x_1)) atTop (𝓝 (μ x ^ 0))

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun n => (L + ε) ^ (-(↑(n % m1) / ↑n)) * (μ x ^ (n % m1)) ^ (1 * 1 / ↑n)) atTop (𝓝 (1 * 1))

Tactic:
apply Tendsto.mul

Result:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun x => (L + ε) ^ (-(↑(x % m1) / ↑x))) atTop (𝓝 1)

case hg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun x_1 => (μ x ^ (x_1 % m1)) ^ (1 * 1 / ↑x_1)) atTop (𝓝 1)

Proof state:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
h0 : Tendsto (fun t => -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ ¬(L = 0 ∧ ε = 0) ∨ 0 < 0

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

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun t => -(↑(t % m1) / ↑t)) atTop (𝓝 0)

Tactic:
rw [← neg_zero]

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun t => -(↑(t % m1) / ↑t)) atTop (𝓝 (-0))

Proof state:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
h0 : Tendsto (fun t => -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ L + ε ≠ 0 ∨ 0 < 0

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

Result:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
h0 : Tendsto (fun t => -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ ¬(L = 0 ∧ ε = 0) ∨ 0 < 0

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun t => -(↑(t % m1) / ↑t)) atTop (𝓝 (-0))

Tactic:
exact Tendsto.neg h_exp

Result:
no goals

Proof state:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
h0 : Tendsto (fun t => -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ Tendsto (fun x => (L + ε) ^ (-(↑(x % m1) / ↑x))) atTop (𝓝 1)

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

Result:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
h0 : Tendsto (fun t => -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ Tendsto (fun x => (L + ε) ^ (-(↑(x % m1) / ↑x))) atTop (𝓝 ((L + ε) ^ 0))

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
⊢ Tendsto (fun n => (L + ε) ^ (-(↑(n % m1) / ↑n)) * (μ x ^ (n % m1)) ^ (1 / ↑n)) atTop (𝓝 1)

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

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
⊢ Tendsto (fun n => (L + ε) ^ (-(↑(n % m1) / ↑n)) * (μ x ^ (n % m1)) ^ (1 * 1 / ↑n)) atTop (𝓝 (1 * 1))

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
⊢ Tendsto (fun n => (L + ε) ^ (-(↑(n % m1) / ↑n)) * (μ x ^ (n % m1)) ^ (1 * 1 / ↑n)) atTop (𝓝 (1 * 1))

Tactic:
have h_exp : Tendsto (fun n : ℕ => ((n % m1 : ℕ) : ℝ) / (n : ℝ)) atTop (𝓝 0) :=
  tendsto_mod_div_atTop_nhds_zero_nat hm1

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun n => (L + ε) ^ (-(↑(n % m1) / ↑n)) * (μ x ^ (n % m1)) ^ (1 * 1 / ↑n)) atTop (𝓝 (1 * 1))

Proof state:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun x => (L + ε) ^ (-(↑(x % m1) / ↑x))) atTop (𝓝 1)

Tactic:
have h0 : Tendsto (fun t : ℕ => -(((t % m1 : ℕ) : ℝ) / (t : ℝ))) atTop (𝓝 0) := by
  rw [← neg_zero]
  exact Tendsto.neg h_exp

Result:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
h0 : Tendsto (fun t => -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ Tendsto (fun x => (L + ε) ^ (-(↑(x % m1) / ↑x))) atTop (𝓝 1)

Proof state:
case hg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n => ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun x_1 => μ x ^ (↑(x_1 % m1) / ↑x_1)) atTop (𝓝 (μ x ^ 0))

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

Result:
no goals