-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
x_1 : (↑(D.U i) : Type u)
y : (↑(D.U j) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        x_1 :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right j)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
x : (↑(∐ D.diagram.left) : Type u)
⊢ InvImage (α := (↑(∐ D.U) : Type u)) D.Rel
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (sigmaIsoSigma D.U).hom) :
        (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) :
      (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap :
          (a : (↑(∐ D.diagram.left) : Type u)) → (↑(∐ D.diagram.right) : Type u))
        x :
      (↑(∐ D.diagram.right) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.sndSigmaMap :
          (a : (↑(∐ D.diagram.left) : Type u)) → (↑(∐ D.diagram.right) : Type u))
        x :
      (↑(∐ D.diagram.right) : Type u))
have mp : ∀ (i j : D.J) (y : (↑(D.diagram.left (i, j)) : Type u)),
  InvImage (α := (↑(∐ D.U) : Type u)) D.Rel
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (sigmaIsoSigma D.U).hom) :
        (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) :
      (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap :
          (a : (↑(∐ D.diagram.left) : Type u)) → (↑(∐ D.diagram.right) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (sigmaIsoSigma D.diagram.left).inv :
              (a : (↑(of ((i : (MultispanShape.prod D.J).L) × (↑(D.diagram.left i) : Type u))) : Type u)) →
                (↑(∐ D.diagram.left) : Type u))
            (Sigma.mk (β := fun (i : (MultispanShape.prod D.J).L) ↦ (↑(D.diagram.left i) : Type u)) (i, j) y) :
          (↑(∐ D.diagram.left) : Type u)) :
      (↑(∐ D.diagram.right) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.sndSigmaMap :
          (a : (↑(∐ D.diagram.left) : Type u)) → (↑(∐ D.diagram.right) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (sigmaIsoSigma D.diagram.left).inv :
              (a : (↑(of ((i : (MultispanShape.prod D.J).L) × (↑(D.diagram.left i) : Type u))) : Type u)) →
                (↑(∐ D.diagram.left) : Type u))
            (Sigma.mk (β := fun (i : (MultispanShape.prod D.J).L) ↦ (↑(D.diagram.left i) : Type u)) (i, j) y) :
          (↑(∐ D.diagram.left) : Type u)) :
      (↑(∐ D.diagram.right) : Type u))
Tactic: obtain ⟨⟨⟨i, j⟩, y⟩, rfl⟩ :=
      (ConcreteCategory.bijective_of_isIso (sigmaIsoSigma.{u, u} _).inv).2 x
Cleared hypotheses: x