-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
ι : Type v
α : ι → TopCat
i : ι
x : (↑(α i) : Type (max u v))
rw :
  Eq (α := (↑(∐ α) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
            (sigmaIsoSigma.{v, u} α).inv :
          (a : (↑(of ((i : ι) × (↑(α i) : Type (max u v)))) : Type (max v u))) → (↑(∐ α) : Type (max v u)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC :=
              carrier) (sigmaIsoSigma.{v, u} α).hom :
            (a : (↑(∐ α) : Type (max v u))) → (↑(of ((i : ι) × (↑(α i) : Type (max u v)))) : Type (max v u)))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                carrier) (Y := ∐ α) (Sigma.ι α i) :
              (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
            x)) :
      (↑(∐ α) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (Y := ∐ α) (Sigma.ι α i) :
          (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
        x :
      (↑(∐ α) : Type (max u v)))
rw₁ :
  Eq (α := (↑(∐ α) : Type (max v u)))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
            carrier
            (fun (X Y : TopCat) ↦
              (ContinuousMap.instFunLike :
                FunLike C((↑X : Type (max u v)), (↑Y : Type (max u v))) (↑X : Type (max u v)) (↑Y : Type (max u v))))
            _ _ _ ((sigmaIsoSigma.{v, u} α).hom ≫ (sigmaIsoSigma.{v, u} α).inv) :
          (a : (↑(∐ α) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (Y := ∐ α) (Sigma.ι α i) :
            (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
          x) :
      (↑(∐ α) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (Y := ∐ α) (Sigma.ι α i) :
          (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
        x :
      (↑(∐ α) : Type (max u v)))
rw₂ :
  Eq (α := (↑(∐ α) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (Sigma.ι α i ≫ (sigmaIsoSigma.{v, u} α).hom ≫ (sigmaIsoSigma.{v, u} α).inv) :
          (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
        x :
      (↑(∐ α) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (Y := ∐ α) (Sigma.ι α i) :
          (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
        x :
      (↑(∐ α) : Type (max u v)))
rw₃ :
  Eq (α := (↑(∐ α) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (Sigma.ι α i ≫ 𝟙 (∐ α)) :
          (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
        x :
      (↑(∐ α) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (Y := ∐ α) (Sigma.ι α i) :
          (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
        x :
      (↑(∐ α) : Type (max u v)))
rw₄ rw₅ :
  Eq (α := (↑(∐ α) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (Y := ∐ α) (Sigma.ι α i) :
          (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
        x :
      (↑(∐ α) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (Y := ∐ α) (Sigma.ι α i) :
          (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
        x :
      (↑(∐ α) : Type (max u v)))
⊢ Eq (α := (↑(∐ α) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
            (sigmaIsoSigma.{v, u} α).inv :
          (a : (↑(of ((i : ι) × (↑(α i) : Type (max u v)))) : Type (max v u))) → (↑(∐ α) : Type (max v u)))
        (Sigma.mk (β := fun (i : ι) ↦ (↑(α i) : Type (max u v))) i x) :
      (↑(∐ α) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (Y := ∐ α) (Sigma.ι α i) :
          (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
        x :
      (↑(∐ α) : Type (max u v)))

Tactic:
rw [← sigmaIsoSigma_hom_ι_apply, ← comp_app, ← comp_app, Iso.hom_inv_id,
    Category.comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, TopCat.comp_app, TopCat.sigmaIsoSigma_hom_ι_apply