How can I make Mathematica do, ArcTanh[x] + ArcTanh[y] = ArcTanh[x+y/1+xy]?

A little bit of trickery:

ArcTanh[x] + ArcTanh[y] // Tanh // TrigExpand // FullSimplify // ArcTanh

   (* ArcTanh[(x + y)/(1 + x y)] *)

Note the parentheses.

Probably, MathematicalFunctionData["ArcTanh"] knows about this.

First let's see what categories of things are known:

MathematicalFunctionData["ArcTanh", "Properties"]

ah well, let's just list them all (this will take a while to download the first time around)

all = DeleteDuplicates@Flatten[MathematicalFunctionData["ArcTanh", #] & /@ 
 MathematicalFunctionData["ArcTanh", "Properties"]];

now let's look whether that fact about ArcTanh[_] + ArcTanh[_] is in there

facts = Cases[all,
  Function[{_, _}, 
   e_ /; Not@FreeQ[e, Inactivate[ArcTanh[_] + ArcTanh[_]]]]
  ];

maybe some of these help. Let's Activate them.

activefacts = Through[facts[x, y]] // Activate  

drop some conditions

activefacts = Assuming[x \[Element] Reals && y \[Element] Reals, FullSimplify@activefacts];

Now

activefacts /. {x -> ..., y -> ...}

should be a list of True, Undefined or Indeterminate == ... for any real x and y.

(However, it seems to break here for exactly one of them being 1, the other not, activefacts /. {x -> 1, y -> 0.9} is {False, Undefined, False})

---

I think this is a method worth knowing in general.

For example, use

all = MathematicalFunctionData["Sinh", #] & /@ 
   MathematicalFunctionData["Sinh", "Properties"];
all = Flatten@all;
Cases[all,
 Function[{_, _}, e_ /; Not@FreeQ[e, Inactivate@Sinh[_ + _]]]
 ]

to learn everything MathematicalFunctionData knows about $\sinh(x + y)$.

This is just not true for all (x,y):

(ArcTanh[x] + ArcTanh[y] - ArcTanh[x + y/(1 - x y)]) /. x -> 0.23 /.y -> .323

-0.0916564

or

(ArcTanh[x] + ArcTanh[y] - ArcTanh[(x + y)/(1 - x y)]) /.x -> 0.23 /. y -> .323

-0.11988

Solve[ArcTanh[x] + ArcTanh[y] == ArcTanh[x + y/(1 - x)], {x, y}]

{{x -> 0}, {y -> 0}, {y -> -1 - x + x^2}}