-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x : (↑(I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max (max s w) w'))
i : J.R
a :
  (hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.fst i)) :
        (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.fst i)))) →
          (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
      ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.fst i))) =
    (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.right i)
b :
  (hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd i)) :
        (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd i)))) →
          (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
      ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.snd i))) =
    (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.right i)
a₁ :
  Eq (α := (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))
    ((hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.fst i)) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.fst i)))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
        ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.fst i))) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))
    ((hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd i)) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd i)))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
        ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.snd i))) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))
⊢ (hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd i)) :
        (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd i)))) →
          (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
      ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.snd i))) =
    (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.right i)

Tactic:
rw [← b] at a