-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
S : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)
eq₁ :
  Eq (α := (↑(pullback (D.f i j) (D.f i k)) : TopCat) ⟶ (↑(D.V (i, j)) : TopCat))
    (CategoryStruct.comp (Y :=
        pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k)))
        (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)))
        (pullback.fst (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k))) :
      Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶ Functor.obj (forget C) (D.V (i, j)))
    (Hom.base (pullback.fst (D.f i j) (D.f i k)))
eq₂ :
  Eq (α := (↑(pullback (D.f i j) (D.f i k)) : TopCat) ⟶ (↑(D.V (i, k)) : TopCat))
    (CategoryStruct.comp (Y :=
        pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k)))
        (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)))
        (pullback.snd (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k))) :
      Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶ Functor.obj (forget C) (D.V (i, k)))
    (Hom.base (pullback.snd (D.f i j) (D.f i k)))
rw :
  Eq (α := Set (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (Set.image (α :=
      (↑(pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
            (CategoryTheory.Functor.map (forget C) (D.f i k))) :
        Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X :=
            pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
              (CategoryTheory.Functor.map (forget C) (D.f i k)))
            (pullback.snd (CategoryTheory.Functor.map (forget C) (D.f i j))
              (CategoryTheory.Functor.map (forget C) (D.f i k)))) :
        (a : (↑(pullback ((forget C).map (D.f i j)) ((forget C).map (D.f i k))) : Type v)) →
          (↑(↑(D.V (i, k)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X :=
              pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
                (CategoryTheory.Functor.map (forget C) (D.f i k)))
              (pullback.fst (CategoryTheory.Functor.map (forget C) (D.f i j))
                (CategoryTheory.Functor.map (forget C) (D.f i k)))) :
          (a : (↑(pullback ((forget C).map (D.f i j)) ((forget C).map (D.f i k))) : Type v)) →
            (↑(↑(D.V (i, j)) : TopCat) : Type v)) ⁻¹'
        S))
    (Set.preimage (β := (↑(↑(D.U i) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.f i k).base) :
        (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.f i j).base) :
          (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ''
        S))
h :
  Function.Surjective (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) (β :=
    (↑(pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k))) :
      Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Y :=
            pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
              (CategoryTheory.Functor.map (forget C) (D.f i k)))
            (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)) :
              Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶
                pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
                  (CategoryTheory.Functor.map (forget C) (D.f i k))) :
          C((↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v),
            (↑(pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
                  (CategoryTheory.Functor.map (forget C) (D.f i k))) :
              Type v))) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
        (↑(pullback ((forget C).map (D.f i j)) ((forget C).map (D.f i k))) : Type v))
⊢ Eq (α := Set (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.fst (D.f i j) (D.f i k)))) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : TopCat) : Type v)) ⁻¹'
        S))
    (Set.preimage (β := (↑(↑(D.U i) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.f i k).base) :
        (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.f i j).base) :
          (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ''
        S))

Tactic:
rw [← eq₁, ← eq₂, TopCat.coe_comp, Set.image_comp, TopCat.coe_comp, Set.preimage_comp,
    Set.image_preimage_eq]

Premises used: Set.image_preimage_eq, Set.preimage_comp, Set.image_comp, TopCat.coe_comp