case h
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
⊢ x ∈ Set.range ((forget TopCat).map (prod.map f g)) ↔
    x ∈
      (forget TopCat).map prod.fst ⁻¹' Set.range ((forget TopCat).map f) ∩
        (forget TopCat).map prod.snd ⁻¹' Set.range ((forget TopCat).map g)
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
⊢ Set.range ((forget TopCat).map (prod.map f g)) =
    (forget TopCat).map prod.fst ⁻¹' Set.range ((forget TopCat).map f) ∩
      (forget TopCat).map prod.snd ⁻¹' Set.range ((forget TopCat).map g)
ext x
case h.mp
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
⊢ x ∈ Set.range ((forget TopCat).map (prod.map f g)) →
    x ∈
      (forget TopCat).map prod.fst ⁻¹' Set.range ((forget TopCat).map f) ∩
        (forget TopCat).map prod.snd ⁻¹' Set.range ((forget TopCat).map g)

case h.mpr
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
⊢ x ∈
      (forget TopCat).map prod.fst ⁻¹' Set.range ((forget TopCat).map f) ∩
        (forget TopCat).map prod.snd ⁻¹' Set.range ((forget TopCat).map g) →
    x ∈ Set.range ((forget TopCat).map (prod.map f g))
case h
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
⊢ x ∈ Set.range ((forget TopCat).map (prod.map f g)) ↔
    x ∈
      (forget TopCat).map prod.fst ⁻¹' Set.range ((forget TopCat).map f) ∩
        (forget TopCat).map prod.snd ⁻¹' Set.range ((forget TopCat).map g)
constructor
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
y : (forget TopCat).obj (W ⨯ X)
⊢ (forget TopCat).map (prod.map f g) y ∈
    (forget TopCat).map prod.fst ⁻¹' Set.range ((forget TopCat).map f) ∩
      (forget TopCat).map prod.snd ⁻¹' Set.range ((forget TopCat).map g)
case h.mp
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
⊢ x ∈ Set.range ((forget TopCat).map (prod.map f g)) →
    x ∈
      (forget TopCat).map prod.fst ⁻¹' Set.range ((forget TopCat).map f) ∩
        (forget TopCat).map prod.snd ⁻¹' Set.range ((forget TopCat).map g)
rintro ⟨y, rfl⟩
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
y : (forget TopCat).obj (W ⨯ X)
⊢ (∃ y_1, (forget TopCat).map f y_1 = (forget TopCat).map (prod.map f g ≫ prod.fst) y) ∧
    ∃ y_1, (forget TopCat).map g y_1 = (forget TopCat).map (prod.map f g ≫ prod.snd) y
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
y : (forget TopCat).obj (W ⨯ X)
⊢ (forget TopCat).map (prod.map f g) y ∈
    (forget TopCat).map prod.fst ⁻¹' Set.range ((forget TopCat).map f) ∩
      (forget TopCat).map prod.snd ⁻¹' Set.range ((forget TopCat).map g)
simp only [Set.mem_preimage, Set.mem_range, Set.mem_inter_iff, ← comp_apply]
no goals
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
y : (forget TopCat).obj (W ⨯ X)
⊢ (∃ y_1, (forget TopCat).map f y_1 = (forget TopCat).map (prod.map f g ≫ prod.fst) y) ∧
    ∃ y_1, (forget TopCat).map g y_1 = (forget TopCat).map (prod.map f g ≫ prod.snd) y
simp only [Limits.prod.map_fst, Limits.prod.map_snd, exists_apply_eq_apply, comp_apply,
  and_self_iff]
case h.mpr.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ x ∈ Set.range ((forget TopCat).map (prod.map f g))
case h.mpr
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
⊢ x ∈
      (forget TopCat).map prod.fst ⁻¹' Set.range ((forget TopCat).map f) ∩
        (forget TopCat).map prod.snd ⁻¹' Set.range ((forget TopCat).map g) →
    x ∈ Set.range ((forget TopCat).map (prod.map f g))
rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩
case h.mpr.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map (prod.map f g) ((forget TopCat).map (prodIsoProd W X).inv (x₁, x₂)) = x
case h.mpr.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ x ∈ Set.range ((forget TopCat).map (prod.map f g))
use (prodIsoProd W X).inv (x₁, x₂)
case h.mpr.intro.intro.intro.a
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ ∀ (j : Discrete WalkingPair),
    (forget TopCat).map (limit.π (pair Y Z) j)
        ((forget TopCat).map (prod.map f g) ((forget TopCat).map (prodIsoProd W X).inv (x₁, x₂))) =
      (forget TopCat).map (limit.π (pair Y Z) j) x
case h.mpr.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map (prod.map f g) ((forget TopCat).map (prodIsoProd W X).inv (x₁, x₂)) = x
apply Concrete.limit_ext
case h.mpr.intro.intro.intro.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left })
      ((forget TopCat).map (prod.map f g) ((forget TopCat).map (prodIsoProd W X).inv (x₁, x₂))) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left }) x

