J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Embedding ((forget TopCat).map f)
hg : Embedding ((forget TopCat).map g)
this : Mono f
⊢ Function.Injective ((forget TopCat).map (prod.map f g))
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Embedding ((forget TopCat).map f)
hg : Embedding ((forget TopCat).map g)
⊢ Function.Injective ((forget TopCat).map (prod.map f g))
haveI := (TopCat.mono_iff_injective _).mpr hf.inj
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Embedding ((forget TopCat).map f)
hg : Embedding ((forget TopCat).map g)
this✝ : Mono f
this : Mono g
⊢ Function.Injective ((forget TopCat).map (prod.map f g))
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Embedding ((forget TopCat).map f)
hg : Embedding ((forget TopCat).map g)
this : Mono f
⊢ Function.Injective ((forget TopCat).map (prod.map f g))
haveI := (TopCat.mono_iff_injective _).mpr hg.inj
no goals
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Embedding ((forget TopCat).map f)
hg : Embedding ((forget TopCat).map g)
this✝ : Mono f
this : Mono g
⊢ Function.Injective ((forget TopCat).map (prod.map f g))
exact (TopCat.mono_iff_injective _).mp inferInstance