-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : (↑I.multicospan.sections : Type (max (max u u_2) u_1))
a :
  ∀ (a : J.L),
    (↑((fun (s : I.sections) ↦
                Subtype.mk (p := fun (x : (j : WalkingMulticospan J) → I.multicospan.obj j) ↦
                  x ∈ I.multicospan.sections)
                  (fun (i : WalkingMulticospan J) ↦
                    match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
                    | WalkingMulticospan.left i => s.val i
                    | WalkingMulticospan.right j =>
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                          (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                        (s.val (J.fst j)))
                  ⋯)
              ((fun (s : (↑I.multicospan.sections : Type (max (max u u_2) u_1))) ↦
                  ({
                      val := fun (i : J.L) ↦
                        (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.left i),
                      property := ⋯ } :
                    I.sections))
                s)) :
          (j : WalkingMulticospan J) → I.multicospan.obj j)
        (WalkingMulticospan.left a) =
      (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.left a)
a₁ :
  ∀ (r : J.R),
    (↑((fun (s : I.sections) ↦
                Subtype.mk (p := fun (x : (j : WalkingMulticospan J) → I.multicospan.obj j) ↦
                  x ∈ I.multicospan.sections)
                  (fun (i : WalkingMulticospan J) ↦
                    match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
                    | WalkingMulticospan.left i => s.val i
                    | WalkingMulticospan.right j =>
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                          (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                        (s.val (J.fst j)))
                  ⋯)
              ((fun (s : (↑I.multicospan.sections : Type (max (max u u_2) u_1))) ↦
                  ({
                      val := fun (i : J.L) ↦
                        (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.left i),
                      property := ⋯ } :
                    I.sections))
                s)) :
          (j : WalkingMulticospan J) → I.multicospan.obj j)
        (WalkingMulticospan.right r) =
      (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.right r)
⊢ (fun (s : I.sections) ↦
        Subtype.mk (p := fun (x : (j : WalkingMulticospan J) → I.multicospan.obj j) ↦ x ∈ I.multicospan.sections)
          (fun (i : WalkingMulticospan J) ↦
            match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
            | WalkingMulticospan.left i => s.val i
            | WalkingMulticospan.right j =>
              (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                  (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                (s.val (J.fst j)))
          ⋯)
      ((fun (s : (↑I.multicospan.sections : Type (max (max u u_2) u_1))) ↦
          ({ val := fun (i : J.L) ↦ (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.left i),
              property := ⋯ } :
            I.sections))
        s) =
    s

Tactic:
ext (_ | r)