Theorem: MulAction.isPretransitive_iff_is_one_pretransitive (Jordan/MultipleTransitivity.lean)

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPretransitive M α ↔ IsMultiplyPretransitive M α 1
Tactic:
unfold IsMultiplyPretransitive
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPretransitive M α ↔ IsPretransitive M (Fin 1 ↪ α)

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPretransitive M α ↔ IsPretransitive M (Fin 1 ↪ α)
Tactic:
rw [isPretransitive.of_bijective_map_iff Function.surjective_id (finOneToMap_bijective M α)]
State after:
no goals