awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
hs :
  ∀ {X : C} (i : I) (f : X ⟶ Y i),
    s X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
        (x i)
hs' :
  ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
        (s X) =
      s W
hex : (fun (X : Cᵒᵖ) ↦ s (Opposite.unop X)) ∈ F.sections
⊢ ∃ (x_1 : (↑F.sections : Type (max u w))), ∀ (i : I), (↑x_1 : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i

Tactic:
refine ⟨⟨fun X => s X.unop, ?_⟩, fun i => (hs i (𝟙 (Y i))).trans (by simp)⟩
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
hs :
  ∀ {X : C} (i : I) (f : X ⟶ Y i),
    s X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
        (x i)
hs' :
  ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
        (s X) =
      s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
hex :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
      (s Y₁) =
    s Y₂
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Opposite.op f)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
        ((fun (X : Cᵒᵖ) ↦ (s (Opposite.unop X) : F.obj (Opposite.op (Opposite.unop X)))) (Opposite.op Y₁)) :
      (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
    ((fun (X : Cᵒᵖ) ↦ (s (Opposite.unop X) : F.obj (Opposite.op (Opposite.unop X)))) (Opposite.op Y₂) :
      F.obj (Opposite.op (Opposite.unop (Opposite.op Y₂))))

Tactic:
change F.map f.op (s Y₁) = s Y₂

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
hs :
  ∀ {X : C} (i : I) (f : X ⟶ Y i),
    s X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
        (x i)
hs' :
  ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
        (s X) =
      s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
hex :
  ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y₂⦄,
    Sieve.arrows (Sieve.ofObjects Y Y₂) f_1 →
      Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y_1)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                  (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) →
                    (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
                (s Y₁) :
              (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) :
          (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y_1)))
            (s Y₂) :
          (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y_1)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
      (s Y₁) =
    s Y₂

Tactic:
apply (H.isSeparated _ (hY Y₂)).ext

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheaf.isSeparated
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
hs :
  ∀ {X : C} (i : I) (f : X ⟶ Y i),
    s X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
        (x i)
hs' :
  ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
        (s X) =
      s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
Z : C
φ : Z ⟶ Y₂
i : I
g : Z ⟶ Y i
hex :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
            (s Y₁) :
          (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) :
      (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op ≫ F.map φ.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        (s Y₁) :
      (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
            (s Y₁) :
          (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) :
      (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        (s Y₂) :
      (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))

Tactic:
rw [hs' φ i g, ← hs' (φ ≫ f) i g, op_comp, F.map_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) :=
  fun (X : C) ↦ ⋯.amalgamate (R := Sieve.arrows (Sieve.ofObjects Y X)) (x.familyOfElements X) ⋯
hs :
  ∀ {X : C} (i : I) (f : X ⟶ Y i),
    s X =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op (Y i)))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op X)))
        (x i)
hs' :
  ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map a.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op X))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op W)))
        (s X) =
      s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
