Theorem: Nat.Combination_isPretransitive (Jordan/MulActionCombination.lean)

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ IsPretransitive (Equiv.Perm α) ↑(Combination α n)
Tactic:
apply Nat.Combination_isPretransitive_of_IsMultiplyPretransitive
State after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n

State before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Tactic:
apply Equiv.Perm.isMultiplyPretransitive
State after:
no goals