-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
refine_1 :
  ((E.sigmaOfIsColimit hc hd).multifork F).pt ≅
    Cone.pt.{w, v_1, w, u_1} (J := WalkingMulticospan (E.sigmaOfIsColimit hc hd).multicospanShape)
      (Functor.obj
        (Equivalence.functor
          (Equivalence.symm
            (MulticospanIndex.multiforkOfParallelHomsEquivFork (E.sigmaOfIsColimit hc hd).multicospanShape
              (F.map
                (Quiver.Hom.op
                  (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                    E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                      c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)))
              (F.map
                (Quiver.Hom.op
                  (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                    E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                      c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))))))
        (E.forkOfIsColimit hc hd F))
refine_2 :
  (i : (E.sigmaOfIsColimit hc hd).multicospanShape.L) →
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).left i ≅
      MulticospanIndex.left
        (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape (X := F.obj (op c.pt))
          (F.map
            (Quiver.Hom.op
              (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                  c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)))
          (F.map
            (Quiver.Hom.op
              (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                  c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))))
        i
⊢ IsLimit ((E.sigmaOfIsColimit hc hd).multifork F) ≃ IsLimit (E.multifork F)
have refine_3 : (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R) →
  ((E.sigmaOfIsColimit hc hd).multicospanIndex F).right i ≅
    MulticospanIndex.right
      (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape (X := F.obj (op c.pt))
        (F.map
          (Quiver.Hom.op
            (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
              E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)))
        (F.map
          (Quiver.Hom.op
            (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
              E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))))
      i
Tactic: refine (Multifork.isLimitEquivOfIsos _ _ ?_ ?_ ?_ ?_ ?_ ?_).trans
    (IsLimit.ofConeEquiv <| (MulticospanIndex.multiforkOfParallelHomsEquivFork
      (E.sigmaOfIsColimit hc hd).multicospanShape _ _).symm) |>.trans
      (E.isLimitMultiforkEquivIsLimitFork hc hd F).symm