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₀ : 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
rw :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op Y₀))
    (restriction.res data G₀ (X₀ := X₀) (f := f) (g := GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := g, hf := hg })
      (Nonempty.some ⋯))
    (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₀))
    (⋯.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)

Tactic:
rw [G₀.2.amalgamate_map _ _ _ ⟨_, g, hg⟩]

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.GrothendieckTopology.Cover.Arrow.mk
-- 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
fac₁ :
  CategoryStruct.comp (Y :=
      F.obj
        ((data X).X
          (SieveStruct.i₀ (X₀ := X₀) (f := f) (Y₀ :=
            GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
              Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀) ((data X).sieve f)
                ⋯)
              { Y := Y₀, f := g, hf := hg })
            (g := GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := g, hf := hg }) (Nonempty.some ⋯))))
      (SieveStruct.q (Nonempty.some ⋯))
      ((data X).f
        (SieveStruct.i₀ (X₀ := X₀) (f := f) (Y₀ :=
          GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀) ((data X).sieve f) ⋯)
            { Y := Y₀, f := g, hf := hg })
          (g := GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := g, hf := hg }) (Nonempty.some ⋯))) =
    p ≫ (data X).f i
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op Y₀))
    (restriction.res data G₀ (X₀ := X₀) (f := f) (g := GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := g, hf := hg })
      (Nonempty.some ⋯))
    (presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ p)

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
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
fac₁ : F.map g ≫ f = p ≫ (data X).f i
fac₂ fac₃ : F.map g ≫ f = F.map g ≫ f
⊢ CategoryStruct.comp (Y :=
      F.obj
        ((data X).X
          (SieveStruct.i₀ (X₀ := X₀) (f := f) (Y₀ :=
            GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
              Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀) ((data X).sieve f)
                ⋯)
              { Y := Y₀, f := g, hf := hg })
            (g := GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := g, hf := hg }) (Nonempty.some ⋯))))
      (SieveStruct.q (Nonempty.some ⋯))
      ((data X).f
        (SieveStruct.i₀ (X₀ := X₀) (f := f) (Y₀ :=
          GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀) ((data X).sieve f) ⋯)
            { Y := Y₀, f := g, hf := hg })
          (g := GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := g, hf := hg }) (Nonempty.some ⋯))) =
    p ≫ (data X).f i

Tactic:
rw [hg.some.fac, fac]

Premises used: Nonempty.some, CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.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
i : (data X).I₀
p : F.obj X₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = f
⊢ p ≫ (data X).f i = F.map (𝟙 X₀) ≫ f

Tactic:
simpa using 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
i : (data X).I₀
p : F.obj X₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = f
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀)) (restriction data G₀ f)
    (presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ p)

Tactic:
simpa using restriction_map data G₀ f (𝟙 _) p (by simpa using fac)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_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 Y : C
f : X ⟶ Y
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
⊢ ∃ (a : F.obj ((data X).Y j) ⟶ Y),
    a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f ∧ a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f

Tactic:
⟨_, rfl, (data X).w_assoc j _⟩

Premises used: CategoryTheory.Functor.PreOneHypercoverDenseData.w_assoc, And.intro, Exists.intro, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData, rfl
-- 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
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
⊢ Eq (α :=
    presheafObj data G₀ Y ⟶
      ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).right
        (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j))
    ((fun (i₀ : (data X).multicospanShape.L) ↦
          (restriction data G₀ ((data X).f i₀ ≫ f) :
            presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i₀))))
        ((data X).multicospanShape.fst
          (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j)) ≫
      ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).fst
        (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j))
    ((fun (i₀ : (data X).multicospanShape.L) ↦
          (restriction data G₀ ((data X).f i₀ ≫ f) :
            presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i₀))))
        ((data X).multicospanShape.snd
          (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j)) ≫
      ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).snd
        (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j))

Tactic:
Presheaf.IsSheaf.hom_ext G₀.property
      ⟨_, cover_lift F J₀ _ (J.pullback_stable a (data Y).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
-- 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_1 : C
f : X ⟶ Y_1
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y_1
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y_1).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y_1).toPreOneHypercover.X i
fac : p ≫ (data Y_1).f i = F.map b ≫ a
simp :
  Eq (α := presheafObj data G₀ Y_1 ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (restriction data G₀ ((data X).f i₁ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (b ≫ (data X).p₁ j).op)
    (restriction data G₀ ((data X).f i₂ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (b ≫ (data X).p₂ j).op)
⊢ Eq (α := presheafObj data G₀ Y_1 ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    ((restriction data G₀ ((data X).f i₁ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map ((data X).p₁ j).op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map b.op)
    ((restriction data G₀ ((data X).f i₂ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map ((data X).p₂ j).op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map b.op)

Tactic:
simp only [assoc, ← 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_1 : C
f : X ⟶ Y_1
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y_1
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y_1).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y_1).toPreOneHypercover.X i
fac : p ≫ (data Y_1).f i = F.map b ≫ a
fac₁ : p ≫ (data Y_1).f i = F.map (b ≫ (data X).p₂ j) ≫ (data X).f i₂ ≫ f
fac₂ : p ≫ (data Y_1).f i = F.map (b ≫ (data X).p₁ j) ≫ (data X).f i₁ ≫ f
⊢ Eq (α := presheafObj data G₀ Y_1 ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (restriction data G₀ ((data X).f i₁ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (b ≫ (data X).p₁ j).op)
    (restriction data G₀ ((data X).f i₂ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (b ≫ (data X).p₂ j).op)

Tactic:
rw [restriction_map (p := p), restriction_map (p := p)]

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_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 Y_1 : C
f : X ⟶ Y_1
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y_1
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y_1).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y_1).toPreOneHypercover.X i
fac : p ≫ (data Y_1).f i = F.map b ≫ a
⊢ p ≫ (data Y_1).f i = F.map (b ≫ (data X).p₂ j) ≫ (data X).f i₂ ≫ f

Tactic:
simp_all
-- 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_1 : C
f : X ⟶ Y_1
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y_1
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y_1).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y_1).toPreOneHypercover.X i
fac : p ≫ (data Y_1).f i = F.map b ≫ a
⊢ p ≫ (data Y_1).f i = F.map (b ≫ (data X).p₁ j) ≫ (data X).f i₁ ≫ f

Tactic:
simp_all
-- 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
i : (data X).I₀
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafMap data G₀ f ≫ presheafObjπ data G₀ X i) (restriction data G₀ ((data X).f i ≫ f))

Tactic:
Multiequalizer.lift_ι _ _ _ _ _

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap, 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
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀))
    (presheafMap data G₀ g ≫ restriction data G₀ f) (restriction data G₀ (f ≫ g))

Tactic:
Presheaf.IsSheaf.hom_ext G₀.property ⟨_, GrothendieckTopology.bind_covering
    (hS := cover_lift F J₀ J (J.pullback_stable f (data X).mem₀)) (hR := fun Y₀ a ha ↦
      cover_lift F J₀ J (J.pullback_stable
        (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g) (data Y).mem₀))⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Sieve.ofArrows.h, Subtype.mk, CategoryTheory.Functor.OneHypercoverDenseData.mem₀, CategoryTheory.GrothendieckTopology.bind_covering, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.PreOneHypercoverDenseData.f, CategoryTheory.Sieve.ofArrows.i, CategoryTheory.Functor.cover_lift, 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 Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
refine :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
          (Sieve.bind
            (Sieve.functorPullback F
                (Sieve.pullback f
                  (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
            fun (Y₀ : C₀) (a : Y₀ ⟶ X₀)
              (ha :
                (Sieve.functorPullback F
                      (Sieve.pullback f
                        (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
                  a) ↦
            Sieve.functorPullback F
              (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
                (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)))
          ⋯)),
    Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
      ((presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
      (restriction data G₀ (f ≫ g) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀))
    (presheafMap data G₀ g ≫ restriction data G₀ f) (restriction data G₀ (f ≫ g))

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property ⟨_, GrothendieckTopology.bind_covering
    (hS := cover_lift F J₀ J (J.pullback_stable f (data X).mem₀)) (hR := fun Y₀ a ha ↦
      cover_lift F J₀ J (J.pullback_stable
        (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g) (data Y).mem₀))⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Sieve.ofArrows.h, Subtype.mk, CategoryTheory.Functor.OneHypercoverDenseData.mem₀, CategoryTheory.GrothendieckTopology.bind_covering, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.PreOneHypercoverDenseData.f, CategoryTheory.Sieve.ofArrows.i, CategoryTheory.Functor.cover_lift, 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 Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd :
  (Sieve.functorPullback F
        (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
    d
hc :
  Sieve.arrows
    ((fun (Y₀ : C₀) (a : Y₀ ⟶ X₀)
          (ha :
            (Sieve.functorPullback F
                  (Sieve.pullback f
                    (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
              a) ↦
        Sieve.functorPullback F
          (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
            (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)))
      Y₀ d hd)
    c
⊢ Sieve.ofArrows.h hc ≫ (data Y).toPreOneHypercover.f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g

Tactic:
have hc' := Sieve.ofArrows.fac hc
-- 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
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd :
  (Sieve.functorPullback F
        (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
    d
hc :
  Sieve.arrows
    ((fun (Y₀ : C₀) (a : Y₀ ⟶ X₀)
          (ha :
            (Sieve.functorPullback F
                  (Sieve.pullback f
                    (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
              a) ↦
        Sieve.functorPullback F
          (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
            (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)))
      Y₀ d hd)
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).toPreOneHypercover.f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
⊢ Sieve.ofArrows.h hd ≫ (data X).toPreOneHypercover.f (Sieve.ofArrows.i hd) = F.map d ≫ f

Tactic:
have hd' := Sieve.ofArrows.fac hd