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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
p : F.obj W₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac : p ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = a
T₀ : C₀
b : T₀ ⟶ W₀
c : T₀ ⟶ X₀
hc : F.map c = F.map b ≫ a
dsimp :
  Eq (α := presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    ((hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map b.op :
      presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    ((presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map b.op :
      presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
⊢ Eq (α :=
    (presheaf data G₀).obj (op (F.obj X₀)) ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀) (F.imageSieve a) ⋯)
            { Y := T₀, f := b, hf := ⋯ })))
    ((hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := b, hf := ⋯ })))
    ((presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := b, hf := ⋯ })))

Tactic:
dsimp
-- 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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
p : F.obj W₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac : p ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = a
T₀ : C₀
b : T₀ ⟶ W₀
c : T₀ ⟶ X₀
hc : F.map c = F.map b ≫ a
simp :
  Eq (α := presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    (hom data G₀ X₀ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map c.op :
      presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map b ≫ p) :
      presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
⊢ Eq (α := presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    ((hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map b.op :
      presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    ((presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map b.op :
      presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))

Tactic:
simp only [assoc, IsDenseSubsite.mapPreimage_comp_map, ← hc,
    IsDenseSubsite.mapPreimage_map]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
p : F.obj W₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac : p ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = a
T₀ : C₀
b : T₀ ⟶ W₀
c : T₀ ⟶ X₀
hc : F.map c = F.map b ≫ a
⊢ (F.map b ≫ p) ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = F.map c

Tactic:
simp only [assoc, fac, hc]

Premises used: CategoryTheory.Category.assoc
-- 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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
p : F.obj W₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac : p ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = a
T₀ : C₀
b : T₀ ⟶ W₀
c : T₀ ⟶ X₀
hc : F.map c = F.map b ≫ a
⊢ Eq (α := presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    (hom data G₀ X₀ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map c.op :
      presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map b ≫ p) :
      presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))

Tactic:
exact hom_map data G₀ c _ (by simp only [assoc, fac, hc])

Premises used: 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 : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
⊢ CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (inv data G₀ X₀)
      (presheafObjπ data G₀ (F.obj X₀) i) =
    IsDenseSubsite.mapPreimage J F G₀ (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i)

Tactic:
Multiequalizer.lift_ι _ _ _ _ _

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj, CategoryTheory.Limits.limit, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv, CategoryTheory.Limits.Multiequalizer.lift_ι
-- 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 : F.obj Y₀ ⟶ F.obj X₀
⊢ CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (inv data G₀ X₀) (restriction data G₀ f) =
    IsDenseSubsite.mapPreimage J F G₀ f

Tactic:
Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, IsDenseSubsite.imageSieve_mem J₀ J F f⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, Subtype.mk, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem
-- 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 : F.obj Y₀ ⟶ F.obj X₀
refine :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Y₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Y₀) (F.imageSieve f) ⋯)),
    CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (inv data G₀ X₀) (restriction data G₀ f) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op =
      IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op
⊢ CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (inv data G₀ X₀) (restriction data G₀ f) =
    IsDenseSubsite.mapPreimage J F G₀ f

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, IsDenseSubsite.imageSieve_mem J₀ J F f⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, Subtype.mk, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem
-- 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 : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
⊢ Eq (α :=
    G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Y₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Y₀) (F.imageSieve f) ⋯)
            { Y := W₀, f := a, hf := ⋯ })))
    (CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (inv data G₀ X₀) (restriction data G₀ f) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := a, hf := ⋯ })))
    (IsDenseSubsite.mapPreimage J F G₀ f ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := a, hf := ⋯ })))

Tactic:
Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, J₀.pullback_stable b (cover_lift F J₀ _ (data (F.obj X₀)).mem₀)⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.GrothendieckTopology.pullback_stable, Subtype.mk, CategoryTheory.Functor.OneHypercoverDenseData.mem₀, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.cover_lift, CategoryTheory.Functor.obj
-- 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 : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
refine :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀)
          (Sieve.pullback b
            (Sieve.functorPullback F
              (PreZeroHypercover.sieve₀.{w, v, u}
                (PreOneHypercover.toPreZeroHypercover
                  (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀))))))))
          ⋯)),
    Eq (α := G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
      ((CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (inv data G₀ X₀) (restriction data G₀ f) ≫
          G₀.obj (P := Presheaf.IsSheaf J₀).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := a, hf := ⋯ }))) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
      ((IsDenseSubsite.mapPreimage J F G₀ f ≫
          G₀.obj (P := Presheaf.IsSheaf J₀).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := a, hf := ⋯ }))) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
