x : ℂ
⊢ HasStrictDerivAt cos (-(exp (-x * I) - exp (x * I)) * I * 2⁻¹) x
x : ℂ
⊢ HasStrictDerivAt cos (-sin x) x
simp only [sin, div_eq_mul_inv, neg_mul_eq_neg_mul]
case h.e'_7
x : ℂ
⊢ -(exp (-x * I) - exp (x * I)) * I * 2⁻¹ = (exp (id x * I) * (1 * I) + exp (-id x * I) * (-1 * I)) * 2⁻¹
x : ℂ
⊢ HasStrictDerivAt cos (-(exp (-x * I) - exp (x * I)) * I * 2⁻¹) x
convert (((hasStrictDerivAt_id x).mul_const I).cexp.add
  ((hasStrictDerivAt_id x).neg.mul_const I).cexp).mul_const (2 : ℂ)⁻¹ using 1
case h.e'_7
x : ℂ
⊢ -(exp (-x * I) - exp (x * I)) * I * 2⁻¹ = (exp (x * I) * (1 * I) + exp (-x * I) * (-1 * I)) * 2⁻¹
case h.e'_7
x : ℂ
⊢ -(exp (-x * I) - exp (x * I)) * I * 2⁻¹ = (exp (id x * I) * (1 * I) + exp (-id x * I) * (-1 * I)) * 2⁻¹
simp only [Function.comp, id]
no goals
case h.e'_7
x : ℂ
⊢ -(exp (-x * I) - exp (x * I)) * I * 2⁻¹ = (exp (x * I) * (1 * I) + exp (-x * I) * (-1 * I)) * 2⁻¹
ring