-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
X : Type u'
inst_1 : TopologicalSpace X
f : (↑c.pt : Type u) → X
mp :
  (∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)) →
    ∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)
mpr :
  (∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)) →
    ∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)
mp₁ mp₂ mp₃ :
  (∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)) →
    ∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)
mpr₁ mpr₂ mpr₃ :
  (∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)) →
    ∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)
mp₄ mp₅ mp₆ :
  (∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)) →
    ∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)
mpr₄ mpr₅ mpr₆ :
  (∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)) →
    ∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)
mp₇ mp₈ mp₉ :
  (∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)) →
    ∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)
mpr₇ mpr₈ mpr₉ :
  (∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)) →
    ∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)
mp₁₀ mp₁₁ :
  (∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)) →
    ∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)
mpr₁₀ mpr₁₁ :
  (∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)) →
    ∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)
⊢ (∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)) ↔
    ∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)

Tactic:
tauto