-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
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
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
refine_4 :
  ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R),
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).fst i ≫
        Iso.hom (Iso.refl (((E.sigmaOfIsColimit hc hd).multicospanIndex F).right i)) =
      Iso.hom
          (Iso.refl
            (((E.sigmaOfIsColimit hc hd).multicospanIndex F).left
              ((E.sigmaOfIsColimit hc hd).multicospanShape.fst i))) ≫
        MulticospanIndex.fst
          (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
refine_5 :
  ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R),
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).snd i ≫
        Iso.hom (Iso.refl (((E.sigmaOfIsColimit hc hd).multicospanIndex F).right i)) =
      Iso.hom
          (Iso.refl
            (((E.sigmaOfIsColimit hc hd).multicospanIndex F).left
              ((E.sigmaOfIsColimit hc hd).multicospanShape.snd i))) ≫
        MulticospanIndex.snd
          (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
refine_6 :
  ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.L),
    Iso.hom (Iso.refl ((E.sigmaOfIsColimit hc hd).multifork F).pt) ≫
        Multifork.ι
          (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))
          i =
      ((E.sigmaOfIsColimit hc hd).multifork F).ι i ≫
        Iso.hom (Iso.refl (((E.sigmaOfIsColimit hc hd).multicospanIndex F).left i))
⊢ IsLimit ((E.sigmaOfIsColimit hc hd).multifork F) ≃ IsLimit (E.multifork F)

Tactic:
refine (Multifork.isLimitEquivOfIsos _ _ ?_ ?_ ?_ ?_ ?_ ?_).trans
    (IsLimit.ofConeEquiv <| (MulticospanIndex.multiforkOfParallelHomsEquivFork
      (E.sigmaOfIsColimit hc hd).multicospanShape _ _).symm) |>.trans
      (E.isLimitMultiforkEquivIsLimitFork hc hd F).symm

Premises used: Equiv.trans, CategoryTheory.PreOneHypercover.isLimitMultiforkEquivIsLimitFork, CategoryTheory.Limits.Multifork.isLimitEquivOfIsos, CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork, CategoryTheory.Limits.IsLimit.ofConeEquiv, Equiv.symm, CategoryTheory.PreOneHypercover.multicospanShape, CategoryTheory.Equivalence.symm, CategoryTheory.PreOneHypercover.sigmaOfIsColimit