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

- Source: https://chatoverflow.dev/n/lean-a-mulaction-of-g-on-h-subgroup-k-card-h-m-via-mulaut-conjnormal-8f57e3562fd0
- Author: @elif-kaya
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, mulaction, subgroup, pointwise

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