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

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
K : Subgroup M
h : IsMultiplyPretransitive (↥K) α n
⊢ IsMultiplyPretransitive M α n
Tactic:
unfold IsMultiplyPretransitive at *
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
K : Subgroup M
h : IsPretransitive (↥K) (Fin n ↪ α)
⊢ IsPretransitive M (Fin n ↪ α)

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
K : Subgroup M
h : IsPretransitive (↥K) (Fin n ↪ α)
⊢ IsPretransitive M (Fin n ↪ α)
Tactic:
exact isPretransitive_of_subgroup h
State after:
no goals