-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A B C : Rep.{w, u, v} k G
X Y Z : Rep.{u_1, u, v} k G
x : X ⟶ Y
x_1 : Y ⟶ Z
hf :
  ∀ (x_2 : (↑(of (A.ρ.linHom X.ρ)) : Type (max w u_1))) (x_3 : (↑A : Type w)),
    Eq.{u_1 + 1} (α := (↑Z : Type u_1))
      ((((Representation.IntertwiningMap.toLinearMap
                    (Hom.hom
                      (ofHom
                        {
                          toLinearMap :=
                            (LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Z : Type u_1) :
                                (a : (↑X : Type u_1) →ₗ[k] (↑Z : Type u_1)) →
                                  ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Z : Type u_1))
                              (Hom.hom (x ≫ x_1)).toLinearMap,
                          isIntertwining' := ⋯ : (A.ρ.linHom X.ρ).IntertwiningMap (A.ρ.linHom Z.ρ) })) :
                  (a : (↑(of (A.ρ.linHom X.ρ)) : Type (max w u_1))) → (↑(of (A.ρ.linHom Z.ρ)) : Type (max w u_1)))
                x_2 :
              (↑(of (A.ρ.linHom Z.ρ)) : Type (max w u_1))) :
            (a : (↑A : Type w)) → (↑Z : Type u_1))
          x_3 :
        (↑Z : Type u_1))
      ((((Representation.IntertwiningMap.toLinearMap
                    (Hom.hom
                      (CategoryStruct.comp (Y := of (A.ρ.linHom Y.ρ))
                        (ofHom
                          {
                            toLinearMap :=
                              (LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Y : Type u_1) :
                                  (a : (↑X : Type u_1) →ₗ[k] (↑Y : Type u_1)) →
                                    ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
                                (Hom.hom x).toLinearMap,
                            isIntertwining' := ⋯ : (A.ρ.linHom X.ρ).IntertwiningMap (A.ρ.linHom Y.ρ) })
                        (ofHom
                          {
                            toLinearMap :=
                              (LinearMap.llcomp k (↑A : Type w) (↑Y : Type u_1) (↑Z : Type u_1) :
                                  (a : (↑Y : Type u_1) →ₗ[k] (↑Z : Type u_1)) →
                                    ((↑A : Type w) →ₗ[k] (↑Y : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Z : Type u_1))
                                (Hom.hom x_1).toLinearMap,
                            isIntertwining' := ⋯ : (A.ρ.linHom Y.ρ).IntertwiningMap (A.ρ.linHom Z.ρ) }))) :
                  (a : (↑(of (A.ρ.linHom X.ρ)) : Type (max w u_1))) → (↑(of (A.ρ.linHom Z.ρ)) : Type (max w u_1)))
                x_2 :
              (↑(of (A.ρ.linHom Z.ρ)) : Type (max w u_1))) :
            (a : (↑A : Type w)) → (↑Z : Type u_1))
          x_3 :
        (↑Z : Type u_1))
⊢ Eq (α := of (A.ρ.linHom X.ρ) ⟶ of (A.ρ.linHom Z.ρ))
    (ofHom
      {
        toLinearMap :=
          (LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Z : Type u_1) :
              (a : (↑X : Type u_1) →ₗ[k] (↑Z : Type u_1)) →
                ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Z : Type u_1))
            (Hom.hom (x ≫ x_1)).toLinearMap,
        isIntertwining' := ⋯ })
    (CategoryStruct.comp (Y := of (A.ρ.linHom Y.ρ))
      (ofHom
        {
          toLinearMap :=
            (LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Y : Type u_1) :
                (a : (↑X : Type u_1) →ₗ[k] (↑Y : Type u_1)) →
                  ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
              (Hom.hom x).toLinearMap,
          isIntertwining' := ⋯ })
      (ofHom
        {
          toLinearMap :=
            (LinearMap.llcomp k (↑A : Type w) (↑Y : Type u_1) (↑Z : Type u_1) :
                (a : (↑Y : Type u_1) →ₗ[k] (↑Z : Type u_1)) →
                  ((↑A : Type w) →ₗ[k] (↑Y : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Z : Type u_1))
              (Hom.hom x_1).toLinearMap,
          isIntertwining' := ⋯ }))

Tactic:
ext