no goals
A : Type u_1
A' : Type ?u.368339
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(coeff A (bit0 n)) (cos A) = (-1) ^ n * ↑(coeff A (bit0 n)) (exp A)
rw [cos, coeff_mk, if_pos (even_bit0 n), Nat.bit0_div_two, ← mul_one_div, map_mul, map_pow,
  map_neg, map_one, coeff_exp]