rw [mul_div_assoc', mul_add, eq_div_iff, ← cast_add_one, div_mul_eq_mul_div, mul_comm, ← cast_mul,
  succ_mul_centralBinom_succ, cast_mul, mul_div_cancel]
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(centralBinom (n + 1)) / ↑(centralBinom n) = 4 * ((↑n + 1 / 2) / (↑n + 1))
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(2 * (2 * n + 1)) = 4 * ↑n + 4 * (1 / 2)

case h
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(centralBinom n) ≠ 0

α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑n + 1 ≠ 0