-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.Forget (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v_1, u_1, u_2} C FC (CC := CC)
D : Type u_3
inst_3 : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst_4 : (X Y : D) → FunLike.{u_4 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{w, v_2, u_3, u_4} D FD (CC := CD)
inst_6 : HasForget₂.{w, v_1, u_1, u_2, v_2, u_3, u_4} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x :
  ToType.{w, v_2, u_3, u_4} (FC := FD) (CC := CD)
    (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X)
rw :
  Eq (α := CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f ≫
              Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) g) :
          (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Z))
        x :
      CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) g) :
          (a : CD ((forget₂ C D).obj Y)) → CD ((forget₂ C D).obj Z))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
                (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f) :
              (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Y))
            x :
          CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Y)) :
      CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
⊢ Eq (α := CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) (f ≫ g)) :
          (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Z))
        x :
      CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) g) :
          (a : CD ((forget₂ C D).obj Y)) → CD ((forget₂ C D).obj Z))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
                (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f) :
              (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Y))
            x :
          CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Y)) :
      CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
have rw₁ : Eq (α := CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
  ((ConcreteCategory.hom (FC := FD) (CC := CD)
          (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) g) :
        (a : CD ((forget₂ C D).obj Y)) → CD ((forget₂ C D).obj Z))
      ((ConcreteCategory.hom (FC := FD) (CC := CD)
              (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f) :
            (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Y))
          x :
        CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Y)) :
    CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
  ((ConcreteCategory.hom (FC := FD) (CC := CD)
          (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) g) :
        (a : CD ((forget₂ C D).obj Y)) → CD ((forget₂ C D).obj Z))
      ((ConcreteCategory.hom (FC := FD) (CC := CD)
              (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f) :
            (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Y))
          x :
        CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Y)) :
    CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
Tactic: rw [Functor.map_comp, CategoryTheory.comp_apply]