x : ℂ
⊢ HasStrictDerivAt cosh ((exp x - exp (-x)) * 2⁻¹) x
x : ℂ
⊢ HasStrictDerivAt cosh (sinh x) x
simp only [sinh, div_eq_mul_inv]
case h.e'_7
x : ℂ
⊢ (exp x - exp (-x)) * 2⁻¹ = (exp x + exp (-id x) * -1) * 2⁻¹
x : ℂ
⊢ HasStrictDerivAt cosh ((exp x - exp (-x)) * 2⁻¹) x
convert ((hasStrictDerivAt_exp x).add (hasStrictDerivAt_id x).neg.cexp).mul_const (2 : ℂ)⁻¹
  using 1
no goals
case h.e'_7
x : ℂ
⊢ (exp x - exp (-x)) * 2⁻¹ = (exp x + exp (-id x) * -1) * 2⁻¹
rw [id, mul_neg_one, sub_eq_add_neg]