awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X₀ Y₀ : C₀
a : Y₀ ⟶ X₀
Y : C
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
b : F.obj Y₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac : b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = F.map a
⊢ CategoryStruct.comp (Y := presheafObj data G₀ (F.obj X₀))
        (presheafObjObjIso.inv data G₀ X₀ :
          G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶ (presheaf data G₀).obj (op (F.obj X₀)))
        (presheafObjObjIso.hom data G₀ X₀) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map a.op =
    𝟙 (G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀)) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map a.op

Tactic:
simp [presheafObjObjIso.hom_map data G₀ _ b fac, ← IsDenseSubsite.mapPreimage_comp, fac]

Premises used: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_map
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
i : (data X).I₀
rw :
  Eq (α := presheafObj data G₀ X ⟶ (presheaf data G₀).obj (op (F.obj ((data X).X i))))
    (presheafMap data G₀ ((data X).f i)) (presheafObjπ data G₀ X i ≫ Iso.inv (presheafObjObjIso data G₀ ((data X).X i)))
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafMap data G₀ ((data X).f i) ≫ Iso.hom (presheafObjObjIso data G₀ ((data X).X i))) (presheafObjπ data G₀ X i)

Tactic:
rw [← cancel_mono (presheafObjObjIso data G₀ ((data X).X i)).inv, assoc, Iso.hom_inv_id,
    comp_id]

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso, CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.PreOneHypercoverDenseData.X, CategoryTheory.Iso.inv, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
i : (data X).I₀
h :
  ∀
    (i_1 :
      PreOneHypercoverDenseData.I₀ (S := F.obj ((data X).X i))
        (toPreOneHypercoverDenseData (data (F.obj ((data X).X i))))),
    Eq (α :=
      presheafObj data G₀ X ⟶
        G₀.obj (P := Presheaf.IsSheaf J₀).obj
          (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) i_1)))
      (presheafMap data G₀ ((data X).f i) ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) i_1)
      (CategoryStruct.comp (Y := presheafObj data G₀ (F.obj ((data X).X i)))
        (presheafObjπ data G₀ X i ≫ Iso.inv (presheafObjObjIso data G₀ ((data X).X i)) :
          presheafObj data G₀ X ⟶ (presheaf data G₀).obj (op (F.obj ((data X).X i))))
        (presheafObjπ data G₀ (F.obj ((data X).X i)) i_1))
⊢ Eq (α := presheafObj data G₀ X ⟶ (presheaf data G₀).obj (op (F.obj ((data X).X i))))
    (presheafMap data G₀ ((data X).f i)) (presheafObjπ data G₀ X i ≫ Iso.inv (presheafObjObjIso data G₀ ((data X).X i)))

Tactic:
apply presheafObj_hom_ext

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_hom_ext
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
i : (data X).I₀
j : PreOneHypercoverDenseData.I₀ (S := F.obj ((data X).X i)) (toPreOneHypercoverDenseData (data (F.obj ((data X).X i))))
h :
  Eq (α :=
    presheafObj data G₀ X ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) j)))
    (restriction data G₀
      (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) j ≫ (data X).f i))
    (presheafObjπ data G₀ X i ≫
      IsDenseSubsite.mapPreimage J F G₀
        (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) j))
⊢ Eq (α :=
    presheafObj data G₀ X ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) j)))
    (presheafMap data G₀ ((data X).f i) ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) j)
    (CategoryStruct.comp (Y := presheafObj data G₀ (F.obj ((data X).X i)))
      (presheafObjπ data G₀ X i ≫ Iso.inv (presheafObjObjIso data G₀ ((data X).X i)) :
        presheafObj data G₀ X ⟶ (presheaf data G₀).obj (op (F.obj ((data X).X i))))
      (presheafObjπ data G₀ (F.obj ((data X).X i)) j))

Tactic:
rw [assoc, presheafMap_π, presheafObjObjIso, presheafObjObjIso.inv_π data G₀]

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso, CategoryTheory.Category.assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
i : (data X).I₀
j : PreOneHypercoverDenseData.I₀ (S := F.obj ((data X).X i)) (toPreOneHypercoverDenseData (data (F.obj ((data X).X i))))
h :
  PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) j ≫ (data X).f i =
    PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) j ≫ (data X).f i
⊢ Eq (α :=
    presheafObj data G₀ X ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) j)))
    (restriction data G₀
      (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) j ≫ (data X).f i))
    (presheafObjπ data G₀ X i ≫
      IsDenseSubsite.mapPreimage J F G₀
        (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) j))

