case induced
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Inducing ((forget TopCat).map f)
hg : Inducing ((forget TopCat).map g)
⊢ topologicalSpace_forget (W ⨯ Y) = induced ((forget TopCat).map (prod.map f g)) (topologicalSpace_forget (X ⨯ Z))
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Inducing ((forget TopCat).map f)
hg : Inducing ((forget TopCat).map g)
⊢ Inducing ((forget TopCat).map (prod.map f g))
constructor
case induced
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Inducing ((forget TopCat).map f)
hg : Inducing ((forget TopCat).map g)
⊢ induced ((forget TopCat).map prod.fst) W.str ⊓ induced ((forget TopCat).map prod.snd) Y.str =
    induced ((forget TopCat).map (prod.fst ≫ f)) X.str ⊓ induced ((forget TopCat).map (prod.snd ≫ g)) Z.str
case induced
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Inducing ((forget TopCat).map f)
hg : Inducing ((forget TopCat).map g)
⊢ topologicalSpace_forget (W ⨯ Y) = induced ((forget TopCat).map (prod.map f g)) (topologicalSpace_forget (X ⨯ Z))
simp only [prod_topology, induced_compose, ← coe_comp, Limits.prod.map_fst, Limits.prod.map_snd,
  induced_inf]
case induced
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Inducing ((forget TopCat).map f)
hg : Inducing ((forget TopCat).map g)
⊢ induced ((forget TopCat).map prod.fst) W.str ⊓ induced ((forget TopCat).map prod.snd) Y.str =
    induced ((forget TopCat).map f ∘ (forget TopCat).map prod.fst) X.str ⊓
      induced ((forget TopCat).map g ∘ (forget TopCat).map prod.snd) Z.str
case induced
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Inducing ((forget TopCat).map f)
hg : Inducing ((forget TopCat).map g)
⊢ induced ((forget TopCat).map prod.fst) W.str ⊓ induced ((forget TopCat).map prod.snd) Y.str =
    induced ((forget TopCat).map (prod.fst ≫ f)) X.str ⊓ induced ((forget TopCat).map (prod.snd ≫ g)) Z.str
simp only [coe_comp]
no goals
case induced
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Inducing ((forget TopCat).map f)
hg : Inducing ((forget TopCat).map g)
⊢ induced ((forget TopCat).map prod.fst) W.str ⊓ induced ((forget TopCat).map prod.snd) Y.str =
    induced ((forget TopCat).map f ∘ (forget TopCat).map prod.fst) X.str ⊓
      induced ((forget TopCat).map g ∘ (forget TopCat).map prod.snd) Z.str
rw [← @induced_compose _ _ _ _ _ f, ← @induced_compose _ _ _ _ _ g, ← hf.induced, ← hg.induced]