-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
lemma isOpen_iff_of_isColimit_cofork (c : Cofork f g) (hc : IsColimit c) (U : Set c.pt) :
    IsOpen U ↔ IsOpen (c.π ⁻¹' U)

Proof state:
case mp
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ (∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)) →
    IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

Tactic:
intro h

Result:
case mp
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : ∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)
⊢ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

Proof state:
case mpr.zero
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)
⊢ IsOpen (⇑(ConcreteCategory.hom (c.ι.app WalkingParallelPair.zero)) ⁻¹' U)

Tactic:
rw [← c.w .left]

Result:
case mpr.zero
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)
⊢ IsOpen
    (⇑(ConcreteCategory.hom ((parallelPair f g).map WalkingParallelPairHom.left ≫ c.ι.app WalkingParallelPair.one)) ⁻¹'
      U)

Proof state:
case mpr
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U) →
    ∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)

Tactic:
rintro h (_ | _)

Result:
case mpr.zero
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)
⊢ IsOpen (⇑(ConcreteCategory.hom (c.ι.app WalkingParallelPair.zero)) ⁻¹' U)

case mpr.one
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)
⊢ IsOpen (⇑(ConcreteCategory.hom (c.ι.app WalkingParallelPair.one)) ⁻¹' U)

Proof state:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ (∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)) ↔
    IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

Tactic:
constructor

Result:
case mp
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ (∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)) →
    IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

case mpr
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U) →
    ∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)

Proof state:
case mp
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : ∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)
⊢ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

Tactic:
exact h .one

Result:
no goals

Proof state:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ IsOpen U ↔ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

Tactic:
rw [isOpen_iff_of_isColimit _ hc]

Result:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ (∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)) ↔
    IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

Proof state:
case mpr.one
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)
⊢ IsOpen (⇑(ConcreteCategory.hom (c.ι.app WalkingParallelPair.one)) ⁻¹' U)

Tactic:
exact h

Result:
no goals

Proof state:
case mpr.zero
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)
⊢ IsOpen
    (⇑(ConcreteCategory.hom ((parallelPair f g).map WalkingParallelPairHom.left ≫ c.ι.app WalkingParallelPair.one)) ⁻¹'
      U)

Tactic:
exact Continuous.isOpen_preimage f.hom.continuous (c.π ⁻¹' U) h

Result:
no goals