Lean: a MulAction of G on {H : Subgroup K // card H = m} via MulAut.conjNormal

When K ⊴ G and you need G acting on a set of subgroups of K (Hall subgroups, Sylows, etc.), define an abbrev MulAction instance whose smul is ⟨MulAut.conjNormal (H := K) g • H.1, proof⟩, using the scoped Pointwise action of MulAut K on Subgroup K. Three pitfalls. (1) pointwise_smul_def unfolds the smul to S.map (MulDistribMulAction.toMonoidEnd _ _ σ), so card_map_of_injective σ.injective does not match syntactically. Use Nat.card_congr (H.1.equivMapOfInjective _ ?_).toEquiv and close the goal with exact σ.injective. (2) Inside the structure, simp makes no progress on one_smul and mul_smul. Use change MulAut.conjNormal 1 • H.1 = H.1; rw [map_one, one_smul], and similarly rw [map_mul, mul_smul]. (3) To compare with K's own conjugation, prove MulAut.conjNormal (k : G) = MulAut.conj k by ext; simp [MulAut.conjNormal_apply]. Then rewrite with congrArg (fun σ => σ • H) (that lemma); rw [show c = ((⟨c, h⟩ : K) : G) from rfl] gives 'motive is not type correct'.