coprodEquivSemidirectProduct

open Monoid Monoid.Coprod SemidirectProduct

-- def Monoid.CoprodI.mapEquivHom (ι M : Type*) [Monoid M] :
--     Equiv.Perm ι →* MulAut (Monoid.CoprodI (fun _ : ι => M)) :=
--   { toFun := fun e =>
--       MonoidHom.toMulEquiv
--         (Monoid.CoprodI.lift (fun i =>
--           CoprodI.of (M := fun _ : ι => M) (i := e i)))
--         (Monoid.CoprodI.lift (fun i =>
--           CoprodI.of (M := fun _ : ι => M) (i := e.symm i)))
--         (CoprodI.ext_hom _ _ (fun _ => by ext; simp))
--         (CoprodI.ext_hom _ _ (fun _ => by ext; simp))
--     map_one' := MulEquiv.toMonoidHom_injective
--       (CoprodI.ext_hom _ _ (fun _ => by ext; simp))
--     map_mul' := fun _ _ => MulEquiv.toMonoidHom_injective
--       (CoprodI.ext_hom _ _ (fun _ => by ext; simp)) }

-- @[simp] theorem Monoid.CoprodI.mapEquivHom_of (ι M : Type*) [Monoid M]
--     (e : Equiv.Perm ι) (i : ι) (m : M) :
--     Monoid.CoprodI.mapEquivHom ι M e (CoprodI.of (M := fun _ : ι => M) (i := i) m) =
--       CoprodI.of (M := fun _ : ι => M) (i := e i) m := by
--   simp [Monoid.CoprodI.mapEquivHom]

-- def coprodEquivSemidirectProduct (G H : Type*) [Group G] [Group H] :
--     (G ∗ H) ≃* Monoid.CoprodI (fun _ : H => G)
--       ⋊[(CoprodI.mapEquivHom H G).comp (MulAction.toPermHom _ _)] H :=
--   MonoidHom.toMulEquiv
--     (Coprod.lift
--       (inl.comp (CoprodI.of (M := fun _ : H => G) (i := 1)))
--       inr)
--     (SemidirectProduct.lift
--       (CoprodI.lift (fun h : H => (MulAut.conj (Coprod.inr h)).toMonoidHom.comp
--         Coprod.inl))
--       inr
--       (fun h => CoprodI.ext_hom _ _
--         (fun h₂ => by ext; simp [CoprodI.mapEquivHom])))
--     (Coprod.ext_hom _ _ (by ext; simp) (by ext; simp))