-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i_1 j_1 : D.J
x : (↑(D.U i_1) : Type u)
y_1 : (↑(D.U j_1) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i_1)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U i_1) : Type u)) → (↑D.glued : Type u))
        x :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right j_1)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U j_1) : Type u)) → (↑D.glued : Type u))
        y_1 :
      (↑D.glued : Type u))
i j : D.J
y : (↑(D.diagram.left (i, j)) : Type u)
⊢ D.Rel
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          D.diagram.left (i, j)) (Y := of ((i : D.J) × (↑(D.U i) : Type u)))
          (NatTrans.app
              (Cocone.ι
                (Cofan.mk
                  (Cocone.pt (F := Discrete.functor D.diagram.right)
                    (colimit.cocone (Discrete.functor D.diagram.right)))
                  fun (i : (MultispanShape.prod D.J).L) ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right)) ((MultispanShape.prod D.J).fst i)))
              { as := (i, j) } ≫
            (sigmaIsoSigma D.U).hom) :
        (a : (↑(D.diagram.left (i, j)) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
      y)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          D.diagram.left (i, j)) (Y := of ((i : D.J) × (↑(D.U i) : Type u)))
          (NatTrans.app
              (Cocone.ι
                (Cofan.mk
                  (Cocone.pt (F := Discrete.functor D.diagram.right)
                    (colimit.cocone (Discrete.functor D.diagram.right)))
                  fun (i : (MultispanShape.prod D.J).L) ↦
                  D.diagram.snd i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right)) ((MultispanShape.prod D.J).snd i)))
              { as := (i, j) } ≫
            (sigmaIsoSigma D.U).hom) :
        (a : (↑(D.diagram.left (i, j)) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
      y)
have mp : D.Rel
  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
    ((MultispanShape.prod D.J).fst { as := (i, j) : Discrete (MultispanShape.prod D.J).L }.as)
    ((Hom.hom' (D.diagram.fst { as := (i, j) : Discrete (MultispanShape.prod D.J).L }.as) :
        (a : (↑(D.diagram.left { as := (i, j) }.as) : Type u)) →
          (↑(D.diagram.right ((MultispanShape.prod D.J).fst { as := (i, j) }.as)) : Type u))
      y))
  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) ((MultispanShape.prod D.J).snd { as := (i, j) }.as)
    ((Hom.hom' (D.diagram.snd { as := (i, j) }.as) :
        (a : (↑(D.diagram.left { as := (i, j) }.as) : Type u)) →
          (↑(D.diagram.right ((MultispanShape.prod D.J).snd { as := (i, j) }.as)) : Type u))
      y))
Tactic: erw [sigmaIsoSigma_hom_ι_apply, sigmaIsoSigma_hom_ι_apply]