awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 j : E.I₀),
    Cofan.inj
          (Cofan.mk c'.pt fun (i : E.I₀ × E.I₀) ↦
            c'.inj ((equiv.symm : (a : E.I₀ × E.I₀) → E.toPreOneHypercover.I₁') i))
          (i, j) ≫
        Iso.hom
            (Iso.refl
              (Cocone.pt.{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)))) ≫
          pullback.fst ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit) =
      pullback.fst
          (E.f
            (Sigma.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦
                E.toPreOneHypercover.I₁ i.1 i.2)
                ((equiv.symm : (a : E.I₀ × E.I₀) → E.toPreOneHypercover.I₁') (i, j))).1)
          (E.f
            (Sigma.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦
                E.toPreOneHypercover.I₁ i.1 i.2)
                ((equiv.symm : (a : E.I₀ × E.I₀) → E.toPreOneHypercover.I₁') (i, j))).2) ≫
        c.inj i

Tactic:
simp [c', equiv, Equiv.sigmaPUnit]

Premises used: Equiv.sigmaPUnit
-- 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 j : E.I₀),
    Cofan.inj
          (Cofan.mk c'.pt fun (i : E.I₀ × E.I₀) ↦
            c'.inj ((equiv.symm : (a : E.I₀ × E.I₀) → E.toPreOneHypercover.I₁') i))
          (i, j) ≫
        Iso.hom
            (Iso.refl
              (Cocone.pt.{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)))) ≫
          pullback.snd ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit) =
      pullback.snd
          (E.f
            (Sigma.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦
                E.toPreOneHypercover.I₁ i.1 i.2)
                ((equiv.symm : (a : E.I₀ × E.I₀) → E.toPreOneHypercover.I₁') (i, j))).1)
          (E.f
            (Sigma.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦
                E.toPreOneHypercover.I₁ i.1 i.2)
                ((equiv.symm : (a : E.I₀ × E.I₀) → E.toPreOneHypercover.I₁') (i, j))).2) ≫
        c.inj j

Tactic:
simp [c', equiv, Equiv.sigmaPUnit]

Premises used: Equiv.sigmaPUnit
-- 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₀)
⊢ 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)))

Tactic:
exact IsUniversalColimit.nonempty_isColimit_prod_of_isPullback
      huniv huniv E.f E.f ((E.sigmaOfIsColimit hc).f ⟨⟩) ((E.sigmaOfIsColimit hc).f ⟨⟩)
      (fun i j ↦ .of_hasPullback _ _) (.of_hasPullback _ _) (.refl _) (by simp) (by simp)
      (by simp [c', equiv, Equiv.sigmaPUnit]) (by simp [c', equiv, Equiv.sigmaPUnit])

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback, CategoryTheory.PreZeroHypercover.sigmaOfIsColimit, CategoryTheory.IsPullback.of_hasPullback, PUnit.unit
-- 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₀)
have :
  (hc' : IsColimit c') →
    IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ IsLimit (E.toPreOneHypercover.multifork F)
⊢ IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ IsLimit (E.toPreOneHypercover.multifork F)

Tactic:
have hc' : IsColimit c' := by
    refine (c'.isColimitEquivOfEquiv equiv.symm).symm (Nonempty.some ?_)
    exact IsUniversalColimit.nonempty_isColimit_prod_of_isPullback
      huniv huniv E.f E.f ((E.sigmaOfIsColimit hc).f ⟨⟩) ((E.sigmaOfIsColimit hc).f ⟨⟩)
      (fun i j ↦ .of_hasPullback _ _) (.of_hasPullback _ _) (.refl _) (by simp) (by simp)
      (by simp [c', equiv, Equiv.sigmaPUnit]) (by simp [c', equiv, Equiv.sigmaPUnit])
-- 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'
refine :
  IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃
    IsLimit ((E.toPreOneHypercover.sigmaOfIsColimit hc hc').multifork F)
⊢ IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ IsLimit (E.toPreOneHypercover.multifork F)

Tactic:
refine .trans ?_ (E.toPreOneHypercover.isLimitSigmaOfIsColimitEquiv hc 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)
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 : (E.sigmaOfIsColimit hc).toPreOneHypercover ≅ E.toPreOneHypercover.sigmaOfIsColimit hc hc'
⊢ IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃
    IsLimit ((E.toPreOneHypercover.sigmaOfIsColimit hc hc').multifork F)

Tactic:
apply PreOneHypercover.isLimitEquivOfIso

Premises used: CategoryTheory.PreOneHypercover.isLimitEquivOfIso
-- 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 a : E.toPreOneHypercover.I₁'
⊢ pullback.fst (E.f a.fst (β := fun (i : E.I₀ × E.I₀) ↦ PUnit.{w + 1}).1)
        (E.f a.fst (β := fun (i : E.I₀ × E.I₀) ↦ PUnit.{w + 1}).2) ≫
      c.inj a.fst (β := fun (i : E.I₀ × E.I₀) ↦ PUnit.{w + 1}).1 =
    c'.inj a ≫ pullback.fst ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit)

Tactic:
simp [c']
-- 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
a : E.toPreOneHypercover.I₁'
⊢ pullback.snd (E.f a.fst (β := fun (i : E.I₀ × E.I₀) ↦ PUnit.{w + 1}).1)
        (E.f a.fst (β := fun (i : E.I₀ × E.I₀) ↦ PUnit.{w + 1}).2) ≫
      c.inj a.fst (β := fun (i : E.I₀ × E.I₀) ↦ PUnit.{w + 1}).2 =
    c'.inj a ≫ pullback.snd ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit)

Tactic:
simp [c']
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_2 : G.IsCocontinuous J K
U : C
S : Sieve.{v_2, u_2} (G.obj U)
hS : Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U)) S
⊢ Sieve.functorPullback G S ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
IsCocontinuous.cover_lift hS

Premises used: CategoryTheory.Functor.IsCocontinuous.cover_lift
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
G : Functor.{v_1, v_2, u_1, u_2} C D
G' : Functor.{v_2, v_3, u_2, u_3} D E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
U : C
S : Sieve.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) U)
h :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) U)))
    ((J : (a : C) → Set (Sieve a)) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) U)) S
⊢ Sieve.functorPullback (𝟭 C) S ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
⊢ F.IsCocontinuous J K ↔ CoverPreserving K J G

Tactic:
⟨fun h ↦ ⟨?_⟩, fun h ↦ ⟨?_⟩⟩

Premises used: CategoryTheory.Functor.IsCocontinuous.mk, CategoryTheory.CoverPreserving.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
refine_1 :
  ∀ (h : F.IsCocontinuous J K) {U : D} {S : Sieve.{v_2, u_2} U},
    S ∈ (K : (a : D) → Set (Sieve a)) U →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} (G.obj U))) ((J : (a : C) → Set (Sieve a)) (G.obj U))
        (Sieve.functorPushforward G S)
refine_2 :
  ∀ (h : CoverPreserving K J G) {U : C} {S : Sieve.{v_2, u_2} (F.obj U)},
    Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj U))) ((K : (a : D) → Set (Sieve a)) (F.obj U)) S →
      Sieve.functorPullback F S ∈ (J : (a : C) → Set (Sieve a)) U
⊢ F.IsCocontinuous J K ↔ CoverPreserving K J G

Tactic:
refine ⟨fun h ↦ ⟨?_⟩, fun h ↦ ⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
h : F.IsCocontinuous J K
U : D
S : Sieve.{v_2, u_2} U
hS : S ∈ (K : (a : D) → Set (Sieve a)) U
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (G.obj U))) ((J : (a : C) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G S)

Tactic:
J.superset_covering ?_ <| h.cover_lift (K.pullback_stable (adj.counit.app _) hS)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.app, CategoryTheory.Functor.IsCocontinuous.cover_lift