no goals
n : ℕ
⊢ choose (2 * n + 2) (n + 1) * (n + 1) = choose (2 * n + 1) n * (2 * n + 2)
rw [choose_succ_right_eq, choose_mul_succ_eq]
no goals
n : ℕ
⊢ choose (2 * n + 1) n * (2 * n + 2) = 2 * (choose (2 * n + 1) n * (n + 1))
ring
no goals
n : ℕ
⊢ 2 * (choose (2 * n + 1) n * (n + 1)) = 2 * (choose (2 * n + 1) n * (2 * n + 1 - n))
rw [two_mul n, add_assoc,
    Nat.add_sub_cancel_left]
no goals
n : ℕ
⊢ 2 * (choose (2 * n + 1) n * (2 * n + 1 - n)) = 2 * (choose (2 * n) n * (2 * n + 1))
rw [choose_mul_succ_eq]
no goals
n : ℕ
⊢ 2 * (choose (2 * n) n * (2 * n + 1)) = 2 * (2 * n + 1) * choose (2 * n) n
rw [mul_assoc, mul_comm (2 * n + 1)]