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
G₀_1 : Sheaf.{v₀, v', u₀, u'} J₀ A
simp : F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map c ≫ F.map d ≫ f
⊢ (F.map c ≫ Sieve.ofArrows.h hd) ≫ (data X).f (Sieve.ofArrows.i hd) = F.map (c ≫ d) ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y : C
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
G₀_1 : Sheaf.{v₀, v', u₀, u'} J₀ A
⊢ F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map c ≫ F.map d ≫ f

Tactic:
grind
-- 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
G₀_1 : Sheaf.{v₀, v', u₀, u'} J₀ A
simp : Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) = F.map c ≫ F.map d ≫ f ≫ g
⊢ Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) = F.map (c ≫ d) ≫ f ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y : C
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
G₀_1 : Sheaf.{v₀, v', u₀, u'} J₀ A
⊢ Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) = F.map c ≫ F.map d ≫ f ≫ g

Tactic:
grind
-- 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
rw :
  Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc))
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    ((presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (d.op ≫ c.op))
    (restriction data G₀ (f ≫ g) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (d.op ≫ c.op))

Tactic:
rw [assoc, ← op_comp, restriction_map (i := Sieve.ofArrows.i hd)
    (p := F.map c ≫ Sieve.ofArrows.h hd) (fac := by simp; grind),
    restriction_map (i := Sieve.ofArrows.i hc) (p := Sieve.ofArrows.h hc) (fac := by simp; grind),
    presheafMap_π_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π_assoc, CategoryTheory.Sieve.ofArrows.h, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, 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
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
dsimp :
  Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc))
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc))

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 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
⊢ F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈
    (J₀ : (a : C₀) → Set (Sieve a)) U₀

Tactic:
have := J₀.intersection_covering (IsDenseSubsite.imageSieve_mem J₀ J F (Sieve.ofArrows.h hc))
    (J₀.pullback_stable c (IsDenseSubsite.imageSieve_mem J₀ J F (Sieve.ofArrows.h hd)))
-- 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₀
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc))

Tactic:
Presheaf.IsSheaf.hom_ext G₀.property ⟨_, this⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, 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 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₀
refine :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} U₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) U₀)
          (F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd))) this)),
    Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
      ((restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
          IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd)) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
      ((presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc))

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property ⟨_, this⟩ _ _ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, 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 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
dsimp :
  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) ≫
        IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map a.op)
    ((presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map a.op)
⊢ Eq (α :=
    presheafObj data G₀ Y ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} U₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) U₀)
              (F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd))) this)
            { Y := V₀, f := a, hf := ⋯ })))
    ((restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
        IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := V₀, f := a, hf := ⋯ })))
    ((presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := V₀, f := a, 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 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
⊢ F.map a ≫ F.map c ≫ Sieve.ofArrows.h hd = F.map x₂

Tactic:
simpa using fac₂.symm

Premises used: Eq.symm
-- 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₀))
    (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)
⊢ 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) ≫
        IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map a.op)
    ((presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map a.op)

Tactic:
rw [assoc, assoc,
    IsDenseSubsite.mapPreimage_map_of_fac J F G₀ _ _ x₂ (by simpa using fac₂.symm),
    IsDenseSubsite.mapPreimage_map_of_fac J F G₀ _ _ x₁ fac₁.symm]

Premises used: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_fac, CategoryTheory.Category.assoc, Eq.symm
-- 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
⊢ F.map x₁ ≫ (data Y).f (Sieve.ofArrows.i hc) = F.map x₂ ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g

Tactic:
simp_all