awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
τ : F ⟶ F'
e : F ≅ F'
G : Functor.{v₂, v₃, u₂, u₃} D E
F'' : Functor.{v₁, v₁, u₁, u₁} C C
eF'' : F'' ≅ 𝟭 C
FG : Functor.{v₁, v₃, u₁, u₃} C E
eFG : F ⋙ G ≅ FG
A : Type u
inst_3 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} E
inst_4 : F.IsContinuous J K
inst_5 : F'.IsContinuous J K
w :
  ∀ (x : Sheaf.{v₂, t, u₂, u} K A) (x_1 : Cᵒᵖ),
    Eq (α :=
      (obj (F'.sheafPushforwardContinuous A J K) x).obj (P := Presheaf.IsSheaf J).obj x_1 ⟶
        (obj (F'.sheafPushforwardContinuous A J K) x).obj (P := Presheaf.IsSheaf J).obj x_1)
      (NatTrans.app
        (InducedCategory.Hom.hom
          (NatTrans.app
            (CategoryStruct.comp (Y := F.sheafPushforwardContinuous A J K)
              (sheafPushforwardContinuousNatTrans e.hom A J K) (sheafPushforwardContinuousNatTrans e.inv A J K))
            x))
        x_1)
      (NatTrans.app (InducedCategory.Hom.hom (NatTrans.app (𝟙 (F'.sheafPushforwardContinuous A J K)) x)) x_1)
⊢ Eq (α :=
    Quiver.Hom (V := Sheaf.{v₂, t, u₂, u} K A ⥤ Sheaf.{v₁, t, u₁, u} J A) (F'.sheafPushforwardContinuous A J K)
      (F'.sheafPushforwardContinuous A J K))
    (CategoryStruct.comp (Y := F.sheafPushforwardContinuous A J K) (sheafPushforwardContinuousNatTrans e.hom A J K)
      (sheafPushforwardContinuousNatTrans e.inv A J K))
    (𝟙 (F'.sheafPushforwardContinuous A J K))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
τ : F ⟶ F'
e : F ≅ F'
G : Functor.{v₂, v₃, u₂, u₃} D E
F'' : Functor.{v₁, v₁, u₁, u₁} C C
eF'' : F'' ≅ 𝟭 C
FG : Functor.{v₁, v₃, u₁, u₃} C E
eFG : F ⋙ G ≅ FG
A : Type u
inst_3 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} E
inst_4 : F.IsContinuous J K
inst_5 : F'.IsContinuous J K
x : Sheaf.{v₂, t, u₂, u} K A
x_1 : Cᵒᵖ
⊢ Eq (α :=
    (obj (F'.sheafPushforwardContinuous A J K) x).obj (P := Presheaf.IsSheaf J).obj x_1 ⟶
      (obj (F'.sheafPushforwardContinuous A J K) x).obj (P := Presheaf.IsSheaf J).obj x_1)
    (NatTrans.app
      (InducedCategory.Hom.hom
        (NatTrans.app
          (CategoryStruct.comp (Y := F.sheafPushforwardContinuous A J K)
            (sheafPushforwardContinuousNatTrans e.hom A J K) (sheafPushforwardContinuousNatTrans e.inv A J K))
          x))
      x_1)
    (NatTrans.app (InducedCategory.Hom.hom (NatTrans.app (𝟙 (F'.sheafPushforwardContinuous A J K)) x)) x_1)

Tactic:
simp [← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_3 : F.IsContinuous J K
inst_4 : G.IsContinuous K J
P : Sheaf.{v₂, v₃, u₂, u₃} K E
⊢ InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        Functor.obj (F.sheafPushforwardContinuous E J K)
          (Functor.obj (G.sheafPushforwardContinuous E K J) (Functor.obj (F.sheafPushforwardContinuous E J K) P)))
        (Functor.map (F.sheafPushforwardContinuous E J K)
            (NatTrans.app
              {
                app := fun (P : Sheaf.{v₂, v₃, u₂, u₃} K E) ↦
                  { hom := NatTrans.app (unit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf K)) },
                naturality := ⋯ }
              P) :
          Functor.obj (F.sheafPushforwardContinuous E J K) P ⟶
            Functor.obj (F.sheafPushforwardContinuous E J K)
              (Functor.obj (G.sheafPushforwardContinuous E K J) (Functor.obj (F.sheafPushforwardContinuous E J K) P)))
        (NatTrans.app
            {
              app := fun (P : Sheaf.{v₁, v₃, u₁, u₃} J E) ↦
                { hom := NatTrans.app (counit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf J)) },
              naturality := ⋯ }
            (Functor.obj (F.sheafPushforwardContinuous E J K) P) :
          Functor.obj (G.sheafPushforwardContinuous E K J ⋙ F.sheafPushforwardContinuous E J K)
              (Functor.obj (F.sheafPushforwardContinuous E J K) P) ⟶
            Functor.obj (𝟭 (Sheaf.{v₁, v₃, u₁, u₃} J E)) (Functor.obj (F.sheafPushforwardContinuous E J K) P))) =
    InducedCategory.Hom.hom (𝟙 (Functor.obj (F.sheafPushforwardContinuous E J K) P))

Tactic:
(adj.op.whiskerLeft _).left_triangle_components P.obj

Premises used: CategoryTheory.Adjunction.whiskerLeft, CategoryTheory.Adjunction.op, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_3 : F.IsContinuous J K
inst_4 : G.IsContinuous K J
P : Sheaf.{v₂, v₃, u₂, u₃} K E
⊢ InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        Functor.obj (F.sheafPushforwardContinuous E J K)
          (Functor.obj (G.sheafPushforwardContinuous E K J) (Functor.obj (F.sheafPushforwardContinuous E J K) P)))
        (Functor.map (F.sheafPushforwardContinuous E J K)
            (NatTrans.app
              {
                app := fun (P : Sheaf.{v₂, v₃, u₂, u₃} K E) ↦
                  { hom := NatTrans.app (unit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf K)) },
                naturality := ⋯ }
              P) :
          Functor.obj (F.sheafPushforwardContinuous E J K) P ⟶
            Functor.obj (F.sheafPushforwardContinuous E J K)
              (Functor.obj (G.sheafPushforwardContinuous E K J) (Functor.obj (F.sheafPushforwardContinuous E J K) P)))
        (NatTrans.app
            {
              app := fun (P : Sheaf.{v₁, v₃, u₁, u₃} J E) ↦
                { hom := NatTrans.app (counit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf J)) },
              naturality := ⋯ }
            (Functor.obj (F.sheafPushforwardContinuous E J K) P) :
          Functor.obj (G.sheafPushforwardContinuous E K J ⋙ F.sheafPushforwardContinuous E J K)
              (Functor.obj (F.sheafPushforwardContinuous E J K) P) ⟶
            Functor.obj (𝟭 (Sheaf.{v₁, v₃, u₁, u₃} J E)) (Functor.obj (F.sheafPushforwardContinuous E J K) P))) =
    InducedCategory.Hom.hom (𝟙 (Functor.obj (F.sheafPushforwardContinuous E J K) P))

Tactic:
exact (adj.op.whiskerLeft _).left_triangle_components P.obj

Premises used: CategoryTheory.Adjunction.whiskerLeft, CategoryTheory.Adjunction.op, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_3 : F.IsContinuous J K
inst_4 : G.IsContinuous K J
P : Sheaf.{v₁, v₃, u₁, u₃} J E
h :
  InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        Functor.obj (G.sheafPushforwardContinuous E K J)
          (Functor.obj (F.sheafPushforwardContinuous E J K) (Functor.obj (G.sheafPushforwardContinuous E K J) P)))
        (NatTrans.app
            {
              app := fun (P : Sheaf.{v₂, v₃, u₂, u₃} K E) ↦
                { hom := NatTrans.app (unit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf K)) },
              naturality := ⋯ }
            (Functor.obj (G.sheafPushforwardContinuous E K J) P) :
          Functor.obj (𝟭 (Sheaf.{v₂, v₃, u₂, u₃} K E)) (Functor.obj (G.sheafPushforwardContinuous E K J) P) ⟶
            Functor.obj (F.sheafPushforwardContinuous E J K ⋙ G.sheafPushforwardContinuous E K J)
              (Functor.obj (G.sheafPushforwardContinuous E K J) P))
        (Functor.map (G.sheafPushforwardContinuous E K J)
          (NatTrans.app
            {
              app := fun (P : Sheaf.{v₁, v₃, u₁, u₃} J E) ↦
                { hom := NatTrans.app (counit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf J)) },
              naturality := ⋯ }
            P))) =
    InducedCategory.Hom.hom (𝟙 (Functor.obj (G.sheafPushforwardContinuous E K J) P))
⊢ CategoryStruct.comp (Y :=
      Functor.obj (G.sheafPushforwardContinuous E K J)
        (Functor.obj (F.sheafPushforwardContinuous E J K) (Functor.obj (G.sheafPushforwardContinuous E K J) P)))
      (NatTrans.app
          {
            app := fun (P : Sheaf.{v₂, v₃, u₂, u₃} K E) ↦
              { hom := NatTrans.app (unit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf K)) },
            naturality := ⋯ }
          (Functor.obj (G.sheafPushforwardContinuous E K J) P) :
        Functor.obj (𝟭 (Sheaf.{v₂, v₃, u₂, u₃} K E)) (Functor.obj (G.sheafPushforwardContinuous E K J) P) ⟶
          Functor.obj (F.sheafPushforwardContinuous E J K ⋙ G.sheafPushforwardContinuous E K J)
            (Functor.obj (G.sheafPushforwardContinuous E K J) P))
      (Functor.map (G.sheafPushforwardContinuous E K J)
        (NatTrans.app
          {
            app := fun (P : Sheaf.{v₁, v₃, u₁, u₃} J E) ↦
              { hom := NatTrans.app (counit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf J)) },
            naturality := ⋯ }
          P)) =
    𝟙 (Functor.obj (G.sheafPushforwardContinuous E K J) P)

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_3 : F.IsContinuous J K
inst_4 : G.IsContinuous K J
P : Sheaf.{v₁, v₃, u₁, u₃} J E
⊢ InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        Functor.obj (G.sheafPushforwardContinuous E K J)
          (Functor.obj (F.sheafPushforwardContinuous E J K) (Functor.obj (G.sheafPushforwardContinuous E K J) P)))
        (NatTrans.app
            {
              app := fun (P : Sheaf.{v₂, v₃, u₂, u₃} K E) ↦
                { hom := NatTrans.app (unit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf K)) },
              naturality := ⋯ }
            (Functor.obj (G.sheafPushforwardContinuous E K J) P) :
          Functor.obj (𝟭 (Sheaf.{v₂, v₃, u₂, u₃} K E)) (Functor.obj (G.sheafPushforwardContinuous E K J) P) ⟶
            Functor.obj (F.sheafPushforwardContinuous E J K ⋙ G.sheafPushforwardContinuous E K J)
              (Functor.obj (G.sheafPushforwardContinuous E K J) P))
        (Functor.map (G.sheafPushforwardContinuous E K J)
          (NatTrans.app
            {
              app := fun (P : Sheaf.{v₁, v₃, u₁, u₃} J E) ↦
                { hom := NatTrans.app (counit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf J)) },
              naturality := ⋯ }
            P))) =
    InducedCategory.Hom.hom (𝟙 (Functor.obj (G.sheafPushforwardContinuous E K J) P))

Tactic:
(adj.op.whiskerLeft _).right_triangle_components P.obj

Premises used: CategoryTheory.Adjunction.whiskerLeft, CategoryTheory.Adjunction.op, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Adjunction.right_triangle_components
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_3 : F.IsContinuous J K
inst_4 : G.IsContinuous K J
P : Sheaf.{v₁, v₃, u₁, u₃} J E
⊢ InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        Functor.obj (G.sheafPushforwardContinuous E K J)
          (Functor.obj (F.sheafPushforwardContinuous E J K) (Functor.obj (G.sheafPushforwardContinuous E K J) P)))
        (NatTrans.app
            {
              app := fun (P : Sheaf.{v₂, v₃, u₂, u₃} K E) ↦
                { hom := NatTrans.app (unit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf K)) },
              naturality := ⋯ }
            (Functor.obj (G.sheafPushforwardContinuous E K J) P) :
          Functor.obj (𝟭 (Sheaf.{v₂, v₃, u₂, u₃} K E)) (Functor.obj (G.sheafPushforwardContinuous E K J) P) ⟶
            Functor.obj (F.sheafPushforwardContinuous E J K ⋙ G.sheafPushforwardContinuous E K J)
              (Functor.obj (G.sheafPushforwardContinuous E K J) P))
        (Functor.map (G.sheafPushforwardContinuous E K J)
          (NatTrans.app
            {
              app := fun (P : Sheaf.{v₁, v₃, u₁, u₃} J E) ↦
                { hom := NatTrans.app (counit (Adjunction.whiskerLeft E adj.op)) (P.obj (P := Presheaf.IsSheaf J)) },
              naturality := ⋯ }
            P))) =
    InducedCategory.Hom.hom (𝟙 (Functor.obj (G.sheafPushforwardContinuous E K J) P))

Tactic:
exact (adj.op.whiskerLeft _).right_triangle_components P.obj

Premises used: CategoryTheory.Adjunction.whiskerLeft, CategoryTheory.Adjunction.op, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Adjunction.right_triangle_components
-- 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
⊢ HasPullback (Cofan.IsColimit.desc hc E.f) (Cofan.IsColimit.desc hc E.f)

Tactic:
have : HasPullback (Cofan.IsColimit.desc hc E.f) (Cofan.IsColimit.desc hc E.f) :=
    inferInstanceAs <| HasPullback
      ((E.sigmaOfIsColimit hc).f ⟨⟩) ((E.sigmaOfIsColimit hc).f ⟨⟩)
-- 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)
b : E.toPreOneHypercover.I₁'
⊢ Eq (α :=
    E.X b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).1 ⟶
      S)
    (E.f b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).1 ≫
      𝟙 S)
    (c.inj
        b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).1 ≫
      (E.sigmaOfIsColimit hc).f PUnit.unit)

