-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : Functor.{w, u, w, u + 1} (WalkingMultispan (MultispanShape.prod ι)) (Type u) :=
  (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan
h :
  ∀ (i₁ i₂ : (MultispanShape.prod ι).R)
    (x : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₁)
    (x : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₂) (x₁ : X)
    (h₁ : x₁ ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₁) (x₂ : X)
    (h₂ : x₂ ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₂)
    (h :
      Eq.{u + 1} (α :=
        Functor.CoconeTypes.pt.{u, u, w, w} (J := WalkingMultispan (MultispanShape.prod ι)) (F :=
          (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan)
          (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
              (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
                (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
            (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes)))
        (Functor.CoconeTypes.ι
          (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
              (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
                (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
            (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
          (WalkingMultispan.right i₁)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₁) x₁ h₁))
        (Functor.CoconeTypes.ι
          (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
              (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
                (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
            (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
          (WalkingMultispan.right i₂)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₂) x₂ h₂))),
    (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.ιColimitType
        (WalkingMultispan.right i₁)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₁) x₁ h₁) =
      (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.ιColimitType
        (WalkingMultispan.right i₂)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₂) x₂ h₂)
⊢ (∀ (i₁ i₂ : (MultispanShape.prod ι).R)
      (x₁ : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₁)
      (x₂ : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₂),
      Eq.{u + 1} (α :=
          Functor.CoconeTypes.pt.{u, u, w, w} (J := WalkingMultispan (MultispanShape.prod ι)) (F :=
            (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan)
            (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
                (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
                  (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
              (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes)))
          (Functor.CoconeTypes.ι
            (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
                (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
                  (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
              (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
            (WalkingMultispan.right i₁) x₁)
          (Functor.CoconeTypes.ι
            (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
                (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
                  (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
              (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
            (WalkingMultispan.right i₂) x₂) →
        (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.ιColimitType
            (WalkingMultispan.right i₁) x₁ =
          (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.ιColimitType
            (WalkingMultispan.right i₂) x₂) ∧
    ∀
      (x :
        Functor.CoconeTypes.pt.{u, u, w, w} (J := WalkingMultispan (MultispanShape.prod ι)) (F :=
          (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan)
          (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
              (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
                (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
            (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))),
      ∃ (i : (MultispanShape.prod ι).R) (a :
        (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i),
        Functor.CoconeTypes.ι
            (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
                (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
                  (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
              (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
            (WalkingMultispan.right i) a =
          x
have h₁ : ∀
  (x :
    Functor.CoconeTypes.pt.{u, u, w, w} (J := WalkingMultispan (MultispanShape.prod ι)) (F :=
      (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan)
      (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
          (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
            (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
        (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes)))
  (x : X) (hx : x ∈ c.multicofork (x := A) (u := U) (v := V).pt),
  ∃ (i : (MultispanShape.prod ι).R) (a : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i),
    Functor.CoconeTypes.ι
        (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
            (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
              (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
          (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
        (WalkingMultispan.right i) a =
      Subtype.mk (p := fun (x : X) ↦ x ∈ c.multicofork (x := A) (u := U) (v := V).pt) x hx
Tactic: refine ⟨fun i₁ i₂ ⟨x₁, h₁⟩ ⟨x₂, h₂⟩ h ↦ ?_, fun ⟨x, hx⟩ ↦ ?_⟩