-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem tendsto_factorial_div_pow_self_atTop :
    Tendsto (fun n ↦ n ! / (n : ℝ) ^ n : ℕ → ℝ) atTop (𝓝 0) :=
  tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds
    (tendsto_const_div_atTop_nhds_zero_nat 1)
    (Eventually.of_forall fun n ↦
      div_nonneg (mod_cast n.factorial_pos.le)
        (pow_nonneg (mod_cast n.zero_le) _))
    (by
      refine (eventually_gt_atTop 0).mono fun n hn ↦ ?_
      rcases Nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩
      rw [← prod_range_add_one_eq_factorial, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div,
        prod_natCast, Nat.cast_succ, ← Finset.prod_inv_distrib, ← prod_mul_distrib,
        Finset.prod_range_succ']
      simp only [prod_range_succ', one_mul, Nat.cast_add, zero_add, Nat.cast_one]
      refine
            mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_) <;>
          intro x hx <;>
        rw [Finset.mem_range] at hx
      · positivity
      · refine (div_le_one <| mod_cast hn).mpr ?_
        norm_cast
        omega)

Proof state:
case intro.refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1

Tactic:
refine (div_le_one <| mod_cast hn).mpr ?_

Result:
case intro.refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ ↑x + 1 + 1 ≤ ↑k + 1

Proof state:
case intro
k : ℕ
hn : 0 < k.succ
⊢ (∏ k_1 ∈ Finset.range k, ↑(k_1 + 1 + 1) * (↑k + 1)⁻¹) * (↑(0 + 1) * (↑k + 1)⁻¹) ≤ (↑k + 1)⁻¹

Tactic:
simp only [prod_range_succ', one_mul, Nat.cast_add, zero_add, Nat.cast_one]

Result:
case intro
k : ℕ
hn : 0 < k.succ
⊢ (∏ x ∈ Finset.range k, (↑x + 1 + 1) * (↑k + 1)⁻¹) * (↑k + 1)⁻¹ ≤ (↑k + 1)⁻¹

Proof state:
case intro.refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ x + 1 + 1 ≤ k + 1

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
⊢ ↑n ! / ↑n ^ n ≤ 1 / ↑n

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩

Result:
case intro
k : ℕ
hn : 0 < k.succ
⊢ ↑k.succ ! / ↑k.succ ^ k.succ ≤ 1 / ↑k.succ

Proof state:
⊢ ∀ᶠ (b : ℕ) in atTop, ↑b ! / ↑b ^ b ≤ 1 / ↑b

Tactic:
refine (eventually_gt_atTop 0).mono fun n hn ↦ ?_

Result:
n : ℕ
hn : 0 < n
⊢ ↑n ! / ↑n ^ n ≤ 1 / ↑n

Proof state:
case intro
k : ℕ
hn : 0 < k.succ
⊢ ↑k.succ ! / ↑k.succ ^ k.succ ≤ 1 / ↑k.succ

Tactic:
rw [← prod_range_add_one_eq_factorial, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div,
  prod_natCast, Nat.cast_succ, ← Finset.prod_inv_distrib, ← prod_mul_distrib,
  Finset.prod_range_succ']

Result:
case intro
k : ℕ
hn : 0 < k.succ
⊢ (∏ k_1 ∈ Finset.range k, ↑(k_1 + 1 + 1) * (↑k + 1)⁻¹) * (↑(0 + 1) * (↑k + 1)⁻¹) ≤ (↑k + 1)⁻¹

Proof state:
case intro.refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
case intro.refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ ↑x + 1 + 1 ≤ ↑k + 1

Tactic:
norm_cast

Result:
case intro.refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ x + 1 + 1 ≤ k + 1

Proof state:
case intro
k : ℕ
hn : 0 < k.succ
⊢ (∏ x ∈ Finset.range k, (↑x + 1 + 1) * (↑k + 1)⁻¹) * (↑k + 1)⁻¹ ≤ (↑k + 1)⁻¹

Tactic:
refine
      mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_) <;>
    intro x hx <;>
  rw [Finset.mem_range] at hx

Result:
case intro.refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹

case intro.refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1