-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
U : Set (↑D.glued : Type u)
⊢ (∀ (j : Discrete (MultispanShape.prod D.J).R),
      IsOpen (X := (↑(Functor.obj (Discrete.functor D.diagram.right) j) : Type u))
        (Set.preimage (β := (↑(colimit (Discrete.functor D.diagram.right)) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                Functor.obj (Discrete.functor D.diagram.right) j) (Y := colimit (Discrete.functor D.diagram.right))
                (colimit.ι (Discrete.functor D.diagram.right) j)) :
            (a : (↑((Discrete.functor D.diagram.right).obj j) : Type u)) →
              (↑(colimit (Discrete.functor D.diagram.right)) : Type u))
          (Set.preimage (β :=
            (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                  D.diagram.sndSigmaMap) :
              Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := ∐ D.diagram.right) (Y :=
                  coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                    D.diagram.sndSigmaMap)
                  (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) :
              (a : (↑(∐ D.diagram.right) : Type u)) →
                (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u))
            ((⇑(homeoOfIso (Iso.symm (Multicoequalizer.isoCoequalizer D.diagram))) :
                (a : (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u)) →
                  (↑(multicoequalizer D.diagram) : Type u)) ⁻¹'
              U)))) ↔
    ∀ (i : D.J),
      IsOpen (X := (↑(D.U i) : 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)) ⁻¹'
          U)
have mp : (∀ (j : Discrete (MultispanShape.prod D.J).R),
    IsOpen (X := (↑(Functor.obj (Discrete.functor D.diagram.right) j) : Type u))
      (Set.preimage (β := (↑(colimit (Discrete.functor D.diagram.right)) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              Functor.obj (Discrete.functor D.diagram.right) j) (Y := colimit (Discrete.functor D.diagram.right))
              (colimit.ι (Discrete.functor D.diagram.right) j)) :
          (a : (↑((Discrete.functor D.diagram.right).obj j) : Type u)) →
            (↑(colimit (Discrete.functor D.diagram.right)) : Type u))
        (Set.preimage (β :=
          (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
            Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                ∐ D.diagram.right) (Y :=
                coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                  D.diagram.sndSigmaMap)
                (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) :
            (a : (↑(∐ D.diagram.right) : Type u)) →
              (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u))
          ((⇑(homeoOfIso (Iso.symm (Multicoequalizer.isoCoequalizer D.diagram))) :
              (a : (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u)) →
                (↑(multicoequalizer D.diagram) : Type u)) ⁻¹'
            U)))) →
  ∀ (i : D.J),
    IsOpen (X := (↑(D.U i) : 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)) ⁻¹'
        U)
Tactic: tauto