-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Eq (α := Set (↑(↑(D.U j) : TopCat) : Type v))
    (Set.image (α := (↑(D.toTopGlueData.V (i, j)) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.toTopGlueData.t i j ≫ D.toTopGlueData.f j i)) :
        (a : (↑(D.toTopGlueData.V (i, j)) : Type v)) → (↑(D.toTopGlueData.U j) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.toTopGlueData.f i j)) :
          (a : (↑(D.toTopGlueData.V (i, j)) : Type v)) → (↑(D.toTopGlueData.U i) : Type v)) ⁻¹'
        (↑U : Set (↑(↑(D.U i) : TopCat) : Type v))))
    (Set.image (α := (↑(↑(D.V (j, i)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.f j i).base) :
        (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.U j) : TopCat) : Type v))
      (Set.preimage (β := (↑(↑(D.V (i, j)) : TopCat) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t j i).base) :
          (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : 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)) ⁻¹'
          (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)))))
have h : Eq (α := Set (↑(↑(D.U j) : TopCat) : Type v))
  (Set.image (α := (↑(↑(D.V (i, j)) : TopCat) : Type v))
    (Function.comp (β := (↑(↑(D.V (j, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.f j i).base) : (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.U j) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t i j).base) :
        (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.V (j, 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)) ⁻¹'
      (↑U : Set (↑(↑(D.U i) : TopCat) : Type v))))
  (Set.image (α := (↑(↑(D.V (j, i)) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.f j i).base) :
      (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.U j) : TopCat) : Type v))
    (Set.preimage (β := (↑(↑(D.V (i, j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t j i).base) :
        (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : 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)) ⁻¹'
        (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)))))
Tactic: dsimp