-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
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))
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})
h₂ :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • 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})
h₃ :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk) ↔
    support
          (↑(((((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
                        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg))⁻¹ :
                    MulAut ↥(alternatingGroup α)) :
                  (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
                (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk)) :
            Perm α) ⊆
        s ∧
      (Eq.{u_1 + 1} (α := Perm α)
          (↑(((((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
                        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg))⁻¹ :
                    MulAut ↥(alternatingGroup α)) :
                  (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
                (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk)) :
            Perm α)
          1 ∨
        cycleType.{u_1} (α := α)
            (↑(((((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
                          (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg))⁻¹ :
                      MulAut ↥(alternatingGroup α)) :
                    (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
                  (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk)) :
              Perm α) =
          {2, 2})
h₄ :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk) ↔
    support
          (↑((MulEquiv.symm
                    ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
                      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)) :
                  (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
                (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk)) :
            Perm α) ⊆
        s ∧
      (Eq.{u_1 + 1} (α := Perm α)
          (↑((MulEquiv.symm
                    ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
                      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)) :
                  (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
                (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk)) :
            Perm α)
          1 ∨
        cycleType.{u_1} (α := α)
            (↑((MulEquiv.symm
                      ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
                        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)) :
                    (a : ↥(alternatingGroup α)) → ↥(alternatingGroup α))
                  (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk)) :
              Perm α) =
          {2, 2})
h₅ :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk) ↔
    (↑((Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)⁻¹ *
                  Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk *
                Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg) :
            Perm α).support ⊆
        s ∧
      ((↑((Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)⁻¹ *
                  Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk *
                Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg) :
            Perm α) =
          1 ∨
        (↑((Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)⁻¹ *
                    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk *
                  Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg) :
              Perm α).cycleType =
          {2, 2})
h₆ :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk) ↔
    ((↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)⁻¹ : Perm α) * k * g).support ⊆ s ∧
      ((↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)⁻¹ : Perm α) * k * g = 1 ∨
        ((↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)⁻¹ : Perm α) * k * g).cycleType = {2, 2})
h₇ :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk) ↔
    (g⁻¹ * k * g).support ⊆ s ∧ (g⁻¹ * k * g = 1 ∨ (g⁻¹ * k * g).cycleType = {2, 2})
h₈ :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk) ↔
    (HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g⁻¹ : ConjAct (Perm α))
            k).support ⊆
        s ∧
      (HSMul.hSMul (α := ConjAct (Perm α))
            ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g⁻¹ : ConjAct (Perm α)) k =
          1 ∨
        (HSMul.hSMul (α := ConjAct (Perm α))
              ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g⁻¹ : ConjAct (Perm α)) k).cycleType =
          {2, 2})
h₉ :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk) ↔
    g⁻¹ • k.support ⊆ s ∧
      (HSMul.hSMul (α := ConjAct (Perm α))
            ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g⁻¹ : ConjAct (Perm α)) k =
          1 ∨
        (HSMul.hSMul (α := ConjAct (Perm α))
              ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g⁻¹ : ConjAct (Perm α)) k).cycleType =
          {2, 2})
h₁₀ :
  k.support ⊆ g • s ∧ (k = 1 ∨ k.cycleType = {2, 2}) ↔
    g⁻¹ • k.support ⊆ s ∧
      (HSMul.hSMul (α := ConjAct (Perm α))
            ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g⁻¹ : ConjAct (Perm α)) k =
          1 ∨
        (HSMul.hSMul (α := ConjAct (Perm α))
              ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g⁻¹ : ConjAct (Perm α)) k).cycleType =
          {2, 2})
h₁₁ :
  g⁻¹ • k.support ⊆ s ∧ (k = 1 ∨ k.cycleType = {2, 2}) ↔
    g⁻¹ • k.support ⊆ s ∧
      (HSMul.hSMul (α := ConjAct (Perm α))
            ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g⁻¹ : ConjAct (Perm α)) k =
          1 ∨
        (HSMul.hSMul (α := ConjAct (Perm α))
              ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g⁻¹ : ConjAct (Perm α)) k).cycleType =
          {2, 2})
h₁₂ :
  g⁻¹ • k.support ⊆ s ∧ (k = 1 ∨ k.cycleType = {2, 2}) ↔
    g⁻¹ • k.support ⊆ s ∧ (g⁻¹ * k * g⁻¹⁻¹ = 1 ∨ (g⁻¹ * k * g⁻¹⁻¹).cycleType = {2, 2})
h₁₃ :
  g⁻¹ • k.support ⊆ s ∧ (k = 1 ∨ k.cycleType = {2, 2}) ↔
    g⁻¹ • k.support ⊆ s ∧ (g⁻¹ * k * g⁻¹⁻¹ = 1 ∨ k.cycleType = {2, 2})
h₁₄ :
  g⁻¹ • k.support ⊆ s ∧ (k = 1 ∨ k.cycleType = {2, 2}) ↔ g⁻¹ • k.support ⊆ s ∧ (g⁻¹ * k = g⁻¹ ∨ k.cycleType = {2, 2})
⊢ 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))

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]

Premises used: MulAut.inv_apply, Equiv.Perm.support_toConjAct_eq_smul_support, Finset.subset_smul_finset_iff, MulAut.smul_def, mul_inv_eq_one, Subgroup.coe_inv, ConjAct.toConjAct_inv_smul, ConjAct.toConjAct_smul, Subgroup.coe_mul, MulAut.conj_symm_apply, Equiv.Perm.cycleType_conj, mul_eq_left, alternatingGroup.mem_map_kleinFour_ofSubtype, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, Subgroup.mk_smul