-- Lean 4 proof step from Mathlib.CategoryTheory.IsomorphismClasses (goal)
Goal:
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))
h :
  ∀ (a b : (↑C : Type u)) (p : (isIsomorphicSetoid (↑C : Type u) : (↑C : Type u) → (↑C : Type u) → Prop) a b),
    Eq (α :=
      Eq (α := Quotient (α := (↑E : Type u)) (isIsomorphicSetoid.{v, u} (↑E : Type u)))
        (TypeCat.Fun.toFun (X := Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
                (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) (f ≫ g).toFunctor.obj ⋯))
          (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) b))
        (TypeCat.Fun.toFun (X := Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := Quotient (α := (↑D : Type u)) (isIsomorphicSetoid.{v, u} (↑D : Type u)))
              (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
                  (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) f.toFunctor.obj ⋯)
              (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) (rb :=
                  (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) g.toFunctor.obj ⋯)))
          (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) b)))
      ⋯ ⋯
⊢ Eq (α := Quotient (α := (↑E : Type u)) (isIsomorphicSetoid.{v, u} (↑E : Type u)))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
            (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) (f ≫ g).toFunctor.obj ⋯))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := Quotient (α := (↑D : Type u)) (isIsomorphicSetoid.{v, u} (↑D : Type u)))
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) f.toFunctor.obj ⋯)
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) g.toFunctor.obj ⋯)))
      x)
have h₁ : ∀ (a : (↑C : Type u)),
  Eq (α := Quotient (α := (↑E : Type u)) (isIsomorphicSetoid.{v, u} (↑E : Type u)))
    (TypeCat.Fun.toFun (X := Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
            (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) (f ≫ g).toFunctor.obj sorry))
      (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) a))
    (TypeCat.Fun.toFun (X := Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := Quotient (α := (↑D : Type u)) (isIsomorphicSetoid.{v, u} (↑D : Type u)))
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) f.toFunctor.obj sorry)
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) g.toFunctor.obj sorry)))
      (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) a))
Tactic: apply @Quot.recOn _ _ _ x