-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
U : Set (↑D.glued : Type u)
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)
mpr :
  (∀ (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)) →
    ∀ (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)))
mp₁ mp₂ 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)
mpr₁ mpr₂ mpr₃ :
  (∀ (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)) →
    ∀ (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)))
mp₄ mp₅ 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)
mpr₄ mpr₅ mpr₆ :
  (∀ (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)) →
    ∀ (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)))
mp₇ 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)
mpr₇ mpr₈ :
  (∀ (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)) →
    ∀ (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)))
⊢ (∀ (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