-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
h :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α))
      (Subgroup.map (ofSubtype (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s))
        (kleinFour ↥(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s)))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk) ↔
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s))
      (HSMul.hSMul (α := MulAut ↥(alternatingGroup α))
        (((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
              (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg))⁻¹ :
          MulAut ↥(alternatingGroup α))
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk))
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α))
      (Subgroup.map (ofSubtype (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s))
        (kleinFour ↥(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s)))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk) ↔
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk ∈
      HSMul.hSMul (α := MulAut ↥(alternatingGroup α)) (β := Subgroup ↥(alternatingGroup α))
        ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg) :
          MulAut ↥(alternatingGroup α))
        (Subgroup.map (ofSubtype s) (kleinFour ↥s))
have h₁ : Membership.mem (γ := Subgroup ↥(alternatingGroup α))
    (Subgroup.map (ofSubtype (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s))
      (kleinFour ↥(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s)))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk) ↔
  (↑(HSMul.hSMul (α := MulAut ↥(alternatingGroup α))
              (((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
                    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg))⁻¹ :
                MulAut ↥(alternatingGroup α))
              (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk)) :
          Perm α).support ⊆
      s ∧
    ((↑(HSMul.hSMul (α := MulAut ↥(alternatingGroup α))
              (((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
                    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg))⁻¹ :
                MulAut ↥(alternatingGroup α))
              (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk)) :
          Perm α) =
        1 ∨
      (↑(HSMul.hSMul (α := MulAut ↥(alternatingGroup α))
                (((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
                      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg))⁻¹ :
                  MulAut ↥(alternatingGroup α))
                (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk)) :
            Perm α).cycleType =
        {2, 2})
Tactic: simp_rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, mem_map_kleinFour_ofSubtype hs,
    Subgroup.mk_smul, MulAut.smul_def, MulAut.inv_apply, MulAut.conj_symm_apply, Subgroup.coe_mul,
    Subgroup.coe_inv, ← ConjAct.toConjAct_inv_smul, Equiv.Perm.support_toConjAct_eq_smul_support,
    mem_map_kleinFour_ofSubtype (s := g • s) (by simpa), Finset.subset_smul_finset_iff,
    ConjAct.toConjAct_smul, cycleType_conj, mul_inv_eq_one, mul_eq_left]