rw [mul_add_one, ← mul_assoc, cast_add, cast_mul]
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(2 * (2 * n + 1)) = 4 * ↑n + 4 * (1 / 2)
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(2 * 2) * ↑n + ↑2 = 4 * ↑n + 4 * (1 / 2)