case intro
m : ℤ
n : ℕ
⊢ 0 ≤ ∏ k in Finset.range (n + n), (m - ↑k)
m : ℤ
n : ℕ
hn : Even n
⊢ 0 ≤ ∏ k in Finset.range n, (m - ↑k)
rcases hn with ⟨n, rfl⟩
case intro.zero
m : ℤ
⊢ 0 ≤ ∏ k in Finset.range (Nat.zero + Nat.zero), (m - ↑k)

case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (n + n), (m - ↑k)
⊢ 0 ≤ ∏ k in Finset.range (Nat.succ n + Nat.succ n), (m - ↑k)
case intro
m : ℤ
n : ℕ
⊢ 0 ≤ ∏ k in Finset.range (n + n), (m - ↑k)
induction' n with n ihn
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ ∏ k in Finset.range (Nat.succ n + Nat.succ n), (m - ↑k)
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (n + n), (m - ↑k)
⊢ 0 ≤ ∏ k in Finset.range (Nat.succ n + Nat.succ n), (m - ↑k)
rw [← two_mul] at ihn
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (∏ x in Finset.range ((1 + 1) * n), (m - ↑x)) * ((m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1)))
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ ∏ k in Finset.range (Nat.succ n + Nat.succ n), (m - ↑k)
rw [← two_mul, Nat.succ_eq_add_one, mul_add, mul_one, ← one_add_one_eq_two, ← add_assoc,
  Finset.prod_range_succ, Finset.prod_range_succ, mul_assoc]
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1))
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (∏ x in Finset.range ((1 + 1) * n), (m - ↑x)) * ((m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1)))
refine' mul_nonneg ihn _
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1))
generalize (1 + 1) * n = k
case intro.succ.inl
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))

case intro.succ.inr
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : ↑k < m
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
cases' le_or_lt m k with hmk hmk
no goals
case intro.zero
m : ℤ
⊢ 0 ≤ ∏ k in Finset.range (Nat.zero + Nat.zero), (m - ↑k)
simp
case intro.succ.inl
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
this : m ≤ ↑k + 1
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
case intro.succ.inl
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
have : m ≤ k + 1 := hmk.trans (lt_add_one (k : ℤ)).le
case intro.succ.inl.convert_2
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
this : m ≤ ↑k + 1
⊢ m - ↑(k + 1) ≤ 0
case intro.succ.inl
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
this : m ≤ ↑k + 1
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
convert mul_nonneg_of_nonpos_of_nonpos (sub_nonpos_of_le hmk) _
no goals
case intro.succ.inl.convert_2
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
this : m ≤ ↑k + 1
⊢ m - ↑(k + 1) ≤ 0
convert sub_nonpos_of_le this
no goals
case intro.succ.inr
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : ↑k < m
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
exact mul_nonneg (sub_nonneg_of_le hmk.le) (sub_nonneg_of_le hmk)