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

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

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ Nat.card ↑(orbit M a) = Subgroup.index (stabilizer M a)
Tactic:
apply Nat.card_congr
State after:
case f
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ ↑(orbit M a) ≃ M ⧸ stabilizer M a

State before:
case f
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ ↑(orbit M a) ≃ M ⧸ stabilizer M a
Tactic:
exact orbitEquivQuotientStabilizer M a
State after:
no goals