x✝ y x : ℝ
⊢ -x + sqrt (1 + (-x) ^ 2) = (x + sqrt (1 + x ^ 2))⁻¹
x✝ y x : ℝ
⊢ arsinh (-x) = -arsinh x
rw [← exp_eq_exp, exp_arsinh, exp_neg, exp_arsinh]
case h
x✝ y x : ℝ
⊢ (-x + sqrt (1 + (-x) ^ 2)) * (x + sqrt (1 + x ^ 2)) = 1
x✝ y x : ℝ
⊢ -x + sqrt (1 + (-x) ^ 2) = (x + sqrt (1 + x ^ 2))⁻¹
apply eq_inv_of_mul_eq_one_left
case h
x✝ y x : ℝ
⊢ 0 ≤ 1 + x ^ 2
case h
x✝ y x : ℝ
⊢ (-x + sqrt (1 + (-x) ^ 2)) * (x + sqrt (1 + x ^ 2)) = 1
rw [neg_sq, neg_add_eq_sub, add_comm x, mul_comm, ← sq_sub_sq, sq_sqrt, add_sub_cancel]
no goals
case h
x✝ y x : ℝ
⊢ 0 ≤ 1 + x ^ 2
exact add_nonneg zero_le_one (sq_nonneg _)