-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
Goal:
G A : Type u
inst : Group G
inst_1 : IsFreeGroup G
inst_2 : MulAction G A
X : Type u
inst_3 : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun (e : IsFreeGroup.Generators G) ↦
    ⟨fun (b : A) ↦
      f (a :=
        Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
          ((IsFreeGroup.of e)⁻¹ • b))
        (b := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b)
        (Subtype.mk (p := fun (e_1 : IsFreeGroup.Generators G) ↦
          HSMul.hSMul (β := A) (IsFreeGroup.of e_1)
              (ActionCategory.back (M := G)
                (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
                  ((IsFreeGroup.of e)⁻¹ • b))) =
            ActionCategory.back (M := G)
              (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b))
          e ⋯),
      IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), (F' : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun (F : G →* (A → X) ⋊[mulAutArrow] G) ↦
          ∀ (a : IsFreeGroup.Generators G), (F : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a)
        y →
      y = F'
a : A
b : Functor.obj (actionAsFunctor G A) PUnit.unit
e : IsFreeGroup.Generators G
h : IsFreeGroup.of e • a = b
refine_2 :
  ∀ (h : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b),
    (f'
            (↑(Subtype.mk (p := fun (e_1 : IsFreeGroup.Generators G) ↦
                  HSMul.hSMul (β := A) (IsFreeGroup.of e_1)
                      (ActionCategory.back (M := G)
                        (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                          PUnit.unit ((IsFreeGroup.of e)⁻¹ • b))) =
                    ActionCategory.back
                      (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                        PUnit.unit b))
                  e h) :
              IsFreeGroup.Generators G)).left
        (ActionCategory.back
          (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit b)) =
      f (a :=
        Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit
          ((IsFreeGroup.of e)⁻¹ • b))
        (b := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit b)
        (Subtype.mk (p := fun (e_1 : IsFreeGroup.Generators G) ↦
          HSMul.hSMul (β := A) (IsFreeGroup.of e_1)
              (ActionCategory.back (M := G)
                (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit
                  ((IsFreeGroup.of e)⁻¹ • b))) =
            ActionCategory.back
              (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit b))
          e h)
⊢ (f'
          (↑(Subtype.mk (p := fun (e : IsFreeGroup.Generators G) ↦
                HSMul.hSMul (β := A) (IsFreeGroup.of e)
                    (ActionCategory.back (M := G)
                      (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                        PUnit.unit a)) =
                  ActionCategory.back
                    (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                      PUnit.unit b))
                e h) :
            IsFreeGroup.Generators G)).left
      (ActionCategory.back
        (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit b)) =
    f (a := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit a)
      (b := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit b)
      (Subtype.mk (p := fun (e : IsFreeGroup.Generators G) ↦
        HSMul.hSMul (β := A) (IsFreeGroup.of e)
            (ActionCategory.back (M := G)
              (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit
                a)) =
          ActionCategory.back
            (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit b))
        e h)

Tactic:
cases inv_smul_eq_iff.mpr h.symm

Premises used: Iff.mpr, inv_smul_eq_iff, Eq.symm