Tactic:
apply restriction_eq_of_fac

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_eq_of_fac
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
i : (data X).I₀
j : PreOneHypercoverDenseData.I₀ (S := F.obj ((data X).X i)) (toPreOneHypercoverDenseData (data (F.obj ((data X).X i))))
⊢ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) j ≫ (data X).f i =
    PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj ((data X).X i)))) j ≫ (data X).f i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X₀ Y₀ : C₀
f : X₀ ⟶ Y₀
h :
  ∀
    (i :
      PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀)))
        (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))),
    CategoryStruct.comp (Y := presheafObj data G₀ (unop (op (F.obj X₀))))
        (G₀.obj (P := Presheaf.IsSheaf J₀).map f.op ≫ Iso.inv (presheafObjObjIso data G₀ X₀) :
          G₀.obj (P := Presheaf.IsSheaf J₀).obj (op Y₀) ⟶ (presheaf data G₀).obj (op (F.obj X₀)))
        (presheafObjπ data G₀ (unop (op (F.obj X₀))) i) =
      CategoryStruct.comp (Y := presheafObj data G₀ (unop (op (F.obj X₀))))
        (CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj Y₀))) (Iso.inv (presheafObjObjIso data G₀ Y₀))
          (presheafMap data G₀ (F.map f)))
        (presheafObjπ data G₀ (unop (op (F.obj X₀))) i)
⊢ Eq (α := G₀.obj (P := Presheaf.IsSheaf J₀).obj (op Y₀) ⟶ (presheaf data G₀).obj (op (F.obj X₀)))
    (G₀.obj (P := Presheaf.IsSheaf J₀).map f.op ≫ Iso.inv (presheafObjObjIso data G₀ X₀))
    (CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj Y₀))) (Iso.inv (presheafObjObjIso data G₀ Y₀))
      (presheafMap data G₀ (F.map f)))

Tactic:
apply presheafObj_hom_ext

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_hom_ext
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X₀ Y₀ : C₀
f : X₀ ⟶ Y₀
j : PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀))) (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))
⊢ CategoryStruct.comp (Y := presheafObj data G₀ (unop (op (F.obj X₀))))
      (G₀.obj (P := Presheaf.IsSheaf J₀).map f.op ≫ Iso.inv (presheafObjObjIso data G₀ X₀) :
        G₀.obj (P := Presheaf.IsSheaf J₀).obj (op Y₀) ⟶ (presheaf data G₀).obj (op (F.obj X₀)))
      (presheafObjπ data G₀ (unop (op (F.obj X₀))) j) =
    CategoryStruct.comp (Y := presheafObj data G₀ (unop (op (F.obj X₀))))
      (CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj Y₀))) (Iso.inv (presheafObjObjIso data G₀ Y₀))
        (presheafMap data G₀ (F.map f)))
      (presheafObjπ data G₀ (unop (op (F.obj X₀))) j)

Tactic:
simp [presheafObjObjIso, IsDenseSubsite.mapPreimage_comp]

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
rw :
  Presheaf.IsSheaf J₀ (F.op ⋙ presheaf data G₀) ∧
    ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork (presheaf data G₀)))
⊢ Presheaf.IsSheaf J (presheaf data G₀)

Tactic:
rw [isSheaf_iff data]

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
left : Presheaf.IsSheaf J₀ (F.op ⋙ presheaf data G₀)
right : ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork (presheaf data G₀)))
⊢ Presheaf.IsSheaf J₀ (F.op ⋙ presheaf data G₀) ∧
    ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork (presheaf data G₀)))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
⊢ Presheaf.IsSheaf J₀ (F.op ⋙ presheaf data G₀)

Tactic:
(Presheaf.isSheaf_of_iso_iff (compPresheafIso data G₀)).2 G₀.property

Premises used: Iff.mpr, CategoryTheory.Presheaf.isSheaf_of_iso_iff, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.compPresheafIso
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
⊢ Presheaf.IsSheaf J₀ (F.op ⋙ presheaf data G₀)

Tactic:
exact (Presheaf.isSheaf_of_iso_iff (compPresheafIso data G₀)).2 G₀.property

Premises used: Iff.mpr, CategoryTheory.Presheaf.isSheaf_of_iso_iff, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.compPresheafIso
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
⊢ Nonempty (IsLimit ((data X).toOneHypercover.multifork (presheaf data G₀)))

