case obj_eq
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j

C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
have obj_eq : ∀ (j : Pairwise ι), (Pairwise.diagram U ⋙ Opens.map f).obj j =
  (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case obj_eq
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j

C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
. rintro ⟨i⟩ <;> rfl
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
⊢ ∀ (X_1 Y_1 : CategoryTheory.Pairwise ι) (f_1 : X_1 ⟶ Y_1),
    HEq ((Pairwise.diagram U ⋙ Opens.map f).map f_1) ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1)
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
refine Functor.hext obj_eq ?_
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
i j : CategoryTheory.Pairwise ι
g : i ⟶ j
⊢ HEq ((Pairwise.diagram U ⋙ Opens.map f).map g) ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map g)
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
⊢ ∀ (X_1 Y_1 : CategoryTheory.Pairwise ι) (f_1 : X_1 ⟶ Y_1),
    HEq ((Pairwise.diagram U ⋙ Opens.map f).map f_1) ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1)
intro i j g
case h₂
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
i j : CategoryTheory.Pairwise ι
g : i ⟶ j
⊢ ((Pairwise.diagram U ⋙ Opens.map f).obj i ⟶ (Pairwise.diagram U ⋙ Opens.map f).obj j) =
    ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj i ⟶
      (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j)
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
i j : CategoryTheory.Pairwise ι
g : i ⟶ j
⊢ HEq ((Pairwise.diagram U ⋙ Opens.map f).map g) ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map g)
apply Subsingleton.helim
no goals
case h₂
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
i j : CategoryTheory.Pairwise ι
g : i ⟶ j
⊢ ((Pairwise.diagram U ⋙ Opens.map f).obj i ⟶ (Pairwise.diagram U ⋙ Opens.map f).obj j) =
    ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj i ⟶
      (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j)
rw [obj_eq, obj_eq]
no goals
case obj_eq
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
rintro ⟨i⟩ <;> rfl