Tactic:
simp
-- 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)
b : E.toPreOneHypercover.I₁'
⊢ Eq (α :=
    E.X b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).2 ⟶
      S)
    (E.f b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).2 ≫
      𝟙 S)
    (c.inj
        b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).2 ≫
      (E.sigmaOfIsColimit hc).f PUnit.unit)

Tactic:
simp
-- 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₀)
refine :
  Nonempty
    (IsColimit.{w, v_1, w, u_1} (J := Discrete (E.I₀ × E.I₀)) (F :=
      Discrete.functor fun (i : E.I₀ × E.I₀) ↦
        E.toPreOneHypercover.Y' ((equiv.symm : (a : E.I₀ × E.I₀) → E.toPreOneHypercover.I₁') i))
      (Cofan.mk c'.pt fun (i : E.I₀ × E.I₀) ↦ c'.inj ((equiv.symm : (a : E.I₀ × E.I₀) → E.toPreOneHypercover.I₁') i)))
⊢ IsColimit c'

Tactic:
refine (c'.isColimitEquivOfEquiv equiv.symm).symm (Nonempty.some ?_)

Premises used: CategoryTheory.Limits.Cofan.isColimitEquivOfEquiv, Nonempty.some, Equiv.symm, DFunLike.coe
-- 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₀)
⊢ ∀ (i : E.I₀), c.inj i ≫ (E.sigmaOfIsColimit hc).f PUnit.unit = E.f i

Tactic:
simp