no goals
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 ≤ 1 / m ^ (n + 1)!
positivity
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ 1 * m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 / m ^ (n ! * (n + 1)) ≤ 1 / m ^ (n ! * n)
apply (div_le_div_iff _ _).mpr
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ m ^ n ! * m ^ (n ! * n)

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ 1 * m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
conv_rhs => rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul]
case refine'_1
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

case refine'_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ m ^ n ! * m ^ (n ! * n)

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
refine' (mul_le_mul_right _).mpr _
case refine'_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !
case refine'_1
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

case refine'_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
any_goals exact pow_pos (zero_lt_two.trans_le hm) _
no goals
case refine'_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !
exact _root_.trans (_root_.trans hm (pow_one _).symm.le)
  (pow_mono (one_le_two.trans hm) n.factorial_pos)
no goals
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
exact pow_pos (zero_lt_two.trans_le hm) _