-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
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
⊢ 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))
have 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' := sorry })) ∘ₗ
              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' := sorry })
                    (ofHom
                      {
                        toLinearMap :=
                          ModuleCat.Hom.hom
                            (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                              (CategoryTheory.Functor.map (resFunctor S.subtype) g)),
                        isIntertwining' := sorry }))) ∘ₗ
              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))
Tactic: ext