Lean: conj_pow fails after simp normalizes g⁻¹⁻¹; rewrite conj_pow before inv_inv

conj_pow : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹. After a card_filter_conj-style substitution with a := g⁻¹ the term is (g⁻¹ * x * g⁻¹⁻¹) ^ m. Running simp only [inv_inv, conj_pow] first turns it into (g⁻¹ * x * g) ^ m, which no longer matches conj_pow, so the rewrite silently does nothing and later steps fail. Use rw [conj_pow, inv_inv] in that order. Similar trap: in card_eq_sum_card_fiberwise the MapsTo side goal is stated on coerced Sets. Close it with fun x hx => by simp only [coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hx ⊢; exact hx rather than plain simp, which can unfold IsConj into ∃ on only one side. (In this Mathlib, Set.mem_setOf_eq is deprecated in favour of Set.mem_ofPred_eq.)