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.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
refine :
  (Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))) →
    ∀ (hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G))
      (hG : ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))), Presheaf.IsSheaf J G
⊢ Presheaf.IsSheaf J G ↔
    Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))

Tactic:
refine ⟨fun hG ↦ ⟨op_comp_isSheaf F J₀ J ⟨_, hG⟩,
    fun X ↦ ⟨(data X).toOneHypercover.isLimitMultifork ⟨G, hG⟩⟩⟩, fun ⟨hG₀, hG⟩ ↦ ?_⟩
-- 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.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
h : Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
rw : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork G))
⊢ Presheaf.IsSheaf J G

Tactic:
rw [Presheaf.isSheaf_iff_multifork]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_multifork
-- 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.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
h : Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
replace :
  ∀ (hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)) (X : C) (S : J.Cover X),
    Nonempty (IsLimit (S.multifork G))
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork G))

Tactic:
replace hG := fun X ↦ (hG X).some
-- 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.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
h : Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork G))

Tactic:
fun X S ↦ ⟨isSheaf_iff.isLimit hG₀ hG S⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.isLimit
-- 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.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
h : Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork G))

Tactic:
exact fun X S ↦ ⟨isSheaf_iff.isLimit hG₀ hG S⟩
-- 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
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_3 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
Z : A
f g : Z ⟶ presheafObj data G₀ X
h : ∀ (i : (data X).I₀), f ≫ presheafObjπ data G₀ X i = g ≫ presheafObjπ data G₀ X i
⊢ f = g

Tactic:
Multiequalizer.hom_ext _ _ _ h

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj, CategoryTheory.Limits.Multiequalizer.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
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_3 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
i i' : (data X).I₀
j : (data X).I₁ i i'
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).Y j)))
    (presheafObjπ data G₀ X i ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map ((data X).p₁ j).op)
    (presheafObjπ data G₀ X i' ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map ((data X).p₂ j).op)

Tactic:
Multiequalizer.condition ((data X).multicospanIndex G₀.obj) ⟨⟨i, i'⟩, j⟩

Premises used: CategoryTheory.Limits.Multiequalizer.condition, CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj, Prod.mk, CategoryTheory.ObjectProperty.FullSubcategory.obj, Sigma.mk, 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 : C
i₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op Y₀))
    (presheafObjπ data G₀ X i₁ ≫ IsDenseSubsite.mapPreimage J F G₀ p₁)
    (presheafObjπ data G₀ X i₂ ≫ IsDenseSubsite.mapPreimage J F G₀ p₂)

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

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

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

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, Subtype.mk, CategoryTheory.GrothendieckTopology.intersection_covering, 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 : C
i₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
W₀ : C₀
a : W₀ ⟶ Y₀
b₁ : W₀ ⟶ (data X).X i₁
h₁ : F.map b₁ = F.map a ≫ p₁
b₂ : W₀ ⟶ (data X).X i₂
h₂ : F.map b₂ = F.map a ≫ p₂
⊢ F.map b₁ ≫ (data X).f i₁ = F.map b₂ ≫ (data X).f i₂

Tactic:
simp only [h₁, h₂, assoc, fac]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
i₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
W₀ : C₀
a : W₀ ⟶ Y₀
b₁ : W₀ ⟶ (data X).X i₁
h₁ : F.map b₁ = F.map a ≫ p₁
b₂ : W₀ ⟶ (data X).X i₂
h₂ : F.map b₂ = F.map a ≫ p₂
U₀ : C₀
c : U₀ ⟶ W₀
j : (data X).I₁ i₁ i₂
t : U₀ ⟶ (data X).Y j
fac₁ : c ≫ b₁ = t ≫ (data X).p₁ j
fac₂ : c ≫ b₂ = t ≫ (data X).p₂ j
⊢ F.map (c ≫ a) ≫ p₁ = F.map (c ≫ b₁)

