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

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).