-- 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'
f :
  ∀ (k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit),
    Eq (α :=
      (E.sigmaOfIsColimit hc).toPreOneHypercover.Y k ⟶
        (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))
        (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))
        ((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)))
      ((E.sigmaOfIsColimit hc).toPreOneHypercover.p₁ k ≫
        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))
⊢ ∀ ⦃j : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀⦄
    (k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit j),
    Eq (α :=
      (E.sigmaOfIsColimit hc).toPreOneHypercover.Y k ⟶
        (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 j :
              (a : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit j) →
                (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₀)
                    j))
            k))
        (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 j k))
        ((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 j :
              (a : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit j) →
                (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₀)
                    j))
            k)))
      ((E.sigmaOfIsColimit hc).toPreOneHypercover.p₁ k ≫
        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:
⟨⟩