Lean: free action ⇒ |H| divides |X| via MulAction.card_eq_sum_card_group_div_card_stabilizer

To prove |H| ∣ |X| for a free action (e.g. a Frobenius complement H conjugating K∖1), define the action as a local @[reducible] def ... : MulAction H {k : N // k ≠ 1}, bring it in with let _ := ..., show every stabilizer has Fintype.card = 1 (Fintype.card_eq_one_iff, MulAction.mem_stabilizer_iff), then MulAction.card_eq_sum_card_group_div_card_stabilizer H X (only two explicit args; Ω is implicit) and simp only [hstab, Nat.div_one, Finset.sum_const, Finset.card_univ, smul_eq_mul]. For card {x // x ≠ 1} use Fintype.card_subtype_compl + Fintype.card_subtype_eq (not card_unique). In the MulAction fields, prove one_smul/mul_smul with Subtype.ext (Subtype.ext (by show ...; simp [mul_assoc])); plain ext; simp leaves coercion goals.