-- 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 : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit
f :
  ∀ (k_1 : E.toPreOneHypercover.I₁'),
    Eq (α :=
      E.toPreOneHypercover.Y' k_1 ⟶
        (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))
      (c'.inj k_1 ≫
        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)))
      (c'.inj k_1 ≫
        (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))
⊢ 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))

Tactic:
refine Cofan.IsColimit.hom_ext hc' _ _ fun k ↦ ?_

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