-- Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
inst_1 : HasFiniteLimits.{v, u} C
inst_2 : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
f : X ⟶ Y
hf : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y) x = y
g : X ⟶ Y
hg : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj X) → F.obj Y) x = y
rw :
  ∀
    (hf_1 :
      Eq (α := F.obj Y) ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y) x : F.obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj X) → F.obj Y) x : F.obj Y))
    (hg : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj X) → F.obj Y) x = y),
    ∃ (W : F.Elements) (h : W ⟶ Sigma.mk (β := fun (c : C) ↦ F.obj c) X x),
      Eq (α := W ⟶ Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y)
        (h ≫
          Subtype.mk (p :=
            fun
              (f :
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c) ⟶
                  (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).fst (β := fun (c : C) ↦ F.obj c)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨Y, y⟩.fst))
                ((Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c)) =
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).snd (β := fun (c : C) ↦ F.obj c))
            f hf)
        (h ≫
          Subtype.mk (p :=
            fun
              (f :
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c) ⟶
                  (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).fst (β := fun (c : C) ↦ F.obj c)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨Y, y⟩.fst))
                ((Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c)) =
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).snd (β := fun (c : C) ↦ F.obj c))
            g hg)
⊢ ∃ (W : F.Elements) (h : W ⟶ Sigma.mk (β := fun (c : C) ↦ F.obj c) X x),
    Eq (α := W ⟶ Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y)
      (h ≫
        Subtype.mk (p :=
          fun
            (f :
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c) ⟶
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).fst (β := fun (c : C) ↦ F.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨Y, y⟩.fst))
              ((Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c)) =
            (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).snd (β := fun (c : C) ↦ F.obj c))
          f hf)
      (h ≫
        Subtype.mk (p :=
          fun
            (f :
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c) ⟶
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).fst (β := fun (c : C) ↦ F.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨Y, y⟩.fst))
              ((Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c)) =
            (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).snd (β := fun (c : C) ↦ F.obj c))
          g hg)

Tactic:
rw [← hg] at hf