case h.mpr.intro.intro.intro.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right })
      ((forget TopCat).map (prod.map f g) ((forget TopCat).map (prodIsoProd W X).inv (x₁, x₂))) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right }) x
case h.mpr.intro.intro.intro.a
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ ∀ (j : Discrete WalkingPair),
    (forget TopCat).map (limit.π (pair Y Z) j)
        ((forget TopCat).map (prod.map f g) ((forget TopCat).map (prodIsoProd W X).inv (x₁, x₂))) =
      (forget TopCat).map (limit.π (pair Y Z) j) x
rintro ⟨⟨⟩⟩
case h.mpr.intro.intro.intro.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map ((prodIsoProd W X).inv ≫ prod.map f g ≫ limit.π (pair Y Z) { as := WalkingPair.left }) (x₁, x₂) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left }) x
case h.mpr.intro.intro.intro.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left })
      ((forget TopCat).map (prod.map f g) ((forget TopCat).map (prodIsoProd W X).inv (x₁, x₂))) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left }) x
simp only [← comp_apply, Category.assoc]
case h.mpr.intro.intro.intro.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map ((prodIsoProd W X).inv ≫ prod.fst ≫ f) (x₁, x₂) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left }) x
case h.mpr.intro.intro.intro.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map ((prodIsoProd W X).inv ≫ prod.map f g ≫ limit.π (pair Y Z) { as := WalkingPair.left }) (x₁, x₂) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left }) x
erw [Limits.prod.map_fst]
case h.mpr.intro.intro.intro.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map f ((forget TopCat).map prodFst (x₁, x₂)) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left }) x
case h.mpr.intro.intro.intro.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map ((prodIsoProd W X).inv ≫ prod.fst ≫ f) (x₁, x₂) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left }) x
rw [TopCat.prodIsoProd_inv_fst_assoc,TopCat.comp_app]
case h.mpr.intro.intro.intro.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
this : (forget TopCat).map prodFst (x₁, x₂) = x₁
⊢ (forget TopCat).map f ((forget TopCat).map prodFst (x₁, x₂)) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left }) x
case h.mpr.intro.intro.intro.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map f ((forget TopCat).map prodFst (x₁, x₂)) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left }) x
have : (forget TopCat).map prodFst (x₁, x₂) = x₁ := rfl
no goals
case h.mpr.intro.intro.intro.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
this : (forget TopCat).map prodFst (x₁, x₂) = x₁
⊢ (forget TopCat).map f ((forget TopCat).map prodFst (x₁, x₂)) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.left }) x
rw [this, hx₁]
case h.mpr.intro.intro.intro.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map ((prodIsoProd W X).inv ≫ prod.map f g ≫ limit.π (pair Y Z) { as := WalkingPair.right }) (x₁, x₂) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right }) x
case h.mpr.intro.intro.intro.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right })
      ((forget TopCat).map (prod.map f g) ((forget TopCat).map (prodIsoProd W X).inv (x₁, x₂))) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right }) x
simp only [← comp_apply, Category.assoc]
case h.mpr.intro.intro.intro.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map ((prodIsoProd W X).inv ≫ prod.snd ≫ g) (x₁, x₂) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right }) x
case h.mpr.intro.intro.intro.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map ((prodIsoProd W X).inv ≫ prod.map f g ≫ limit.π (pair Y Z) { as := WalkingPair.right }) (x₁, x₂) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right }) x
erw [Limits.prod.map_snd]
case h.mpr.intro.intro.intro.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map g ((forget TopCat).map prodSnd (x₁, x₂)) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right }) x
case h.mpr.intro.intro.intro.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map ((prodIsoProd W X).inv ≫ prod.snd ≫ g) (x₁, x₂) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right }) x
rw [TopCat.prodIsoProd_inv_snd_assoc,TopCat.comp_app]
case h.mpr.intro.intro.intro.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
this : (forget TopCat).map prodSnd (x₁, x₂) = x₂
⊢ (forget TopCat).map g ((forget TopCat).map prodSnd (x₁, x₂)) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right }) x
case h.mpr.intro.intro.intro.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
⊢ (forget TopCat).map g ((forget TopCat).map prodSnd (x₁, x₂)) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right }) x
have : (forget TopCat).map prodSnd (x₁, x₂) = x₂ := rfl
no goals
case h.mpr.intro.intro.intro.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : (forget TopCat).map f x₁ = (forget TopCat).map prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : (forget TopCat).map g x₂ = (forget TopCat).map prod.snd x
this : (forget TopCat).map prodSnd (x₁, x₂) = x₂
⊢ (forget TopCat).map g ((forget TopCat).map prodSnd (x₁, x₂)) =
    (forget TopCat).map (limit.π (pair Y Z) { as := WalkingPair.right }) x
rw [this, hx₂]