[GOAL]
x : ℂ
⊢ HasStrictDerivAt sin (cos x) x
[PROOFSTEP]
simp only [cos, div_eq_mul_inv]
[GOAL]
x : ℂ
⊢ HasStrictDerivAt sin ((exp (x * I) + exp (-x * I)) * 2⁻¹) x
[PROOFSTEP]
convert
  ((((hasStrictDerivAt_id x).neg.mul_const I).cexp.sub ((hasStrictDerivAt_id x).mul_const I).cexp).mul_const
        I).mul_const
    (2 : ℂ)⁻¹ using
  1
[GOAL]
case h.e'_7
x : ℂ
⊢ (exp (x * I) + exp (-x * I)) * 2⁻¹ = (exp (-id x * I) * (-1 * I) - exp (id x * I) * (1 * I)) * I * 2⁻¹
[PROOFSTEP]
simp only [Function.comp, id]
[GOAL]
case h.e'_7
x : ℂ
⊢ (exp (x * I) + exp (-x * I)) * 2⁻¹ = (exp (-x * I) * (-1 * I) - exp (x * I) * (1 * I)) * I * 2⁻¹
[PROOFSTEP]
rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc, I_mul_I, mul_neg_one,
  sub_neg_eq_add, add_comm]
[GOAL]
x : ℂ
⊢ HasStrictDerivAt cos (-sin x) x
[PROOFSTEP]
simp only [sin, div_eq_mul_inv, neg_mul_eq_neg_mul]
[GOAL]
x : ℂ
⊢ HasStrictDerivAt cos (-(exp (-x * I) - exp (x * I)) * I * 2⁻¹) x
[PROOFSTEP]
convert
  (((hasStrictDerivAt_id x).mul_const I).cexp.add ((hasStrictDerivAt_id x).neg.mul_const I).cexp).mul_const
    (2 : ℂ)⁻¹ using
  1
