J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
⊢ (∀ (j : WalkingParallelPair), IsOpen ((forget TopCat).map (colimit.ι F j) ⁻¹' U)) ↔
    IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
⊢ IsOpen U ↔ IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
rw [colimit_isOpen_iff]
case mp
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
⊢ (∀ (j : WalkingParallelPair), IsOpen ((forget TopCat).map (colimit.ι F j) ⁻¹' U)) →
    IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)

case mpr
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
⊢ IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U) →
    ∀ (j : WalkingParallelPair), IsOpen ((forget TopCat).map (colimit.ι F j) ⁻¹' U)
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
⊢ (∀ (j : WalkingParallelPair), IsOpen ((forget TopCat).map (colimit.ι F j) ⁻¹' U)) ↔
    IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
constructor
case mp
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : ∀ (j : WalkingParallelPair), IsOpen ((forget TopCat).map (colimit.ι F j) ⁻¹' U)
⊢ IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
case mp
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
⊢ (∀ (j : WalkingParallelPair), IsOpen ((forget TopCat).map (colimit.ι F j) ⁻¹' U)) →
    IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
intro H
no goals
case mp
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : ∀ (j : WalkingParallelPair), IsOpen ((forget TopCat).map (colimit.ι F j) ⁻¹' U)
⊢ IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
exact H _
case mpr
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
j : WalkingParallelPair
⊢ IsOpen ((forget TopCat).map (colimit.ι F j) ⁻¹' U)
case mpr
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
⊢ IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U) →
    ∀ (j : WalkingParallelPair), IsOpen ((forget TopCat).map (colimit.ι F j) ⁻¹' U)
intro H j
case mpr.zero
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
⊢ IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.zero) ⁻¹' U)

case mpr.one
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
⊢ IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
case mpr
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
j : WalkingParallelPair
⊢ IsOpen ((forget TopCat).map (colimit.ι F j) ⁻¹' U)
cases j
case mpr.zero
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
⊢ IsOpen ((forget TopCat).map (F.map WalkingParallelPairHom.left ≫ colimit.ι F WalkingParallelPair.one) ⁻¹' U)
case mpr.zero
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
⊢ IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.zero) ⁻¹' U)
rw [← colimit.w F WalkingParallelPairHom.left]
no goals
case mpr.zero
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
⊢ IsOpen ((forget TopCat).map (F.map WalkingParallelPairHom.left ≫ colimit.ι F WalkingParallelPair.one) ⁻¹' U)
exact (F.map WalkingParallelPairHom.left).continuous_toFun.isOpen_preimage _ H
no goals
case mpr.one
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
⊢ IsOpen ((forget TopCat).map (colimit.ι F WalkingParallelPair.one) ⁻¹' U)
exact H