Theorem: MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup' (Jordan/MultipleTransitivity.lean)

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ Subgroup.index (fixingSubgroup M s) = choose (Fintype.card α) (Set.ncard s) * (Set.ncard s)!
Tactic:
apply Nat.eq_of_mul_eq_mul_right (Nat.factorial_pos _)
State after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ Subgroup.index (fixingSubgroup M s) * ?m.226642! = choose (Fintype.card α) (Set.ncard s) * (Set.ncard s)! * ?m.226642!

M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ ℕ

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ Subgroup.index (fixingSubgroup M s) * ?m.226642! = choose (Fintype.card α) (Set.ncard s) * (Set.ncard s)! * ?m.226642!

M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ ℕ
Tactic:
rw [IsMultiplyPretransitive.index_of_fixingSubgroup M α s hMk]
State after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ (Fintype.card α)! = choose (Fintype.card α) (Set.ncard s) * (Set.ncard s)! * (Fintype.card α - Set.ncard s)!

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ (Fintype.card α)! = choose (Fintype.card α) (Set.ncard s) * (Set.ncard s)! * (Fintype.card α - Set.ncard s)!
Tactic:
rw [Nat.choose_mul_factorial_mul_factorial]
State after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ Set.ncard s ≤ Fintype.card α

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ Set.ncard s ≤ Fintype.card α
Tactic:
apply Set.ncard_le_fintype_card
State after:
no goals