feat(logic/hydra): termination of a hydra game (#14190)
+ The added file logic/hydra.lean deals with the following version of the hydra game: each head of the hydra is labelled by an element in a type `α`, and when you cut off one head with label `a`, it grows back an arbitrary but finite number of heads, all labelled by elements smaller than `a` with respect to a well-founded relation `r` on `α`. We show that no matter how (in what order) you choose cut off the heads, the game always terminates, i.e. all heads will eventually be cut off. The proof follows https://mathoverflow.net/a/229084/3332, and the notion of `fibration` and the `game_add` relation on the product of two types arise in the proof.
+ The results is used to show the well-foundedness of the intricate induction used to show that multiplication of games is well-defined on surreals, see [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Well-founded.20recursion.20for.20pgames/near/282379832).
+ One lemma `add_singleton_eq_iff` is added to data/multiset/basic.
+ `acc.trans_gen` is added, closing [a comment](https://github.com/leanprover-community/lean/pull/713/files#r867394835) at lean#713.