Tactic:
simp [← h₁]
-- 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₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
W₀ : C₀
a : W₀ ⟶ Y₀
b₁ : W₀ ⟶ (data X).X i₁
h₁ : F.map b₁ = F.map a ≫ p₁
b₂ : W₀ ⟶ (data X).X i₂
h₂ : F.map b₂ = F.map a ≫ p₂
U₀ : C₀
c : U₀ ⟶ W₀
j : (data X).I₁ i₁ i₂
t : U₀ ⟶ (data X).Y j
fac₁ : c ≫ b₁ = t ≫ (data X).p₁ j
fac₂ : c ≫ b₂ = t ≫ (data X).p₂ j
⊢ F.map (c ≫ a) ≫ p₂ = F.map (c ≫ b₂)

Tactic:
simp [← h₂]
-- 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₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
W₀ : C₀
a : W₀ ⟶ Y₀
b₁ : W₀ ⟶ (data X).X i₁
h₁ : F.map b₁ = F.map a ≫ p₁
b₂ : W₀ ⟶ (data X).X i₂
h₂ : F.map b₂ = F.map a ≫ p₂
U₀ : C₀
c : U₀ ⟶ W₀
j : (data X).I₁ i₁ i₂
t : U₀ ⟶ (data X).Y j
fac₁ : c ≫ b₁ = t ≫ (data X).p₁ j
fac₂ : c ≫ b₂ = t ≫ (data X).p₂ j
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (presheafObjπ data G₀ X i₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ b₁).op)
    (presheafObjπ data G₀ X i₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ b₂).op)

Tactic:
simpa [fac₁, fac₂] using presheafObj_condition_assoc _ _ _ _ _ _ _

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

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

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

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

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.q, Subtype.mk, CategoryTheory.GrothendieckTopology.intersection_covering, 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 : 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
rw : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
rw₁ : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
rw₂ : F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
rw₃ : F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = F.map a ≫ h₂.q ≫ (data X).f h₂.i₀
rw₄ : F.map a ≫ F.map g ≫ f = F.map a ≫ h₂.q ≫ (data X).f h₂.i₀
rw₅ rw₆ : F.map a ≫ F.map g ≫ f = F.map a ≫ F.map g ≫ f
⊢ F.map b₁ ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀

Tactic:
rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.fac]

Premises used: CategoryTheory.Category.assoc, 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₀ 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
refine :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀) ((data X).sieve₁₀ b₁ b₂)
          ⋯)),
    Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
      ((res data G₀ h₁ ≫
          G₀.obj (P := Presheaf.IsSheaf J₀).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, f := a, hf := ⋯ }))) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
      ((res data G₀ h₂ ≫
          G₀.obj (P := Presheaf.IsSheaf J₀).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, 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₀} Y₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Y₀)
              (F.imageSieve h₁.q ⊓ F.imageSieve h₂.q) ⋯)
            { Y := Z₀, f := a, hf := ⋯ })))
    (res data G₀ h₁ ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, f := a, hf := ⋯ })))
    (res data G₀ h₂ ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, f := a, hf := ⋯ })))

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, (data X).mem₁₀ h₁.i₀ h₂.i₀ b₁ b₂ (by rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.fac])⟩ _ _ ?_

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₀ 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
dsimp :
  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)
⊢ Eq (α :=
    presheafObj data G₀ X ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          { Y := W₀, f := c, hf := hc :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀)
                  ((data X).sieve₁₀ b₁ b₂) ⋯) }.Y))
    ((res data G₀ h₁ ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map
          (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, f := a, hf := ⋯ }))) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        { Y := W₀, f := c, hf := hc :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀)
                  ((data X).sieve₁₀ b₁ b₂) ⋯) }.f.op)
    ((res data G₀ h₂ ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map
          (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, f := a, hf := ⋯ }))) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        { Y := W₀, f := c, hf := hc :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀)
                  ((data X).sieve₁₀ b₁ b₂) ⋯) }.f.op)

Tactic:
dsimp [res]

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