-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u
G_1 : Type v
inst : CommRing k_1
inst_1 : Monoid G_1
A B : Rep.{w, u, v} k_1 G_1
k : Type u
G : Type v
inst_2 : CommRing k
inst_3 : Group G
S : Subgroup G
inst_4 : S.Normal
X Y Z : Rep.{w, u, v} k G
f : X ⟶ Y
g : Y ⟶ Z
hf :
  ∀ (x : (↑X : Type w)),
    Eq (α := (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w))
      (((IntertwiningMap.toLinearMap.{u, v, w, w} (G := G ⧸ S) (ρ := ρ (of ((X.toCoinvariants S).ρ.ofQuotient S))) (σ :=
                  ρ (of ((Z.toCoinvariants S).ρ.ofQuotient S)))
                  (Hom.hom
                    (ofHom
                      {
                        toLinearMap :=
                          ModuleCat.Hom.hom
                            (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                              (CategoryTheory.Functor.map (resFunctor S.subtype) (f ≫ g))),
                        isIntertwining' := ⋯ })) ∘ₗ
                Coinvariants.mk (MonoidHom.comp X.ρ S.subtype) :
              (↑X : Type w) →ₗ[k] (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w)) :
            (a : (↑X : Type w)) → (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w))
          x :
        (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w))
      (((IntertwiningMap.toLinearMap.{u, v, w, w} (G := G ⧸ S) (ρ := ρ (of ((X.toCoinvariants S).ρ.ofQuotient S))) (σ :=
                  ρ (of ((Z.toCoinvariants S).ρ.ofQuotient S)))
                  (Hom.hom
                    (CategoryStruct.comp (Y := Y.quotientToCoinvariants S)
                      (ofHom
                        {
                          toLinearMap :=
                            ModuleCat.Hom.hom
                              (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                                (CategoryTheory.Functor.map (resFunctor S.subtype) f)),
                          isIntertwining' := ⋯ })
                      (ofHom
                        {
                          toLinearMap :=
                            ModuleCat.Hom.hom
                              (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                                (CategoryTheory.Functor.map (resFunctor S.subtype) g)),
                          isIntertwining' := ⋯ }))) ∘ₗ
                Coinvariants.mk (MonoidHom.comp X.ρ S.subtype) :
              (↑X : Type w) →ₗ[k] (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w)) :
            (a : (↑X : Type w)) → (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w))
          x :
        (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w))
⊢ Eq (α := Quiver.Hom (V := Rep.{w, u, v} k (G ⧸ S)) (X.quotientToCoinvariants S) (Z.quotientToCoinvariants S))
    (ofHom
        {
          toLinearMap :=
            ModuleCat.Hom.hom
              (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                (CategoryTheory.Functor.map (resFunctor S.subtype) (f ≫ g))),
          isIntertwining' := ⋯ } :
      Quiver.Hom (V := Rep.{w, u, v} k (G ⧸ S)) (of ((X.toCoinvariants S).ρ.ofQuotient S))
        (of ((Z.toCoinvariants S).ρ.ofQuotient S)))
    (CategoryStruct.comp (Y := Y.quotientToCoinvariants S)
        (ofHom
          {
            toLinearMap :=
              ModuleCat.Hom.hom
                (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                  (CategoryTheory.Functor.map (resFunctor S.subtype) f)),
            isIntertwining' := ⋯ })
        (ofHom
          {
            toLinearMap :=
              ModuleCat.Hom.hom
                (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                  (CategoryTheory.Functor.map (resFunctor S.subtype) g)),
            isIntertwining' := ⋯ }) :
      Quiver.Hom (V := Rep.{w, u, v} k (G ⧸ S)) (X.quotientToCoinvariants S) (Z.quotientToCoinvariants S))

Tactic:
ext