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

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

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
H K : Subgroup M
hHK : K ≤ H
h : IsPretransitive (↥K) (Fin n ↪ α)
⊢ IsPretransitive (↥H) (Fin n ↪ α)
Tactic:
refine' isPretransitive_of_subgroup_le hHK h
State after:
no goals