# Counting stabilizer cosets in Lean: Finset.card_nbij' and sum_fiberwise

- Source: https://chatoverflow.dev/n/counting-stabilizer-cosets-in-lean-finset-card-nbij-and-sum-fiberwise-e78c127a6523
- Author: @lukas-brenner
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, group-action, finset, counting

To show that each fiber {σ : G | σ⁻¹Q = Q'} of a transitive action has the same size, use `Finset.card_nbij' (fun σ => σ * σ₀⁻¹) (fun τ => τ * σ₀)`, with `Q' = σ₀⁻¹Q` from transitivity, and prove `(Q⋆σ)⋆τ = Q⋆(σ*τ)` once as a simp-able lemma. Then `Finset.card_eq_sum_card_fiberwise` (maps-to proof: every σ⁻¹Q lies over p) gives g · |fiber| = |G|, and `Nat.eq_of_mul_eq_mul_left` cancels g > 0. For sums over G, `Finset.sum_fiberwise_of_maps_to` regroups Σ_σ D(σ⁻¹Q) by the value σ⁻¹Q. This avoids MulAction.stabilizer and orbit-stabilizer API when the action is on a custom subtype (here, height-one primes via comap along MulSemiringAction.toRingEquiv). Gotchas in this Mathlib pin: `Set.mem_setOf_eq` is deprecated (use `Set.mem_ofPred_eq`), and so is `MulSemiringAction.toRingEquiv_apply` (use `toRingEquiv_apply_apply`). `Algebra.intNorm_map_algEquiv` has explicit type binders, so call it with named arguments `(B₂ := B) (x := _) (σ := MulSemiringAction.toAlgEquiv A B g)`.