J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(α i)
⊢ (forget TopCat).map ((sigmaIsoSigma α).hom ≫ (sigmaIsoSigma α).inv) ((forget TopCat).map (Sigma.ι α i) x) =
    (forget TopCat).map (Sigma.ι α i) x
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(α i)
⊢ (forget TopCat).map (sigmaIsoSigma α).inv { fst := i, snd := x } = (forget TopCat).map (Sigma.ι α i) x
rw [← sigmaIsoSigma_hom_ι_apply, ← comp_app]
no goals
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(α i)
⊢ (forget TopCat).map ((sigmaIsoSigma α).hom ≫ (sigmaIsoSigma α).inv) ((forget TopCat).map (Sigma.ι α i) x) =
    (forget TopCat).map (Sigma.ι α i) x
simp