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

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPretransitive M α
a : α
⊢ Subgroup.index (stabilizer M a) = Nat.card α
Tactic:
rw [← card_orbit_eq_stabilizer_index]
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPretransitive M α
a : α
⊢ Set.ncard (orbit M a) = Nat.card α

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPretransitive M α
a : α
⊢ Set.ncard (orbit M a) = Nat.card α
Tactic:
convert Set.ncard_univ α
State after:
case h.e'_2.h.e'_2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPretransitive M α
a : α
⊢ orbit M a = Set.univ

State before:
case h.e'_2.h.e'_2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPretransitive M α
a : α
⊢ orbit M a = Set.univ
Tactic:
exact orbit_eq_univ M a
State after:
no goals