-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.TypeValuedFlat (goal)
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
⊢ ∃ (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)
have 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)
Tactic: rw [← hg] at hf
Cleared hypotheses: hg