x✝ y x : ℝ
⊢ (x + sqrt (1 + x ^ 2) - (-x + sqrt (1 + x ^ 2))) / 2 = x
x✝ y x : ℝ
⊢ sinh (arsinh x) = x
rw [sinh_eq, ← arsinh_neg, exp_arsinh, exp_arsinh, neg_sq]
no goals
x✝ y x : ℝ
⊢ (x + sqrt (1 + x ^ 2) - (-x + sqrt (1 + x ^ 2))) / 2 = x
field_simp