-- 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
i₁ i₂ : ι
x : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₁
x_1 : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U 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₂))
eq₁ :
  (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.ιColimitType
      (WalkingMultispan.right i₁) (Subtype.mk (p := fun (x : X) ↦ x ∈ U i₁) x₁ ⋯) =
    (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.ιColimitType
      (WalkingMultispan.left (i₁, i₂)) (Subtype.mk (p := fun (x : X) ↦ x ∈ V i₁ i₂) x₁ ⋯)
eq₂ :
  (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.ιColimitType
      (WalkingMultispan.right i₂) (Subtype.mk (p := fun (x : X) ↦ x ∈ U i₂) x₁ ⋯) =
    (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.ιColimitType
      (WalkingMultispan.left (i₁, i₂)) (Subtype.mk (p := fun (x : X) ↦ x ∈ V i₁ i₂) x₁ ⋯)
h₃ :
  (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.ιColimitType
      (WalkingMultispan.left (i₁, i₂)) (Subtype.mk (p := fun (x : X) ↦ x ∈ V i₁ i₂) x₁ ⋯) =
    (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₁) =
    (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₂)
have h₄ : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.ιColimitType
    (WalkingMultispan.left (i₁, i₂)) (Subtype.mk (p := fun (x : X) ↦ x ∈ V i₁ i₂) x₁ sorry) =
  (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.ιColimitType
    (WalkingMultispan.left (i₁, i₂)) (Subtype.mk (p := fun (x : X) ↦ x ∈ V i₁ i₂) x₁ sorry)
Tactic: rw [eq₁, eq₂]