-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
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
⊢ 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' := ⋯ }))
have 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' := sorry : (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' := sorry : (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' := sorry : (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))
Tactic: ext