J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(∏ α)
this : (piIsoPi α).inv ≫ Pi.π α i = piπ α i
⊢ (forget TopCat).map (piIsoPi α).hom x i = (forget TopCat).map (Pi.π α i) x
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(∏ α)
⊢ (forget TopCat).map (piIsoPi α).hom x i = (forget TopCat).map (Pi.π α i) x
have := piIsoPi_inv_π α i
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(∏ α)
this : Pi.π α i = (piIsoPi α).hom ≫ piπ α i
⊢ (forget TopCat).map (piIsoPi α).hom x i = (forget TopCat).map (Pi.π α i) x
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(∏ α)
this : (piIsoPi α).inv ≫ Pi.π α i = piπ α i
⊢ (forget TopCat).map (piIsoPi α).hom x i = (forget TopCat).map (Pi.π α i) x
rw [Iso.inv_comp_eq] at this
no goals
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(∏ α)
this : Pi.π α i = (piIsoPi α).hom ≫ piπ α i
⊢ (forget TopCat).map (piIsoPi α).hom x i = (forget TopCat).map (Pi.π α i) x
exact ConcreteCategory.congr_hom this x