-- 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 : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
x y : (↑(↑(D.U i) : TopCat) : Type v)
h1 : y ∈ U
h2 :
  Eq (α := (↑(↑D.glued : TopCat) : Type v))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(D.U i) : TopCat)) (Y := (↑D.glued : TopCat))
              (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i)) :
                (↑(D.U i) : TopCat) ⟶ (↑D.glued : TopCat)) :
            C((↑(↑(D.U i) : TopCat) : Type v), (↑(↑D.glued : TopCat) : Type v))) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        y :
      (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat)) (Y :=
            (↑(Limits.colimit D.diagram.multispan) : TopCat))
            (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i))) :
          (a : (↑(↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat) : Type v)) →
            (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
        x :
      (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
this :
  Eq (α := (↑(D.U i) : TopCat) ⟶ (↑D.glued : TopCat))
    (CategoryStruct.comp (Y := (D.mapGlueData (forget C)).glued)
      ((D.mapGlueData (forget C)).ι i : (D.mapGlueData (forget C)).U i ⟶ (D.mapGlueData (forget C)).glued)
      (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ (↑D.glued : TopCat)))
    (Hom.base (D.ι i))
⊢ Function.Injective (α := (↑(↑(D.U i) : TopCat) : Type v)) (β := (↑(↑D.glued : TopCat) : Type v))
    (Function.comp (β := (↑(D.mapGlueData (forget C)).glued : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (D.mapGlueData (forget C)).glued) (Y := (↑D.glued : TopCat))
              (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ (↑D.glued : TopCat)) :
            C((↑(D.mapGlueData (forget C)).glued : Type v), (↑(↑D.glued : TopCat) : Type v))) :
        (a : (↑(D.mapGlueData (forget C)).glued : Type v)) → (↑(↑D.glued : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι i)) :
        (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v)))
have h : Function.Injective (α := (↑(D.mapGlueData (forget C)).glued : Type v)) (β := (↑(↑D.glued : TopCat) : Type v))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
          (D.mapGlueData (forget C)).glued) (Y := (↑D.glued : TopCat))
          (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ (↑D.glued : TopCat)) :
        C((↑(D.mapGlueData (forget C)).glued : Type v), (↑(↑D.glued : TopCat) : Type v))) :
    (a : (↑(D.mapGlueData (forget C)).glued : Type v)) → (↑(↑D.glued : TopCat) : Type v))
Tactic: refine Function.Injective.comp ?_ (TopCat.GlueData.ι_injective D.toTopGlueData i)