Multiply transitive group actions, and a quest for a name

Stream: mathlib4

[Antoine Chambert-Loir]

I have two questions about #23386, in which I introduce multiply transitive group actions.
So assume that G acts on X.

1. The fact that G acts n-transitively on X is introduced as the transitivity of the group action of G on Fin n ↪ X. This group action exists because G is a group. On the other hand, the definition could be partly generalized to actions of monoids, using a more explicit formulation. For example for 2-transitivity, this is equivalent to `∀ {a b c d : X} (_ : a ≠ b) (_ : c ≠ d), ∃ g : G, g • a = c ∧ g • b = d, which makes sense for monoids.

Question 1. Is it worthwhile to have the more general definition?

2. For showing that n-transitivity implies m-transitivity when m ≤ n, one needs to extend an embedding Fin m ↪ Xto an embedding Fin n ↪ X (this requires that X has at least n elements. So I prove this:

theorem _root_.Function.Embedding.giveMeAName'
    {m n : ℕ} (hmn : m ≤ n) (hn : n ≤ ENat.card X) :
   Function.Surjective (fun x : Fin n ↪ X ↦ (Fin.castLEEmb hmn).trans x)

but the proof is slightly lengthy. Maybe there is a simpler way.

Question 2. How should this theorem be called?
There is an unprimed version for Finite X where ENat.card is replaced by Nat.card, and I also need a name for that.

[Antoine Chambert-Loir]

Let me revive this question — essentially in case @Eric Wieser or @Yaël Dillies have an immediate suggestion.

[Johan Commelin]

Minor comment: I guess the Fin 2 in (1) should be Fin n, right?