[GOAL]
x✝ y x : ℝ
⊢ exp (arsinh x) = x + sqrt (1 + x ^ 2)
[PROOFSTEP]
apply exp_log
[GOAL]
case hx
x✝ y x : ℝ
⊢ 0 < x + sqrt (1 + x ^ 2)
[PROOFSTEP]
rw [← neg_lt_iff_pos_add']
[GOAL]
case hx
x✝ y x : ℝ
⊢ -x < sqrt (1 + x ^ 2)
[PROOFSTEP]
apply lt_sqrt_of_sq_lt
[GOAL]
case hx.h
x✝ y x : ℝ
⊢ (-x) ^ 2 < 1 + x ^ 2
[PROOFSTEP]
simp
[GOAL]
x y : ℝ
⊢ arsinh 0 = 0
[PROOFSTEP]
simp [arsinh]
[GOAL]
x✝ y x : ℝ
⊢ arsinh (-x) = -arsinh x
[PROOFSTEP]
rw [← exp_eq_exp, exp_arsinh, exp_neg, exp_arsinh]
[GOAL]
x✝ y x : ℝ
⊢ -x + sqrt (1 + (-x) ^ 2) = (x + sqrt (1 + x ^ 2))⁻¹
[PROOFSTEP]
apply eq_inv_of_mul_eq_one_left
[GOAL]
case h
x✝ y x : ℝ
⊢ (-x + sqrt (1 + (-x) ^ 2)) * (x + sqrt (1 + x ^ 2)) = 1
[PROOFSTEP]
rw [neg_sq, neg_add_eq_sub, add_comm x, mul_comm, ← sq_sub_sq, sq_sqrt, add_sub_cancel]
[GOAL]
case h
x✝ y x : ℝ
⊢ 0 ≤ 1 + x ^ 2
[PROOFSTEP]
exact add_nonneg zero_le_one (sq_nonneg _)
[GOAL]
x✝ y x : ℝ
⊢ sinh (arsinh x) = x
[PROOFSTEP]
rw [sinh_eq, ← arsinh_neg, exp_arsinh, exp_arsinh, neg_sq]
[GOAL]
x✝ y x : ℝ
⊢ (x + sqrt (1 + x ^ 2) - (-x + sqrt (1 + x ^ 2))) / 2 = x
[PROOFSTEP]
field_simp
[GOAL]
x✝ y x : ℝ
⊢ cosh (arsinh x) = sqrt (1 + x ^ 2)
[PROOFSTEP]
rw [← sqrt_sq (cosh_pos _).le, cosh_sq', sinh_arsinh]
[GOAL]
x y : ℝ
⊢ 0 ≤ arsinh x ↔ 0 ≤ x
[PROOFSTEP]
rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
[GOAL]
x y : ℝ
⊢ arsinh x ≤ 0 ↔ x ≤ 0
[PROOFSTEP]
rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
[GOAL]
x✝ y x : ℝ
⊢ HasStrictDerivAt arsinh (sqrt (1 + x ^ 2))⁻¹ x
[PROOFSTEP]
convert
  sinhHomeomorph.toLocalHomeomorph.hasStrictDerivAt_symm (mem_univ x) (cosh_pos _).ne' (hasStrictDerivAt_sinh _) using 2
[GOAL]
case h.e'_7.h.e'_3
x✝ y x : ℝ
⊢ sqrt (1 + x ^ 2) = cosh (↑(LocalHomeomorph.symm (Homeomorph.toLocalHomeomorph sinhHomeomorph)) x)
[PROOFSTEP]
exact (cosh_arsinh _).symm
