countableFreeGroup

import Mathlib.GroupTheory.SemidirectProduct
import Mathlib.GroupTheory.FreeGroup

open FreeGroup SemidirectProduct Multiplicative

def freeAction : Multiplicative ℤ →* MulAut (FreeGroup (Multiplicative ℤ)) :=
  zpowersHom _ (freeGroupCongr (MulAction.toPermHom (Multiplicative ℤ)
    (Multiplicative ℤ) (ofAdd 1)))
#print mint
example : FreeGroup Bool ≃*
    (FreeGroup (Multiplicative ℤ) ⋊[freeAction] Multiplicative ℤ) :=
  MonoidHom.toMulEquiv
    (FreeGroup.lift (fun b => if b then inl (of 1) else inr (ofAdd 1)))
    (SemidirectProduct.lift (FreeGroup.lift (fun z =>
      MulAut.conj (zpowersHom _ (of false) z) (of true)))
        (zpowersHom _ (of false))
        (by
          intro g
          rcases ofAdd.surjective g with ⟨z, rfl⟩
          ext s
          simp [MulAut.conj_apply, freeAction, MulAction.toPerm_apply]
          induction z using Int.induction_on generalizing s with
          | hz => simp
          | hp z ih =>
            rw [← map_zpow, ← map_zpow, zpow_add, MulAut.mul_apply,
              zpow_one, freeGroupCongr_apply, map.of, ih, MulAction.toPerm_apply,
              smul_eq_mul, toAdd_mul, toAdd_ofAdd, ← MulAut.mul_apply,
              ← MulAut.mul_apply, ← zpow_add, ← add_assoc, zpow_add]
            simp [sub_eq_add_neg]
          | hn z ih =>
            rw [← map_zpow, ← map_zpow, zpow_sub, MulAut.mul_apply,
              MulAut.inv_def, zpow_one, freeGroupCongr_symm,
              freeGroupCongr_apply, map.of, ih, MulAction.toPerm_symm_apply,
              smul_eq_mul, toAdd_mul, toAdd_inv, toAdd_ofAdd, ← MulAut.mul_apply,
              ← MulAut.mul_apply, ← zpow_add, ← add_assoc, zpow_add]
            simp [sub_eq_add_neg]))
    (by ext b; cases b <;> simp)
    (by
      apply SemidirectProduct.hom_ext
      · apply FreeGroup.ext_hom
        simp
        simp only [← map_zpow, MulAut.conj_apply]
        simp only [_root_.map_mul, map_zpow, lift.of, if_false, if_true,
          _root_.map_inv]
        simp only [← map_zpow, ← inl_aut, ← _root_.map_inv, freeAction,
          freeGroupCongr_apply, zpowersHom_apply]
        simp [MulAction.toPermHom_apply, MulAction.toPerm_apply, Int.toAdd_zpow, toAdd_ofAdd, one_mul, inl_inj]
        intro a
        rcases ofAdd.surjective a with ⟨z, rfl⟩
        rw [toAdd_ofAdd]
        induction z using Int.induction_on with
        | hz => simp
        | hp z ih =>
          rw [add_comm, zpow_add, MulAut.mul_apply, ih]
          simp
        | hn z ih =>
          rw [sub_eq_add_neg, add_comm, zpow_add, MulAut.mul_apply, ih]
          simp [MulAut.inv_def]
      · apply MonoidHom.ext_mint
        simp)