ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Words.NielsenSchreierCompat

@[reducible] noncomputable def FreeGroupBasis.actionGroupoidIsFree
    {ι G A : Type u} [Group G] [MulAction G A] (b : FreeGroupBasis ι G) :
    IsFreeGroupoid (ActionCategory G A) where
  quiverGenerators :=
    ⟨fun a b' => { i : ι // b i • a.back = b'.back }⟩
  of := fun (e : Subtype _) => ⟨b e, e.property⟩
  unique_lift := by
    intro X _ f
    let f' : ι → (A → X) ⋊[mulAutArrow] G := fun i =>
      ⟨fun a =>
          @f ⟨(), (b i)⁻¹ • a⟩ ⟨(), a⟩
            ⟨i, smul_inv_smul (b i) a⟩,
        b i⟩
    let F' : G →* (A → X) ⋊[mulAutArrow] G := b.lift f'
    have hF' : ∀ i, F' (b i) = f' i := congrFun (b.lift.left_inv f')
    refine ⟨uncurry F' ?_, ?_, ?_⟩
    · intro g
      suffices SemidirectProduct.rightHom.comp F' = MonoidHom.id G by
        exact DFunLike.ext_iff.mp this g
      apply b.ext_hom
      intro i
      rw [MonoidHom.comp_apply, hF' i]
      rfl
    · rintro ⟨⟨⟩, a : A⟩ ⟨⟨⟩, b'⟩ ⟨i, h : b i • a = b'⟩
      change (F' (b i)).left _ = _
      rw [hF' i]
      cases inv_smul_eq_iff.mpr h.symm
      rfl
    · intro E hE
      have hcurried : curry E = F' := by
        apply b.ext_hom
        intro i
        rw [hF' i]
        apply SemidirectProduct.ext
        · funext a
          exact hE ⟨(), (b i)⁻¹ • a⟩ ⟨(), a⟩ ⟨i, smul_inv_smul (b i) a⟩
        · rfl
      apply Functor.hext
      · intro
        apply Unit.ext
      · refine ActionCategory.cases ?_
        intro t g
        simp only [← hcurried, uncurry_map, curry_apply_left, coe_back, homOfPair.val]
        rfl