-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multiequalizer (goal)
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)
⊢ (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
have 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)))
                sorry)
            ((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 := sorry } :
                  I.sections))
              s)) :
        (j : WalkingMulticospan J) → I.multicospan.obj j)
      (WalkingMulticospan.right r) =
    (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.right r)
Tactic: ext (_ | r)