no goals
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
n : ℕ
⊢ 0 ≤ ↑n !
exact_mod_cast n.factorial_pos.le
no goals
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
n : ℕ
⊢ 0 ≤ ↑n
exact_mod_cast n.zero_le
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
n : ℕ
hn : 0 < n
⊢ ↑n ! / ↑n ^ n ≤ 1 / ↑n
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
⊢ ∀ᶠ (b : ℕ) in atTop, ↑b ! / ↑b ^ b ≤ 1 / ↑b
refine' (eventually_gt_atTop 0).mono fun n hn => _
case intro
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
⊢ ↑(succ k)! / ↑(succ k) ^ succ k ≤ 1 / ↑(succ k)
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
n : ℕ
hn : 0 < n
⊢ ↑n ! / ↑n ^ n ≤ 1 / ↑n
rcases Nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩
case intro
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
⊢ (∏ k_1 in Finset.range k, ↑(k_1 + 1 + 1) * (↑k + 1)⁻¹) * (↑(0 + 1) * (↑k + 1)⁻¹) ≤ (↑k + 1)⁻¹
case intro
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
⊢ ↑(succ k)! / ↑(succ k) ^ succ k ≤ 1 / ↑(succ k)
rw [← prod_range_add_one_eq_factorial, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div,
  prod_natCast, Nat.cast_succ, ← prod_inv_distrib, ← prod_mul_distrib,
  Finset.prod_range_succ']
case intro
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
⊢ (∏ x in Finset.range k, (↑x + 1 + 1) * (↑k + 1)⁻¹) * (↑k + 1)⁻¹ ≤ (↑k + 1)⁻¹
case intro
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
⊢ (∏ k_1 in Finset.range k, ↑(k_1 + 1 + 1) * (↑k + 1)⁻¹) * (↑(0 + 1) * (↑k + 1)⁻¹) ≤ (↑k + 1)⁻¹
simp only [prod_range_succ', one_mul, Nat.cast_add, zero_add, Nat.cast_one]
case intro.refine'_1
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹

case intro.refine'_2
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
case intro
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
⊢ (∏ x in Finset.range k, (↑x + 1 + 1) * (↑k + 1)⁻¹) * (↑k + 1)⁻¹ ≤ (↑k + 1)⁻¹
refine'
      mul_le_of_le_one_left (inv_nonneg.mpr <| by exact_mod_cast hn.le) (prod_le_one _ _) <;>
    intro x hx <;>
  rw [Finset.mem_range] at hx
no goals
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
⊢ 0 ≤ ↑k + 1
exact_mod_cast hn.le
no goals
case intro.refine'_1
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹
refine' mul_nonneg _ (inv_nonneg.mpr _) <;> norm_cast <;> linarith
case intro.refine'_2
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ ↑x + 1 + 1 ≤ ↑k + 1
case intro.refine'_2
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
refine' (div_le_one <| by exact_mod_cast hn).mpr _
case intro.refine'_2
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ x + 1 + 1 ≤ k + 1
case intro.refine'_2
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ ↑x + 1 + 1 ≤ ↑k + 1
norm_cast
no goals
case intro.refine'_2
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ x + 1 + 1 ≤ k + 1
linarith
no goals
α : Type ?u.482700
β : Type ?u.482703
ι : Type ?u.482706
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ 0 < ↑k + 1
exact_mod_cast hn