Tactic:
⟨(IsLimit.postcomposeHomEquiv
      (WalkingMulticospan.functorExt
          (fun _ ↦ presheafObjObjIso _ _ _) (fun _ ↦ presheafObjObjIso _ _ _)
          (fun _ ↦ (compPresheafIso _ _).hom.naturality _)
          (fun _ ↦ (compPresheafIso _ _).hom.naturality _)) _).1
      (IsLimit.ofIsoLimit (presheafObjIsLimit data G₀ X)
        (Multifork.ext (Iso.refl _) (fun i ↦ ?_)))⟩

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjIsLimit, CategoryTheory.Limits.WalkingMulticospan.functorExt, CategoryTheory.Iso.refl, Equiv.toFun, Nonempty.intro, CategoryTheory.Limits.Multifork.ext, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
right :
  ∀ (i : (data X).multicospanShape.L),
    Iso.hom (Iso.refl (presheafObjMultifork data G₀ X).pt) ≫
        Multifork.ι
          (obj
            (Cone.postcompose
              (Iso.hom
                (WalkingMulticospan.functorExt
                  (fun (x : (data X).toOneHypercover.multicospanShape.L) ↦ presheafObjObjIso data G₀ ((data X).X x))
                  (fun (x : (data X).toOneHypercover.multicospanShape.R) ↦
                    presheafObjObjIso data G₀
                      ((data X).Y
                        (x.snd (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
                          (data X).toOneHypercover.I₁ i.1 i.2))))
                  ⋯ ⋯)))
            ((data X).toOneHypercover.multifork (presheaf data G₀)))
          i =
      (presheafObjMultifork data G₀ X).ι i
⊢ Nonempty (IsLimit ((data X).toOneHypercover.multifork (presheaf data G₀)))

Tactic:
refine ⟨(IsLimit.postcomposeHomEquiv
      (WalkingMulticospan.functorExt
          (fun _ ↦ presheafObjObjIso _ _ _) (fun _ ↦ presheafObjObjIso _ _ _)
          (fun _ ↦ (compPresheafIso _ _).hom.naturality _)
          (fun _ ↦ (compPresheafIso _ _).hom.naturality _)) _).1
      (IsLimit.ofIsoLimit (presheafObjIsLimit data G₀ X)
        (Multifork.ext (Iso.refl _) (fun i ↦ ?_)))⟩
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
i : (data X).multicospanShape.L
⊢ Iso.hom (Iso.refl (presheafObjMultifork data G₀ X).pt) ≫
      Multifork.ι
        (obj
          (Cone.postcompose
            (Iso.hom
              (WalkingMulticospan.functorExt
                (fun (x : (data X).toOneHypercover.multicospanShape.L) ↦ presheafObjObjIso data G₀ ((data X).X x))
                (fun (x : (data X).toOneHypercover.multicospanShape.R) ↦
                  presheafObjObjIso data G₀
                    ((data X).Y
                      (x.snd (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
                        (data X).toOneHypercover.I₁ i.1 i.2))))
                ⋯ ⋯)))
          ((data X).toOneHypercover.multifork (presheaf data G₀)))
        i =
    (presheafObjMultifork data G₀ X).ι i

Tactic:
simp [Multifork.ι, PreOneHypercover.multifork]

Premises used: CategoryTheory.PreOneHypercover.multifork, CategoryTheory.Limits.Multifork.ι
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
inst_5 : F.IsOneHypercoverDense J₀ J
⊢ IsEquivalence (C := Sheaf.{v, v', u, u'} J A) (F.sheafPushforwardContinuous A J₀ J)

Tactic:
OneHypercoverDenseData.isEquivalence.{w} A (oneHypercoverDenseData F J₀ J)

Premises used: CategoryTheory.Functor.oneHypercoverDenseData, CategoryTheory.Functor.OneHypercoverDenseData.isEquivalence
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
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
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
rw :
  Function.Bijective (α :=
    (fun (X : Type w') ↦ X)
      (obj
        (obj yoneda
          ((obj (G.op.ran ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U)))
        (op X)))
    (β :=
    (fun (X : Type w') ↦ X)
      (obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U)))
        (op X)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (map yoneda (NatTrans.app (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J))) (op U)))
            (op X))) :
      (a :
          (fun (X : Type w') ↦ X)
            ((yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X))) →
        (fun (X : Type w') ↦ X) ((yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)))
⊢ IsIso (X :=
    obj
      (obj yoneda ((obj (G.op.ran ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U)))
      (op X))
    (NatTrans.app (map yoneda (NatTrans.app (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J))) (op U)))
      (op X))

Tactic:
rw [isIso_iff_bijective]

Premises used: CategoryTheory.isIso_iff_bijective