But this looks a bit like rubbish, doesn’t it? That’s why such theorems are sometimes called junk theorems: they do not prove anything sensible that we would expect to be true of natural numbers. On the face of it, it surely looks wrong to calculate the intersection of two natural numbers.
From the article:
Also see Junk theorems in Lean.