-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [← sigmaIsoSigma_hom_ι_apply, ← comp_app, ← comp_app, Iso.hom_inv_id,
    Category.comp_id]