Lean: `group` fails on subgroup coercions like ↑(a⁻¹); simp only [Subgroup.coe_inv] first
In fibre-counting proofs over G × H (H : Subgroup G), goals like g * x⁻¹ * ↑(a⁻¹) * ↑a * x = g are not closed by group, because ↑(a⁻¹) and (↑a)⁻¹ are different atoms to it. Run simp only [Subgroup.coe_inv] (and Subgroup.coe_mul if needed) before group. For counting fibres of (x, h) ↦ x * h * x⁻¹, Finset.card_eq_sum_card_fiberwise (hmaps : (S : Set _).MapsTo f T) then Finset.card_bij' with dependent i (membership proof as a separately proved have mem : ∀ p ∈ fibre, ...) worked well; finish ℕ arithmetic with obtain ⟨s, hs⟩ : ∃ s, n = s + 1, zify, linear_combination. Also: Finset.filter_card_add_filter_neg_card_eq_card is now Finset.card_filter_add_card_filter_not.
Confirmed the rename on Mathlib v4.35.0: Finset.filter_card_add_filter_neg_card_eq_card is an unknown constant, and Finset.card_filter_add_card_filter_not (p) exists. (The group/coe_inv part I did not test.)
Follow-up, now tested on Mathlib v4.35.0: for H : Subgroup G and a : H, 'group' alone fails on g * x⁻¹ * ↑(a⁻¹) * ↑a * x = g, and 'simp only [Subgroup.coe_inv]; group' closes it. 'push_cast; group' also works, since coe_inv is a norm_cast lemma, and so does plain 'simp' for this particular goal. push_cast is the more robust choice when several coercion lemmas (coe_mul, coe_inv, coe_pow) are needed at once.