Z : C
φ : Z ⟶ Y₂
i : I
g : Z ⟶ Y i
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂)))
            (s Y₁) :
          (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₂))) :
      (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op ≫ F.map φ.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (Opposite.op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))
        (s Y₁) :
      (fun (X : Type w) ↦ X) (F.obj (Opposite.op Z)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
y₁ y₂ : (↑F.sections : Type (max u w))
hy₁ : ∀ (i : I), (↑y₁ : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
hy₂ : ∀ (i : I), (↑y₂ : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
i : I
rw : x i = (↑y₂ : (j : Cᵒᵖ) → { obj := F, property := hF }.obj.obj j) (Opposite.op (Y i))
rw₁ rw₂ : x i = x i
⊢ (↑y₁ : (j : Cᵒᵖ) → { obj := F, property := hF }.obj.obj j) (Opposite.op (Y i)) =
    (↑y₂ : (j : Cᵒᵖ) → { obj := F, property := hF }.obj.obj j) (Opposite.op (Y i))

Tactic:
rw [hy₁, hy₂]
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
y₁ y₂ : (↑F.sections : Type (max u w))
hy₁ : ∀ (i : I), (↑y₁ : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
hy₂ : ∀ (i : I), (↑y₂ : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i
⊢ y₁ = y₂

Tactic:
exact hY.sections_ext ⟨F, hF⟩ (fun i => by rw [hy₁, hy₂])

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.GrothendieckTopology.CoversTop.sections_ext
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
i : I
⊢ (↑(hx.section_ hY hF) : (j : Cᵒᵖ) → F.obj j) (Opposite.op (Y i)) = x i

Tactic:
(hx.existsUnique_section hY hF).choose_spec.1 i

Premises used: Exists.choose_spec, And.left, CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.existsUnique_section
-- Module: Mathlib.CategoryTheory.Sites.CoversTop.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
I : Type u_2
X : I → C
hX : J.CoversTop X
I' : I → Type u
Y : (i : I) → I' i → Over.{v_1, u_1} (X i)
hY : ∀ (i : I), CoversTop (J.over (X i)) (Y i)
j Z : C
f : Z ⟶ j
h : Sieve.arrows (Sieve.ofObjects X j) f
i : I
g : Z ⟶ X i
i' : C
⊢ i' ∈ Set.range (Functor.obj (Over.forget (X i)) ∘ Y i) →
    Membership.mem (γ := Set C)
      (Set.range fun (j : (i : I) × I' i) ↦
        (Y (j.fst (β := fun (i : I) ↦ I' i)) (j.snd (β := fun (i : I) ↦ I' i))).left)
      i'

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
G : Functor.{v_1, v_2, u_1, u_2} C D
U Y Z_1 : D
f : Y ⟶ U
h : Presieve.coverByImage G U f
g : Z_1 ⟶ Y
Z : C
f₁ : Y ⟶ G.obj Z
f₂ : G.obj Z ⟶ U
e : f₁ ≫ f₂ = f
rw : g ≫ f₁ ≫ f₂ = g ≫ f
rw₁ rw₂ : g ≫ f₁ ≫ f₂ = g ≫ f₁ ≫ f₂
⊢ (g ≫ f₁) ≫ f₂ = g ≫ f

Tactic:
rw [Category.assoc, ← e]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
X : D
Y : C
f : G.obj Y ⟶ X
⊢ 𝟙 (G.obj Y) ≫ f = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
inst_2 : G.IsCoverDense K
U : D
⊢ Sieve.coverByImage G U ∈ (K : (a : D) → Set (Sieve a)) U

Tactic:
apply Functor.IsCoverDense.is_cover

Premises used: CategoryTheory.Functor.IsCoverDense.is_cover
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
h : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
B : D
obtain :
  ∀ (X : C) (f : G.obj X ⟶ B) (h : Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B),
    Sieve.coverByImage G B ∈ (K : (a : D) → Set (Sieve a)) B
⊢ Sieve.coverByImage G B ∈ (K : (a : D) → Set (Sieve a)) B

Tactic:
obtain ⟨X, f, h⟩ := h B
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
h_1 : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
B : D
X : C
f : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
⊢ Sieve.coverByImage G B ∈ (K : (a : D) → Set (Sieve a)) B

Tactic:
K.superset_covering ?_ h

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
h_1 : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
B : D
X : C
f : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
refine : Sieve.generate (Presieve.singleton f) ≤ Sieve.coverByImage G B
⊢ Sieve.coverByImage G B ∈ (K : (a : D) → Set (Sieve a)) B

Tactic:
refine K.superset_covering ?_ h

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
h_1 : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
B : D
X : C
f_1 : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f_1) ∈ (K : (a : D) → Set (Sieve a)) B
Y : D
f : Y ⟶ B
this :
  ∀ (Z : D) (g : Y ⟶ Z) (w : Z ⟶ B) (h : Presieve.singleton f_1 w) (w : g ≫ w = f), (Sieve.coverByImage G B).arrows f
⊢ (Sieve.generate (Presieve.singleton f_1)).arrows f → (Sieve.coverByImage G B).arrows f

Tactic:
⟨Z, g, _, h, w⟩
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
h_1 : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
B : D
X : C
f_1 : G.obj X ⟶ B
h_2 : Sieve.generate (Presieve.singleton f_1) ∈ (K : (a : D) → Set (Sieve a)) B
Y : D
f : Y ⟶ B
Z : D
g : Y ⟶ Z
w_1 : Z ⟶ B
h : Presieve.singleton f_1 w_1
w : g ≫ w_1 = f
mk : ∀ (g : Y ⟶ G.obj X) (w : g ≫ f_1 = f), (Sieve.coverByImage G B).arrows f
⊢ (Sieve.coverByImage G B).arrows f

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
h_1 : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
B : D
X : C
f_1 : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f_1) ∈ (K : (a : D) → Set (Sieve a)) B
Y : D
f : Y ⟶ B
g : Y ⟶ G.obj X
w : g ≫ f_1 = f
⊢ (Sieve.coverByImage G B).arrows f

Tactic:
⟨⟨_, g, _, w⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Presieve.coverByImage, CategoryTheory.Presieve.CoverByImageStructure.mk
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
h_1 : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
B : D
X : C
f_1 : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f_1) ∈ (K : (a : D) → Set (Sieve a)) B
Y : D
f : Y ⟶ B
g : Y ⟶ G.obj X
w : g ≫ f_1 = f
⊢ (Sieve.coverByImage G B).arrows f

Tactic:
exact ⟨⟨_, g, _, w⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
ℱ : Sheaf K (Type u_5)
X : D
s t : ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)
h :
  ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
    Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
          s :
        (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
          t :
        (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
apply :
  ∀ ⦃Y : D⦄ ⦃f : Y ⟶ X⦄,
    (Sieve.coverByImage G X).arrows f →
      Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op Y)))
            s :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op Y)))
            t :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y)))
⊢ s = t

Tactic:
apply ((isSheaf_iff_isSheaf_of_type _ _).1 ℱ.property
    (Sieve.coverByImage G X) (G.is_cover_of_isCoverDense K X)).isSeparatedFor.ext

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.is_cover_of_isCoverDense, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.Sieve.coverByImage, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
ℱ : Sheaf K (Type u_5)
X : D
s t : ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)
h :
  ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
    Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
          s :
        (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
          t :
        (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
Y : D
Z : C
f₁ : Y ⟶ G.obj Z
f₂ : G.obj Z ⟶ X
⊢ Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (f₁ ≫ f₂).op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op Y)))
        s :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (f₁ ≫ f₂).op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op Y)))
        t :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y)))

Tactic:
simp [h f₂]
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
    (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))

Tactic:
K.transitive T.2 _ fun Y iYX hiYX ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.transitive, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
refine :
  ∀ (Y : D) (iYX : Y ⟶ G.obj X) (hiYX : (↑T : Sieve (G.obj X)).arrows iYX),
    Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X)))) ∈
      (K : (a : D) → Set (Sieve a)) Y
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
    (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))

Tactic:
refine K.transitive T.2 _ fun Y iYX hiYX ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.transitive, Subtype.property