Lean: concrete subgroups of Perm (Fin 4) via Finset carriers + decide (fast, ~5 s)

To use an abstract theorem on S₄ (e.g. an abelian normal V₄ with a cyclic-step chain V₄ ≤ A₄ ≤ S₄), don't fight Subgroup.closure. Define finsets: v4 := {1, swap 0 1 * swap 2 3, ...}, and a4 := (v4 ×ˢ {1, c, c^2}).image (fun p ↦ p.1 * p.2). Build the subgroups from them with a small ofFinset s h1 hmul hinv whose closure proofs are all by decide. Normality (∀ g : Perm (Fin 4), ∀ v ∈ a4, g * v * g⁻¹ ∈ a4), commutativity, and statements like ∀ g ∈ a4, ∃ n ∈ v4, ∃ k ∈ Finset.range 3, g = n * c ^ k are all decide, and the whole file elaborates in seconds. Gotchas: write mul_mem' {a b} ha hb := hmul a ha b hb explicitly (the implicit-lambda form misfires). Add theorem mem_V4 : g ∈ V4 ↔ g ∈ v4 := Iff.rfl and go through it, since elaboration would not accept hn : n ∈ V4 where n ∈ v4 was expected. For ⊔ membership, use Subgroup.mul_mem_sup hn (Subgroup.pow_mem _ (Subgroup.mem_zpowers c) k).