J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ((forget TopCat).map i₁)
H₂ : Embedding ((forget TopCat).map i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding
    ((forget TopCat).map (prod.lift pullback.fst pullback.snd) ∘
      (forget TopCat).map (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ((forget TopCat).map i₁)
H₂ : Embedding ((forget TopCat).map i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding ((forget TopCat).map (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
refine'
  embedding_of_embedding_compose (ContinuousMap.continuous_toFun _)
    (show Continuous (prod.lift pullback.fst pullback.snd : pullback g₁ g₂ ⟶ Y ⨯ Z) from
      ContinuousMap.continuous_toFun _)
    _
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ((forget TopCat).map i₁)
H₂ : Embedding ((forget TopCat).map i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding ((forget TopCat).map (prod.lift pullback.fst pullback.snd ≫ prod.map i₁ i₂))
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ((forget TopCat).map i₁)
H₂ : Embedding ((forget TopCat).map i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding
    ((forget TopCat).map (prod.lift pullback.fst pullback.snd) ∘
      (forget TopCat).map (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
suffices
  Embedding (prod.lift pullback.fst pullback.snd ≫ Limits.prod.map i₁ i₂ : pullback f₁ f₂ ⟶ _) by
  simpa [← coe_comp] using this
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ((forget TopCat).map i₁)
H₂ : Embedding ((forget TopCat).map i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding ((forget TopCat).map (prod.map i₁ i₂) ∘ (forget TopCat).map (prod.lift pullback.fst pullback.snd))
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ((forget TopCat).map i₁)
H₂ : Embedding ((forget TopCat).map i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding ((forget TopCat).map (prod.lift pullback.fst pullback.snd ≫ prod.map i₁ i₂))
rw [coe_comp]
no goals
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ((forget TopCat).map i₁)
H₂ : Embedding ((forget TopCat).map i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding ((forget TopCat).map (prod.map i₁ i₂) ∘ (forget TopCat).map (prod.lift pullback.fst pullback.snd))
refine Embedding.comp (embedding_prod_map H₁ H₂) (embedding_pullback_to_prod _ _)
no goals
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ((forget TopCat).map i₁)
H₂ : Embedding ((forget TopCat).map i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
this : Embedding ((forget TopCat).map (prod.lift pullback.fst pullback.snd ≫ prod.map i₁ i₂))
⊢ Embedding
    ((forget TopCat).map (prod.lift pullback.fst pullback.snd) ∘
      (forget TopCat).map (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
simpa [← coe_comp] using this