[GOAL]
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⁻¹
[PROOFSTEP]
simp only [Function.comp, id]
[GOAL]
case h.e'_7
x : ℂ
⊢ -(exp (-x * I) - exp (x * I)) * I * 2⁻¹ = (exp (x * I) * (1 * I) + exp (-x * I) * (-1 * I)) * 2⁻¹
[PROOFSTEP]
ring
[GOAL]
x : ℂ
⊢ HasStrictDerivAt sinh (cosh x) x
[PROOFSTEP]
simp only [cosh, div_eq_mul_inv]
[GOAL]
x : ℂ
⊢ HasStrictDerivAt sinh ((exp x + exp (-x)) * 2⁻¹) x
[PROOFSTEP]
convert ((hasStrictDerivAt_exp x).sub (hasStrictDerivAt_id x).neg.cexp).mul_const (2 : ℂ)⁻¹ using 1
[GOAL]
case h.e'_7
x : ℂ
⊢ (exp x + exp (-x)) * 2⁻¹ = (exp x - exp (-id x) * -1) * 2⁻¹
[PROOFSTEP]
rw [id, mul_neg_one, sub_eq_add_neg, neg_neg]
[GOAL]
x : ℂ
⊢ HasStrictDerivAt cosh (sinh x) x
[PROOFSTEP]
simp only [sinh, div_eq_mul_inv]
[GOAL]
x : ℂ
⊢ HasStrictDerivAt cosh ((exp x - exp (-x)) * 2⁻¹) x
[PROOFSTEP]
convert ((hasStrictDerivAt_exp x).add (hasStrictDerivAt_id x).neg.cexp).mul_const (2 : ℂ)⁻¹ using 1
[GOAL]
case h.e'_7
x : ℂ
⊢ (exp x - exp (-x)) * 2⁻¹ = (exp x + exp (-id x) * -1) * 2⁻¹
[PROOFSTEP]
rw [id, mul_neg_one, sub_eq_add_neg]
[GOAL]
x y z : ℝ
⊢ ∀ (x : ℝ), 0 < deriv sinh x
[PROOFSTEP]
rw [Real.deriv_sinh]
[GOAL]
x y z : ℝ
⊢ ∀ (x : ℝ), 0 < cosh x
[PROOFSTEP]
exact cosh_pos
[GOAL]
x y z : ℝ
⊢ 0 < sinh x ↔ 0 < x
[PROOFSTEP]
simpa only [sinh_zero] using @sinh_lt_sinh 0 x
[GOAL]
x y z : ℝ
⊢ sinh x ≤ 0 ↔ x ≤ 0
[PROOFSTEP]
simpa only [sinh_zero] using @sinh_le_sinh x 0
[GOAL]
x y z : ℝ
⊢ sinh x < 0 ↔ x < 0
[PROOFSTEP]
simpa only [sinh_zero] using @sinh_lt_sinh x 0
[GOAL]
x y z : ℝ
⊢ 0 ≤ sinh x ↔ 0 ≤ x
[PROOFSTEP]
simpa only [sinh_zero] using @sinh_le_sinh 0 x
[GOAL]
x✝ y z x : ℝ
⊢ |sinh x| = sinh |x|
[PROOFSTEP]
cases le_total x 0
[GOAL]
case inl
x✝ y z x : ℝ
h✝ : x ≤ 0
⊢ |sinh x| = sinh |x|
[PROOFSTEP]
simp [abs_of_nonneg, abs_of_nonpos, *]
[GOAL]
case inr
x✝ y z x : ℝ
h✝ : 0 ≤ x
⊢ |sinh x| = sinh |x|
[PROOFSTEP]
simp [abs_of_nonneg, abs_of_nonpos, *]
[GOAL]
x✝ y z x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv cosh x
[PROOFSTEP]
rw [interior_Ici, mem_Ioi] at hx 
[GOAL]
x✝ y z x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x
[PROOFSTEP]
rwa [deriv_cosh, sinh_pos_iff]
[GOAL]
x✝ y z x : ℝ
⊢ |0| ≤ |x|
[PROOFSTEP]
simp only [_root_.abs_zero, _root_.abs_nonneg]
[GOAL]
x y z : ℝ
⊢ |0| < |x| ↔ x ≠ 0
[PROOFSTEP]
simp only [_root_.abs_zero, abs_pos]
[GOAL]
x y z : ℝ
⊢ StrictMono fun x => sinh x - x
[PROOFSTEP]
refine' strictMono_of_odd_strictMonoOn_nonneg (fun x => by simp; abel) _
[GOAL]
x✝ y z x : ℝ
⊢ sinh (-x) - -x = -(sinh x - x)
[PROOFSTEP]
simp
[GOAL]
x✝ y z x : ℝ
⊢ -sinh x + x = x - sinh x
[PROOFSTEP]
abel
[GOAL]
x✝ y z x : ℝ
⊢ -sinh x + x = x - sinh x
[PROOFSTEP]
abel
[GOAL]
x y z : ℝ
⊢ StrictMonoOn (fun x => sinh x - x) (Ici 0)
[PROOFSTEP]
refine' (convex_Ici _).strictMonoOn_of_deriv_pos _ fun x hx => _
[GOAL]
case refine'_1
x y z : ℝ
⊢ ContinuousOn (fun x => sinh x - x) (Ici 0)
[PROOFSTEP]
exact (continuous_sinh.sub continuous_id).continuousOn
[GOAL]
case refine'_2
x✝ y z x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv (fun x => sinh x - x) x
[PROOFSTEP]
rw [interior_Ici, mem_Ioi] at hx 
[GOAL]
case refine'_2
x✝ y z x : ℝ
hx : 0 < x
⊢ 0 < deriv (fun x => sinh x - x) x
[PROOFSTEP]
rw [deriv_sub, deriv_sinh, deriv_id'', sub_pos, one_lt_cosh]
[GOAL]
case refine'_2
x✝ y z x : ℝ
hx : 0 < x
⊢ x ≠ 0
case refine'_2.hf
x✝ y z x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x => sinh x) x
case refine'_2.hg x✝ y z x : ℝ hx : 0 < x ⊢ DifferentiableAt ℝ (fun x => x) x
[PROOFSTEP]
exacts [hx.ne', differentiableAt_sinh, differentiableAt_id]
[GOAL]
x y z : ℝ
⊢ x ≤ sinh x ↔ sinh 0 - 0 ≤ sinh x - x
[PROOFSTEP]
simp
[GOAL]
x y z : ℝ
⊢ sinh x ≤ x ↔ sinh x - x ≤ sinh 0 - 0
[PROOFSTEP]
simp
