infinite_free_group_embeds_into_f2

import group_theory.semidirect_product
import group_theory.free_group

open free_group multiplicative semidirect_product

universes u v

def free_group_hom_ext {α G : Type*} [group G] {f g : free_group α →* G}
  (h : ∀ a : α, f (of a) = g (of a)) (w : free_group α) : f w = g w :=
free_group.induction_on w (by simp) h (by simp) (by simp {contextual := tt})

def free_group_equiv {α β : Type*} (h : α ≃ β) : free_group α ≃* free_group β :=
{ to_fun := free_group.map h,
  inv_fun := free_group.map h.symm,
  left_inv := λ w, begin rw [← monoid_hom.comp_apply],
    conv_rhs {rw ← monoid_hom.id_apply (free_group α) w},
     exact free_group_hom_ext (by simp) _ end,
  right_inv := λ w, begin rw [← monoid_hom.comp_apply],
    conv_rhs {rw ← monoid_hom.id_apply (free_group β) w},
     exact free_group_hom_ext (by simp) _ end,
  map_mul' := by simp }
#print monoid_hom.ext_mint
def free_group_perm {α : Type u} : equiv.perm α →* mul_aut (free_group α) :=
{ to_fun := free_group_equiv,
  map_one' := by ext; simp [free_group_equiv],
  map_mul' := by intros; ext; simp [free_group_equiv, ← free_group.map.comp] }

def phi : multiplicative ℤ →* mul_aut (free_group (multiplicative ℤ)) :=
(@free_group_perm (multiplicative ℤ)).comp 
  (mul_action.to_perm (multiplicative ℤ) (multiplicative ℤ))
#print int.to_add_gpow
example : free_group bool ≃* free_group (multiplicative ℤ) ⋊[phi] multiplicative ℤ :=
{ to_fun := free_group.lift (λ b, cond b (inl (of (of_add (0 : ℤ)))) (inr (of_add (1 : ℤ)))),
  inv_fun := semidirect_product.lift 
    (free_group.lift (λ a, of ff ^ (to_add a) * of tt * of ff ^ (-to_add a))) 
    (gpowers_hom _ (of ff)) 
    begin
      assume g,
      ext,
      apply free_group_hom_ext,
      assume b,
      simp only [mul_equiv.coe_to_monoid_hom,
        gpow_neg, function.comp_app, monoid_hom.coe_comp, gpowers_hom_apply,
        mul_equiv.map_inv, lift.of, mul_equiv.map_mul, mul_aut.conj_apply, phi,
        free_group_perm, free_group_equiv, mul_action.to_perm,
        units.smul_perm_hom, units.smul_perm],
      dsimp [free_group_equiv, units.smul_perm],
      simp [to_units, mul_assoc, gpow_add]
    end,
  left_inv := λ w, begin
    conv_rhs { rw ← monoid_hom.id_apply _ w },
    rw [← monoid_hom.comp_apply],
    apply free_group_hom_ext,
    intro a,
    cases a; refl,
  end, 
  right_inv := λ s, begin
    conv_rhs { rw ← monoid_hom.id_apply _ s },
    rw [← monoid_hom.comp_apply],
    refine congr_fun (congr_arg _ _) _,
    apply semidirect_product.hom_ext,
    { ext,
      { simp only [right_inl, mul_aut.apply_inv_self, mul_right, 
          mul_one, monoid_hom.map_mul, gpow_neg, lift_inl,
          mul_left, function.comp_app, left_inl, cond, monoid_hom.map_inv, 
          monoid_hom.coe_comp, monoid_hom.id_comp, of_add_zero,
          inv_left, lift.of, phi, free_group_perm, free_group_equiv,
          mul_action.to_perm, units.smul_perm_hom, units.smul_perm],
        dsimp [free_group_equiv, units.smul_perm],
        simp,
        simp only [← monoid_hom.map_gpow],
        simp [- monoid_hom.map_gpow],
        rw [← int.of_add_mul, one_mul],
        simp [to_units] },
      { simp } },
    { apply monoid_hom.ext_mint,
      refl }    
  end,
  map_mul' := by simp }