⊢ Eq (α :=
    G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Y₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Y₀) (F.imageSieve f) ⋯)
            { Y := W₀, f := a, hf := ⋯ })))
    (CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (inv data G₀ X₀) (restriction data G₀ f) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := a, hf := ⋯ })))
    (IsDenseSubsite.mapPreimage J F G₀ f ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := a, hf := ⋯ })))

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, J₀.pullback_stable b (cover_lift F J₀ _ (data (F.obj X₀)).mem₀)⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.GrothendieckTopology.pullback_stable, Subtype.mk, CategoryTheory.Functor.OneHypercoverDenseData.mem₀, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.cover_lift, CategoryTheory.Functor.obj
-- 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 : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
d : F.obj T₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac₂ : d ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = F.map (c ≫ b)
simp :
  CategoryStruct.comp (Y := presheafObj data G₀ (F.obj X₀))
      (inv data G₀ X₀ : G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶ (presheaf data G₀).obj (op (F.obj X₀)))
      (restriction data G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ a).op) =
    IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ a).op
⊢ (CategoryStruct.comp (Y := presheafObj data G₀ (F.obj X₀))
          (inv data G₀ X₀ : G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶ (presheaf data G₀).obj (op (F.obj X₀)))
          (restriction data G₀ f) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map c.op =
    (IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map c.op

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.map_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
X₀ Y₀ : C₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
d : F.obj T₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac₂ : d ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = F.map (c ≫ b)
rw : F.map (c ≫ b) = F.map (c ≫ a) ≫ f
rw₁ : F.map c ≫ F.map b = F.map (c ≫ a) ≫ f
rw₂ : F.map c ≫ F.map b = F.map c ≫ F.map a ≫ f
rw₃ rw₄ : F.map c ≫ F.map a ≫ f = F.map c ≫ F.map a ≫ f
⊢ d ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = F.map (c ≫ a) ≫ f

Tactic:
rw [fac₂, map_comp, map_comp_assoc, fac₁]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_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
X₀ : C₀
i : PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀))) (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))
⊢ 𝟙 (F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)) ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i =
    PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) 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₀ : C₀
⊢ CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (presheafObjObjIso.inv data G₀ X₀)
      (presheafObjObjIso.hom data G₀ X₀) =
    𝟙 (G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀))

Tactic:
Presheaf.IsSheaf.hom_ext G₀.property
      ⟨_, cover_lift F J₀ _ (data (F.obj X₀)).mem₀⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, Subtype.mk, CategoryTheory.Functor.OneHypercoverDenseData.mem₀, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.cover_lift, CategoryTheory.Functor.obj
-- 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₀
refine :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow (X := X₀)
        (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
          (Sieve.functorPullback F
            (PreZeroHypercover.sieve₀.{w, v, u}
              (PreOneHypercover.toPreZeroHypercover
                (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
          ⋯)),
    CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (presheafObjObjIso.inv data G₀ X₀)
          (presheafObjObjIso.hom data G₀ X₀) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op =
      𝟙 (G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀)) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op
⊢ CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (presheafObjObjIso.inv data G₀ X₀)
      (presheafObjObjIso.hom data G₀ X₀) =
    𝟙 (G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀))

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
      ⟨_, cover_lift F J₀ _ (data (F.obj X₀)).mem₀⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, Subtype.mk, CategoryTheory.Functor.OneHypercoverDenseData.mem₀, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.cover_lift, CategoryTheory.Functor.obj
-- 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 :
  PreZeroHypercover.I₀ (S := F.obj X₀)
    (PreOneHypercover.toPreZeroHypercover
      (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))
b :
  F.obj Y₀ ⟶
    PreZeroHypercover.X
      (PreOneHypercover.toPreZeroHypercover
        (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))
      i
fac :
  b ≫
      PreZeroHypercover.f
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))
        i =
    F.map a
dsimp :
  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
⊢ Eq (α :=
    G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
              (Sieve.functorPullback F
                (PreZeroHypercover.sieve₀.{w, v, u}
                  (PreOneHypercover.toPreZeroHypercover
                    (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
              ⋯)
            { Y := Y₀, f := a, hf := ⋯ })))
    (CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (presheafObjObjIso.inv data G₀ X₀)
        (presheafObjObjIso.hom data G₀ X₀) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := a, hf := ⋯ })))
    (𝟙 (G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := a, hf := ⋯ })))

Tactic:
dsimp at i b fac ⊢