-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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'))
a :
  ∀ (a : J.L),
    (↑((fun
                  (x :
                    { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
                      ∀ (i : J.R),
                        Eq.{s + 1} (α := CC (I.right i))
                          ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i))
                              (x (J.fst i)) :
                            CC (I.right i))
                          ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i))
                              (x (J.snd i)) :
                            CC (I.right i)) }) ↦
                Subtype.mk (p :=
                  fun (x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j) ↦
                  x ∈ (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections)
                  (fun (j : WalkingMulticospan J) ↦
                    match (motive :=
                      (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j) j with
                    | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
                    | WalkingMulticospan.right b =>
                      (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                        ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)))
                  ⋯)
              ((fun (x : (↑(I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max (max s w) w'))) ↦
                  (Subtype.mk (p := fun (x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i)) ↦
                      ∀ (i : J.R),
                        Eq.{s + 1} (α := CC (I.right i))
                          ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i))
                              (x (J.fst i)) :
                            CC (I.right i))
                          ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i))
                              (x (J.snd i)) :
                            CC (I.right i)))
                      (fun (x_1 : J.L) ↦
                        (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j)
                          (WalkingMulticospan.left x_1))
                      ⋯ :
                    { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
                      ∀ (i : J.R),
                        Eq.{s + 1} (α := CC (I.right i))
                          ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i))
                              (x (J.fst i)) :
                            CC (I.right i))
                          ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i))
                              (x (J.snd i)) :
                            CC (I.right i)) }))
                x)) :
          (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j)
        (WalkingMulticospan.left a) =
      (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left a)
⊢ (fun
          (x :
            { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
              ∀ (i : J.R),
                Eq.{s + 1} (α := CC (I.right i))
                  ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i)) (x (J.fst i)) :
                    CC (I.right i))
                  ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i)) (x (J.snd i)) :
                    CC (I.right i)) }) ↦
        Subtype.mk (p := fun (x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j) ↦
          x ∈ (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections)
          (fun (j : WalkingMulticospan J) ↦
            match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j) j with
            | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
            | WalkingMulticospan.right b =>
              (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)))
          ⋯)
      ((fun (x : (↑(I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max (max s w) w'))) ↦
          (Subtype.mk (p := fun (x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i)) ↦
              ∀ (i : J.R),
                Eq.{s + 1} (α := CC (I.right i))
                  ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i)) (x (J.fst i)) :
                    CC (I.right i))
                  ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i)) (x (J.snd i)) :
                    CC (I.right i)))
              (fun (x_1 : J.L) ↦
                (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left x_1))
              ⋯ :
            { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
              ∀ (i : J.R),
                Eq.{s + 1} (α := CC (I.right i))
                  ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i)) (x (J.fst i)) :
                    CC (I.right i))
                  ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i)) (x (J.snd i)) :
                    CC (I.right i)) }))
        x) =
    x
have a₁ : ∀ (b : J.R),
  (↑((fun
                (x :
                  { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
                    ∀ (i : J.R),
                      Eq.{s + 1} (α := CC (I.right i))
                        ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i))
                            (x (J.fst i)) :
                          CC (I.right i))
                        ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i))
                            (x (J.snd i)) :
                          CC (I.right i)) }) ↦
              Subtype.mk (p :=
                fun (x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j) ↦
                x ∈ (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections)
                (fun (j : WalkingMulticospan J) ↦
                  match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j)
                    j with
                  | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
                  | WalkingMulticospan.right b =>
                    (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                      ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)))
                sorry)
            ((fun (x : (↑(I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max (max s w) w'))) ↦
                (Subtype.mk (p := fun (x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i)) ↦
                    ∀ (i : J.R),
                      Eq.{s + 1} (α := CC (I.right i))
                        ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i))
                            (x (J.fst i)) :
                          CC (I.right i))
                        ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i))
                            (x (J.snd i)) :
                          CC (I.right i)))
                    (fun (x_1 : J.L) ↦
                      (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j)
                        (WalkingMulticospan.left x_1))
                    sorry :
                  { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
                    ∀ (i : J.R),
                      Eq.{s + 1} (α := CC (I.right i))
                        ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i))
                            (x (J.fst i)) :
                          CC (I.right i))
                        ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i))
                            (x (J.snd i)) :
                          CC (I.right i)) }))
              x)) :
        (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j)
      (WalkingMulticospan.right b) =
    (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.right b)
Tactic: ext (a | b)