-- Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover.{w, v_1, u_1} S
inst_2 : E.HasPullbacks
c : Cofan.{w, v_1, u_1} E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst_3 : (E.sigmaOfIsColimit hc).HasPullbacks
inst_4 : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
inst_5 :
  PreservesLimit.{w, w, v_1, v_2, u_1, u_2} (J := Discrete E.toPreOneHypercover.I₀)
    (Discrete.functor fun (i : E.toPreOneHypercover.I₀) ↦ op (E.toPreOneHypercover.X i)) F
inst_6 :
  PreservesLimit.{w, w, v_1, v_2, u_1, u_2} (J := Discrete E.toPreOneHypercover.I₁')
    (Discrete.functor fun (i : E.toPreOneHypercover.I₁') ↦ op (E.toPreOneHypercover.Y' i)) F
this : HasPullback (Cofan.IsColimit.desc hc E.f) (Cofan.IsColimit.desc hc E.f)
c' : Cofan.{w, v_1, u_1} E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y (i₁ := PUnit.unit) (i₂ := PUnit.unit) PUnit.unit)
    fun (b : E.toPreOneHypercover.I₁') ↦
    pullback.map
      (E.f b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).1)
      (E.f b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).2)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      (c.inj
        b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).1)
      (c.inj
        b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).2)
      (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
k_1 : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit
k : E.toPreOneHypercover.I₁'
⊢ Eq (α :=
    c'.pt ⟶
      (E.toPreOneHypercover.sigmaOfIsColimit hc hc').X
        ((Equiv.refl (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀ :
            (a : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀) → (E.toPreOneHypercover.sigmaOfIsColimit hc hc').I₀)
          PUnit.unit))
    (CategoryStruct.comp (Y :=
      (E.toPreOneHypercover.sigmaOfIsColimit hc hc').Y (i₁ :=
        (Equiv.refl (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀ :
            (a : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀) → (E.toPreOneHypercover.sigmaOfIsColimit hc hc').I₀)
          PUnit.unit)
        (((fun (x x_1 : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀) ↦
                (Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ x x_1) :
                  (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ x x_1 ≃
                    (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ x x_1))
              PUnit.unit PUnit.unit :
            (a : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit) →
              (E.toPreOneHypercover.sigmaOfIsColimit hc hc').I₁
                ((Equiv.refl (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀ :
                    (a : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀) →
                      (E.toPreOneHypercover.sigmaOfIsColimit hc hc').I₀)
                  PUnit.unit)
                ((Equiv.refl (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀ :
                    (a : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀) →
                      (E.toPreOneHypercover.sigmaOfIsColimit hc hc').I₀)
                  PUnit.unit))
          k_1))
      (Iso.hom
        ((fun (x x_1 : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀)
              (x_2 : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ x x_1) ↦
            (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y x_2) :
              (E.sigmaOfIsColimit hc).toPreOneHypercover.Y x_2 ≅ (E.sigmaOfIsColimit hc).toPreOneHypercover.Y x_2))
          PUnit.unit PUnit.unit k_1))
      ((E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₁
        (((fun (x x_1 : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀) ↦
                (Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ x x_1) :
                  (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ x x_1 ≃
                    (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ x x_1))
              PUnit.unit PUnit.unit :
            (a : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit) →
              (E.toPreOneHypercover.sigmaOfIsColimit hc hc').I₁
                ((Equiv.refl (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀ :
                    (a : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀) →
                      (E.toPreOneHypercover.sigmaOfIsColimit hc hc').I₀)
                  PUnit.unit)
                ((Equiv.refl (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀ :
                    (a : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀) →
                      (E.toPreOneHypercover.sigmaOfIsColimit hc hc').I₀)
                  PUnit.unit))
          k_1)))
    ((E.sigmaOfIsColimit hc).toPreOneHypercover.p₁ k_1 ≫
      Iso.hom
        ((fun (x : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀) ↦
            (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X x) :
              (E.sigmaOfIsColimit hc).toPreOneHypercover.X x ≅ (E.sigmaOfIsColimit hc).toPreOneHypercover.X x))
          PUnit.unit))

Tactic:
exact Cofan.IsColimit.hom_ext hc' _ _ fun a ↦ by simp; simp [c']

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext