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 : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
W₀ : C₀
c : W₀ ⟶ Z₀
hc :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀) ((data X).sieve₁₀ b₁ b₂)
            ⋯) :
        Sieve Z₀).arrows
    c
simp :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (presheafObjπ data G₀ X h₁.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ h₁.q))
    (presheafObjπ data G₀ X h₂.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ h₂.q))
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (((presheafObjπ data G₀ X h₁.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ h₁.q) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map c.op)
    (((presheafObjπ data G₀ X h₂.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ h₂.q) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map c.op)

Tactic:
simp only [assoc, IsDenseSubsite.mapPreimage_comp_map]

Premises used: CategoryTheory.Category.assoc, 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 : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
W₀ : C₀
c : W₀ ⟶ Z₀
hc :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀) ((data X).sieve₁₀ b₁ b₂)
            ⋯) :
        Sieve Z₀).arrows
    c
fac : (F.map c ≫ F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map c ≫ F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (presheafObjπ data G₀ X h₁.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ h₁.q))
    (presheafObjπ data G₀ X h₂.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ h₂.q))

Tactic:
apply presheafObj_mapPreimage_condition

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition
-- 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
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
W₀ : C₀
c : W₀ ⟶ Z₀
hc :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀) ((data X).sieve₁₀ b₁ b₂)
            ⋯) :
        Sieve Z₀).arrows
    c
⊢ (F.map c ≫ F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map c ≫ F.map a ≫ h₂.q) ≫ (data X).f h₂.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
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
rw :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    (restriction.res data G₀ h₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₁.op)
    (restriction.res data G₀ h₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₂.op)
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    (restriction.res data G₀ (X₀ := X₀) (f := f) (g := g₁) (Nonempty.some ⋯) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map p₁.op)
    (restriction.res data G₀ (X₀ := X₀) (f := f) (g := g₂) (Nonempty.some ⋯) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map p₂.op)

Tactic:
rw [restriction.res_eq_res data G₀ _ h₁, restriction.res_eq_res data G₀ _ h₂]

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.res_eq_res
-- 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
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    (restriction.res data G₀ h₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₁.op)
    (restriction.res data G₀ h₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₂.op)

Tactic:
Presheaf.IsSheaf.hom_ext G₀.property
        ⟨_, J₀.intersection_covering
          (IsDenseSubsite.imageSieve_mem J₀ J F (F.map p₁ ≫ h₁.q))
          (IsDenseSubsite.imageSieve_mem J₀ J F (F.map p₂ ≫ h₂.q))⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.q, CategoryTheory.Functor.map, Subtype.mk, CategoryTheory.GrothendieckTopology.intersection_covering, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.CategoryStruct.comp, 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 : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
refine :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} T₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) T₀)
          (F.imageSieve (F.map p₁ ≫ h₁.q) ⊓ F.imageSieve (F.map p₂ ≫ h₂.q)) ⋯)),
    Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
      ((restriction.res data G₀ h₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₁.op) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
      ((restriction.res data G₀ h₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₂.op) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    (restriction.res data G₀ h₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₁.op)
    (restriction.res data G₀ h₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₂.op)

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
        ⟨_, J₀.intersection_covering
          (IsDenseSubsite.imageSieve_mem J₀ J F (F.map p₁ ≫ h₁.q))
          (IsDenseSubsite.imageSieve_mem J₀ J F (F.map p₂ ≫ h₂.q))⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.q, CategoryTheory.Functor.map, Subtype.mk, CategoryTheory.GrothendieckTopology.intersection_covering, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.CategoryStruct.comp, 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 : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
W₀ : C₀
a : W₀ ⟶ T₀
q₁ : W₀ ⟶ (data X).X h₁.i₀
w₁ : F.map q₁ = F.map a ≫ F.map p₁ ≫ h₁.q
q₂ : W₀ ⟶ (data X).X h₂.i₀
w₂ : F.map q₂ = F.map a ≫ F.map p₂ ≫ h₂.q
⊢ F.map q₁ ≫ (data X).f h₁.i₀ = F.map q₂ ≫ (data X).f h₂.i₀

Tactic:
simp only [w₁, w₂, assoc, h₁.fac, h₂.fac, ← Functor.map_comp_assoc, w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac, CategoryTheory.Functor.map_comp_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 : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
W₀ : C₀
a : W₀ ⟶ T₀
q₁ : W₀ ⟶ (data X).X h₁.i₀
w₁ : F.map q₁ = F.map a ≫ F.map p₁ ≫ h₁.q
q₂ : W₀ ⟶ (data X).X h₂.i₀
w₂ : F.map q₂ = F.map a ≫ F.map p₂ ≫ h₂.q
refine :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀) ((data X).sieve₁₀ q₁ q₂)
          ⋯)),
    Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
      (((restriction.res data G₀ h₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₁.op) ≫
          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)
      (((restriction.res data G₀ h₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₂.op) ≫
          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 (α :=
    presheafObj data G₀ X ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} T₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) T₀)
              (F.imageSieve (F.map p₁ ≫ h₁.q) ⊓ F.imageSieve (F.map p₂ ≫ h₂.q)) ⋯)
            { Y := W₀, f := a, hf := ⋯ })))
    ((restriction.res data G₀ h₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₁.op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := a, hf := ⋯ })))
    ((restriction.res data G₀ h₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₂.op) ≫
      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
        ⟨_, (data X).mem₁₀ h₁.i₀ h₂.i₀ q₁ q₂ (by
        simp only [w₁, w₂, assoc, h₁.fac, h₂.fac, ← Functor.map_comp_assoc, w])⟩ _ _ ?_

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.i₀, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.OneHypercoverDenseData.mem₁₀, Subtype.mk, CategoryTheory.Presheaf.IsSheaf.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
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
W₀ : C₀
a : W₀ ⟶ T₀
q₁ : W₀ ⟶ (data X).X h₁.i₀
w₁ : F.map q₁ = F.map a ≫ F.map p₁ ≫ h₁.q
q₂ : W₀ ⟶ (data X).X h₂.i₀
w₂ : F.map q₂ = F.map a ≫ F.map p₂ ≫ h₂.q
U₀ : C₀
b : U₀ ⟶ W₀
hb :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀) ((data X).sieve₁₀ q₁ q₂)
            ⋯) :
        Sieve W₀).arrows
    b
dsimp :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (((restriction.res data G₀ h₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₁.op) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map b.op)
    (((restriction.res data G₀ h₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₂.op) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map b.op)
⊢ Eq (α :=
    presheafObj data G₀ X ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          { Y := U₀, f := b, hf := hb :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀)
                  ((data X).sieve₁₀ q₁ q₂) ⋯) }.Y))
    (((restriction.res data G₀ h₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₁.op) ≫
        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
        { Y := U₀, f := b, hf := hb :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀)
                  ((data X).sieve₁₀ q₁ q₂) ⋯) }.f.op)
    (((restriction.res data G₀ h₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₂.op) ≫
        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
        { Y := U₀, f := b, hf := hb :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀)
                  ((data X).sieve₁₀ q₁ q₂) ⋯) }.f.op)

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 : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
W₀ : C₀
a : W₀ ⟶ T₀
q₁ : W₀ ⟶ (data X).X h₁.i₀
w₁ : F.map q₁ = F.map a ≫ F.map p₁ ≫ h₁.q
q₂ : W₀ ⟶ (data X).X h₂.i₀
w₂ : F.map q₂ = F.map a ≫ F.map p₂ ≫ h₂.q
U₀ : C₀
b : U₀ ⟶ W₀
hb :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀) ((data X).sieve₁₀ q₁ q₂)
            ⋯) :
        Sieve W₀).arrows
    b
simp :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (presheafObjπ data G₀ X h₁.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map b ≫ F.map a ≫ F.map p₁ ≫ h₁.q))
    (presheafObjπ data G₀ X h₂.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map b ≫ F.map a ≫ F.map p₂ ≫ h₂.q))
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (((restriction.res data G₀ h₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₁.op) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map b.op)
    (((restriction.res data G₀ h₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map p₂.op) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map b.op)

Tactic:
simp only [assoc, restriction.res, IsDenseSubsite.mapPreimage_comp_map]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.res
-- 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
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
W₀ : C₀
a : W₀ ⟶ T₀
q₁ : W₀ ⟶ (data X).X h₁.i₀
w₁ : F.map q₁ = F.map a ≫ F.map p₁ ≫ h₁.q
q₂ : W₀ ⟶ (data X).X h₂.i₀
w₂ : F.map q₂ = F.map a ≫ F.map p₂ ≫ h₂.q
U₀ : C₀
b : U₀ ⟶ W₀
hb :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀) ((data X).sieve₁₀ q₁ q₂)
            ⋯) :
        Sieve W₀).arrows
    b
fac :
  (F.map b ≫ F.map a ≫ F.map p₁ ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map b ≫ F.map a ≫ F.map p₂ ≫ h₂.q) ≫ (data X).f h₂.i₀
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (presheafObjπ data G₀ X h₁.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map b ≫ F.map a ≫ F.map p₁ ≫ h₁.q))
    (presheafObjπ data G₀ X h₂.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map b ≫ F.map a ≫ F.map p₂ ≫ h₂.q))

Tactic:
apply presheafObj_mapPreimage_condition

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition
-- 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
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
W₀ : C₀
a : W₀ ⟶ T₀
q₁ : W₀ ⟶ (data X).X h₁.i₀
w₁ : F.map q₁ = F.map a ≫ F.map p₁ ≫ h₁.q
q₂ : W₀ ⟶ (data X).X h₂.i₀
w₂ : F.map q₂ = F.map a ≫ F.map p₂ ≫ h₂.q
U₀ : C₀
b : U₀ ⟶ W₀
hb :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀) ((data X).sieve₁₀ q₁ q₂)
            ⋯) :
        Sieve W₀).arrows
    b
⊢ (F.map b ≫ F.map a ≫ F.map p₁ ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map b ≫ F.map a ≫ F.map p₂ ≫ h₂.q) ≫ (data X).f h₂.i₀

Tactic:
simp only [assoc, h₁.fac, h₂.fac, ← Functor.map_comp_assoc, w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac, CategoryTheory.Functor.map_comp_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 : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
⊢ ((data X).sieve f).arrows g

Tactic:
have hg : (data X).sieve f g := ⟨i, p, 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
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
hg : ((data X).sieve f).arrows g
dsimp :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op Y₀))
    (⋯.amalgamate
        (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀) ((data X).sieve f) ⋯)
        (fun
            (x :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
                  ((data X).sieve f) ⋯)) ↦
          (restriction.res data G₀ (Nonempty.some ⋯) :
            presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op x.Y)))
        ⋯ ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map g.op)
    (presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ p)
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op Y₀))
    (restriction data G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map g.op)
    (presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ p)

Tactic:
dsimp only [restriction]

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction