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
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd :
  Presieve.functorPullback F
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover)).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
this :
  F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈
    (J₀ : (a : C₀) → Set (Sieve a)) U₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
rw :
  Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op V₀))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map x₁))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₁.op)
rw₁ rw₂ :
  Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op V₀))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₁.op)
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₁.op)
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op V₀))
    (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₂.op)
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₁.op)

Tactic:
rw [restriction_map data G₀ _ _ (F.map x₁) (by simp_all), IsDenseSubsite.mapPreimage_map]

Premises used: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map, CategoryTheory.Functor.map, 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 : C
h :
  ∀ (i : (data X).I₀),
    presheafMap data G₀ (𝟙 X) ≫ presheafObjπ data G₀ X i = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
⊢ presheafMap data G₀ (𝟙 X) = 𝟙 (presheafObj data G₀ X)

Tactic:
ext 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).I₀
⊢ 𝟙 (F.obj ((data X).X i)) ≫ (data X).f i = (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 : C
i : (data X).I₀
h : restriction data G₀ ((data X).f i ≫ 𝟙 X) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
h₁ : restriction data G₀ ((data X).f i) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
h₂ :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (restriction data G₀ ((data X).f i)) (presheafObjπ data G₀ X i)
h₃ :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ (𝟙 (F.obj ((data X).X i)))) (presheafObjπ data G₀ X i)
h₄ :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafObjπ data G₀ X i ≫ 𝟙 (G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i))))
    (presheafObjπ data G₀ X i)
h₅ h₆ :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i))) (presheafObjπ data G₀ X i)
    (presheafObjπ data G₀ X i)
⊢ presheafMap data G₀ (𝟙 X) ≫ presheafObjπ data G₀ X i = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i

Tactic:
rw [presheafMap_π, comp_id, id_comp,
    restriction_eq_of_fac data G₀ ((data X).f i) (𝟙 _) (by simp),
    IsDenseSubsite.mapPreimage_id, comp_id]

Premises used: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_id, CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.PreOneHypercoverDenseData.f, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_eq_of_fac, CategoryTheory.Category.id_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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (i : (data X).I₀),
    Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
      (presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i)
      ((presheafMap data G₀ g ≫ presheafMap data G₀ f) ≫ presheafObjπ data G₀ X i)
⊢ Eq (α := presheafObj data G₀ Z ⟶ presheafObj data G₀ X) (presheafMap data G₀ (f ≫ g))
    (presheafMap data G₀ g ≫ presheafMap data G₀ f)

Tactic:
ext 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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
i : (data X).I₀
h :
  Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i)
    (presheafMap data G₀ g ≫ presheafMap data G₀ f ≫ presheafObjπ data G₀ X i)
h₁ :
  Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (restriction data G₀ ((data X).f i ≫ f ≫ g))
    (presheafMap data G₀ g ≫ presheafMap data G₀ f ≫ presheafObjπ data G₀ X i)
h₂ :
  Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (restriction data G₀ ((data X).f i ≫ f ≫ g)) (presheafMap data G₀ g ≫ restriction data G₀ ((data X).f i ≫ f))
h₃ :
  Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (restriction data G₀ ((data X).f i ≫ f ≫ g)) (restriction data G₀ (((data X).f i ≫ f) ≫ g))
h₄ h₅ :
  Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (restriction data G₀ ((data X).f i ≫ f ≫ g)) (restriction data G₀ ((data X).f i ≫ f ≫ g))
⊢ Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i)
    ((presheafMap data G₀ g ≫ presheafMap data G₀ f) ≫ presheafObjπ data G₀ X i)

Tactic:
rw [assoc, presheafMap_π, presheafMap_π, presheafMap_restriction, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_restriction, 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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha :
  Sieve.arrows
    (↑(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₀)))))))
          ⋯) :
      Sieve X₀)
    a
T₀ : C₀
b : T₀ ⟶ X₀
hb :
  Sieve.arrows
    (↑(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₀)))))))
          ⋯) :
      Sieve X₀)
    b
U₀ : C₀
p₁ :
  U₀ ⟶
    { Y := W₀, f := a, hf := ha :
        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₀)))))))
            ⋯) }.Y
p₂ :
  U₀ ⟶
    { Y := T₀, f := b, hf := hb :
        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₀)))))))
            ⋯) }.Y
fac :
  p₁ ≫
      { Y := W₀, f := a, hf := ha :
          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₀)))))))
              ⋯) }.f =
    p₂ ≫ { Y := T₀, f := b, hf := hb }.f
⊢ Sieve.ofArrows.h ha ≫
      PreZeroHypercover.f
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))
        (Sieve.ofArrows.i ha) =
    F.map a

Tactic:
have ha' := Sieve.ofArrows.fac ha
-- 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 : W₀ ⟶ X₀
ha :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a
T₀ : C₀
b : T₀ ⟶ X₀
hb :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' :
  Sieve.ofArrows.h ha ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map a
hb' :
  Sieve.ofArrows.h hb ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map b
rw :
  F.map p₁ ≫
      Sieve.ofArrows.h ha ≫
        PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map (p₁ ≫ a)
rw₁ : F.map p₁ ≫ F.map a = F.map (p₁ ≫ a)
rw₂ rw₃ : F.map p₁ ≫ F.map a = F.map p₁ ≫ F.map a
⊢ (F.map p₁ ≫ Sieve.ofArrows.h ha) ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map (p₁ ≫ a)

Tactic:
rw [assoc, ha', map_comp]

Premises used: CategoryTheory.Category.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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a
T₀ : C₀
b : T₀ ⟶ X₀
hb :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' :
  Sieve.ofArrows.h ha ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map a
hb' :
  Sieve.ofArrows.h hb ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map b
rw :
  F.map p₂ ≫
      Sieve.ofArrows.h hb ≫
        PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map (p₁ ≫ a)
rw₁ : F.map p₂ ≫ F.map b = F.map (p₁ ≫ a)
rw₂ : F.map p₂ ≫ F.map b = F.map (p₂ ≫ b)
rw₃ rw₄ : F.map p₂ ≫ F.map b = F.map p₂ ≫ F.map b
⊢ (F.map p₂ ≫ Sieve.ofArrows.h hb) ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map (p₁ ≫ a)

Tactic:
rw [assoc, hb', fac, map_comp]

Premises used: CategoryTheory.Category.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₀ W₀ : C₀
a : W₀ ⟶ 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 = F.map a
⊢ Sieve.arrows
    (Sieve.functorPullback F
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a

Tactic:
have ha : Sieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀ a :=
    ⟨_, p, _, ⟨i⟩, 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₀ W₀ : C₀
a : W₀ ⟶ 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 = F.map a
ha :
  Sieve.arrows
    (Sieve.functorPullback F
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a
⊢ Eq (α := (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (hom data G₀ X₀ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map a.op)
    (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p)

Tactic:
(G₀.2.amalgamate_map _ _ _ ⟨W₀, a, ha⟩).trans
    (presheafObj_mapPreimage_condition _ _ _ _ _ _ _
      ((Sieve.ofArrows.fac ha).trans fac.symm))

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map, CategoryTheory.Sieve.ofArrows.fac, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.GrothendieckTopology.Cover.Arrow.mk, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom, Eq.symm, Eq.trans
-- 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 : W₀ ⟶ 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 = F.map a
ha :
  Sieve.arrows
    (Sieve.functorPullback F
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a
⊢ Eq (α := (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (hom data G₀ X₀ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map a.op)
    (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p)

Tactic:
exact (G₀.2.amalgamate_map _ _ _ ⟨W₀, a, ha⟩).trans
    (presheafObj_mapPreimage_condition _ _ _ _ _ _ _
      ((Sieve.ofArrows.fac ha).trans fac.symm))

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.GrothendieckTopology.Cover.Arrow.mk, Eq.trans
-- 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
⊢ Eq (α := (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a)
    (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p)

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

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

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

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, Subtype.mk, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem