awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst_4 : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf :
  ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
Φ : P.FullSubcategory
x : Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X)
refine_2 :
  ∀ (x : Φ.obj (P := P).fiber.obj X),
    ∃ (a :
      Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) Φ.obj (P := P).presheafFiber
        (∐ fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i))),
      Eq (α := Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Functor.map Φ.obj (P := P).presheafFiber
                  (Sigma.desc fun (i : ι) ↦ Functor.map shrinkYoneda.{w, v, u} (f i))) :
              (a : Φ.obj.presheafFiber.obj (∐ fun (i : ι) ↦ shrinkYoneda.{w, v, u}.obj (U i))) →
                Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))
            a :
          Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
        ((Equiv.symm (Iso.toEquiv (Iso.app Φ.obj (P := P).shrinkYonedaCompPresheafFiberIso X)) :
              (a : Φ.obj.fiber.obj X) → (shrinkYoneda.{w, v, u} ⋙ Φ.obj.presheafFiber).obj X)
            x :
          (shrinkYoneda.{w, v, u} ⋙ Φ.obj (P := P).presheafFiber).obj X)
⊢ ∃ (a :
    Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) Φ.obj (P := P).presheafFiber
      (∐ fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i))),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map Φ.obj (P := P).presheafFiber
              (Sigma.desc fun (i : ι) ↦ Functor.map shrinkYoneda.{w, v, u} (f i))) :
          (a : Φ.obj.presheafFiber.obj (∐ fun (i : ι) ↦ shrinkYoneda.{w, v, u}.obj (U i))) →
            Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))
        a =
      x

Tactic:
obtain ⟨x, rfl⟩ := (Φ.obj.shrinkYonedaCompPresheafFiberIso.app X).toEquiv.symm.surjective x

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.ObjectProperty.FullSubcategory.obj, Equiv.surjective, CategoryTheory.GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso, CategoryTheory.Iso.app, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst_4 : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf :
  ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
Φ : P.FullSubcategory
i : ι
y : Φ.obj (P := P).fiber.obj (U i)
⊢ ∃ (a :
    Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) Φ.obj (P := P).presheafFiber
      (∐ fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i))),
    Eq (α := Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Functor.map Φ.obj (P := P).presheafFiber
                (Sigma.desc fun (i : ι) ↦ Functor.map shrinkYoneda.{w, v, u} (f i))) :
            (a : Φ.obj.presheafFiber.obj (∐ fun (i : ι) ↦ shrinkYoneda.{w, v, u}.obj (U i))) →
              Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))
          a :
        Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
      ((Equiv.symm (Iso.toEquiv (Iso.app Φ.obj (P := P).shrinkYonedaCompPresheafFiberIso X)) :
            (a : Φ.obj.fiber.obj X) → (shrinkYoneda.{w, v, u} ⋙ Φ.obj.presheafFiber).obj X)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y :
            (fun (X : Type w) ↦ X) (Φ.obj (P := P).fiber.obj X)) :
        (shrinkYoneda.{w, v, u} ⋙ Φ.obj (P := P).presheafFiber).obj X)

Tactic:
⟨Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w}.obj (U i)) i)
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app _ y), ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.shrinkYoneda, CategoryTheory.Limits.Sigma.ι, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, CategoryTheory.GrothendieckTopology.Point.presheafFiber, Exists.intro, CategoryTheory.GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst_4 : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf :
  ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
Φ : P.FullSubcategory
i : ι
y : Φ.obj (P := P).fiber.obj (U i)
⊢ Eq (α := (shrinkYoneda.{w, v, u} ⋙ Φ.obj (P := P).presheafFiber).obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Φ.obj (P := P).fiber.map (f i) ≫
              NatTrans.app (Iso.inv Φ.obj (P := P).shrinkYonedaCompPresheafFiberIso) X) :
          (a : Φ.obj.fiber.obj (U i)) → (shrinkYoneda.{w, v, u} ⋙ Φ.obj.presheafFiber).obj X)
        y :
      (shrinkYoneda.{w, v, u} ⋙ Φ.obj (P := P).presheafFiber).obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Iso.inv Φ.obj (P := P).shrinkYonedaCompPresheafFiberIso) (U i) ≫
              (shrinkYoneda.{w, v, u} ⋙ Φ.obj (P := P).presheafFiber).map (f i)) :
          (a : Φ.obj.fiber.obj (U i)) → (shrinkYoneda.{w, v, u} ⋙ Φ.obj.presheafFiber).obj X)
        y :
      (shrinkYoneda.{w, v, u} ⋙ Φ.obj (P := P).presheafFiber).obj X)

Tactic:
have := ConcreteCategory.congr_hom
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.naturality (f i)) y
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
inst_4 : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
⊢ Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X ↔
    ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
      ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
              (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
            y =
          x

Tactic:
⟨fun hf Φ x ↦ ?_, fun hf ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
inst_4 : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
refine_1 :
  ∀ (hf : Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X) (Φ : P.FullSubcategory)
    (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
refine_2 :
  ∀
    (hf :
      ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x),
    Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X ↔
    ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
      ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
              (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
            y =
          x

Tactic:
refine ⟨fun hf Φ x ↦ ?_, fun hf ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
inst_4 : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X
Φ : P.FullSubcategory
x : Φ.obj (P := P).fiber.obj X
refine_1 :
  ∀ (Z : C) ⦃Y : C⦄ (i : ι) (p : Z ⟶ U i) (z : Φ.obj (P := P).fiber.obj Z),
    ∃ (i_1 : ι) (y : Φ.obj (P := P).fiber.obj (U i_1)),
      Eq (α := (fun (X : Type w) ↦ X) (Φ.obj (P := P).fiber.obj X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i_1)) :
              (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i_1))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
            y :
          (fun (X : Type w) ↦ X) (Φ.obj (P := P).fiber.obj X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (p ≫ f i)) :
              (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Z)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
            z :
          (fun (X : Type w) ↦ X) (Φ.obj (P := P).fiber.obj X))
⊢ ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
          (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
        y =
      x

Tactic:
obtain ⟨Z, _, ⟨_, p, _, ⟨i⟩, rfl⟩, z, rfl⟩ := Φ.obj.jointly_surjective _ hf x

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.GrothendieckTopology.Point.jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
inst_4 : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X
Φ : P.FullSubcategory
Z Y : C
i : ι
p : Z ⟶ U i
z : Φ.obj (P := P).fiber.obj Z
⊢ Eq (α := (fun (X : Type w) ↦ X) (Φ.obj (P := P).fiber.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
          (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map p) :
              (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Z)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i)))
            z :
          (fun (X : Type w) ↦ X) (Φ.obj (P := P).fiber.obj (U i))) :
      (fun (X : Type w) ↦ X) (Φ.obj (P := P).fiber.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (p ≫ f i)) :
          (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Z)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
        z :
      (fun (X : Type w) ↦ X) (Φ.obj (P := P).fiber.obj X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
inst_4 : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X
Φ : P.FullSubcategory
Z Y : C
i : ι
p : Z ⟶ U i
z : Φ.obj (P := P).fiber.obj Z
⊢ ∃ (i_1 : ι) (y : Φ.obj (P := P).fiber.obj (U i_1)),
    Eq (α := (fun (X : Type w) ↦ X) (Φ.obj (P := P).fiber.obj X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i_1)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i_1))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y :
        (fun (X : Type w) ↦ X) (Φ.obj (P := P).fiber.obj X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (p ≫ f i)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Z)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          z :
        (fun (X : Type w) ↦ X) (Φ.obj (P := P).fiber.obj X))

Tactic:
exact ⟨i, Φ.obj.fiber.map p z, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
inst_4 : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf :
  ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj (P := P).fiber.obj X
refine_2 :
  ∀ (i : (j : ι') → ι)
    (y :
      (j : ι') → j.fst (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X).obj (P := P).fiber.obj (U (i j)))
    (hy :
      ∀ (j : ι'),
        (ConcreteCategory.hom (FC := TypeCat.Fun)
                (j.fst (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X).obj (P := P).fiber.map
                  (f (i j))) :
              (a : (fun (X : Type w) ↦ X) (j.fst.obj.fiber.obj (U (i j)))) →
                (fun (X : Type w) ↦ X) (j.fst.obj.fiber.obj X))
            (y j) =
          j.snd (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X)),
    Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
choose i y hy using fun (j : ι') ↦ hf j.1 j.2

Premises used: Sigma.fst, Sigma.snd
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
inst_4 : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf :
  ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj (P := P).fiber.obj X
i : (j : ι') → ι
y : (j : ι') → j.fst (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X).obj (P := P).fiber.obj (U (i j))
hy :
  ∀ (j : ι'),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (j.fst (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X).obj (P := P).fiber.map (f (i j))) :
          (a : (fun (X : Type w) ↦ X) (j.fst.obj.fiber.obj (U (i j)))) → (fun (X : Type w) ↦ X) (j.fst.obj.fiber.obj X))
        (y j) =
      j.snd (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X)
⊢ Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
J.superset_covering (S := Sieve.ofArrows _ (fun i' ↦ f (i i'))) ?_ ?_

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
inst_4 : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf :
  ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj (P := P).fiber.obj X
i : (j : ι') → ι
y : (j : ι') → j.fst (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X).obj (P := P).fiber.obj (U (i j))
hy :
  ∀ (j : ι'),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (j.fst (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X).obj (P := P).fiber.map (f (i j))) :
          (a : (fun (X : Type w) ↦ X) (j.fst.obj.fiber.obj (U (i j)))) → (fun (X : Type w) ↦ X) (j.fst.obj.fiber.obj X))
        (y j) =
      j.snd (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X)
refine_2 : (Sieve.ofArrows (fun (i' : ι') ↦ U (i i')) fun (i' : ι') ↦ f (i i')) ≤ Sieve.ofArrows U f
refine_2₁ : (Sieve.ofArrows (fun (i' : ι') ↦ U (i i')) fun (i' : ι') ↦ f (i i')) ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
refine J.superset_covering (S := Sieve.ofArrows _ (fun i' ↦ f (i i'))) ?_ ?_

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
inst_4 : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf :
  ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj (P := P).fiber.obj X
i : (j : ι') → ι
y : (j : ι') → j.fst (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X).obj (P := P).fiber.obj (U (i j))
hy :
  ∀ (j : ι'),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (j.fst (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X).obj (P := P).fiber.map (f (i j))) :
          (a : (fun (X : Type w) ↦ X) (j.fst.obj.fiber.obj (U (i j)))) → (fun (X : Type w) ↦ X) (j.fst.obj.fiber.obj X))
        (y j) =
      j.snd (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X)
refine_2 : ∀ (i_1 : ι'), (Sieve.ofArrows U f).arrows (Y := U (i i_1)) (f (i i_1))
⊢ (Sieve.ofArrows (fun (i' : ι') ↦ U (i i')) fun (i' : ι') ↦ f (i i')) ≤ Sieve.ofArrows U f

Tactic:
rw [Sieve.generate_le_iff, Presieve.ofArrows_le_iff]

Premises used: CategoryTheory.Presieve.ofArrows_le_iff, CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
inst_4 : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf :
  ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj (P := P).fiber.obj X
i : (j : ι') → ι
y : (j : ι') → j.fst (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X).obj (P := P).fiber.obj (U (i j))
hy :
  ∀ (j : ι'),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (j.fst (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X).obj (P := P).fiber.map (f (i j))) :
          (a : (fun (X : Type w) ↦ X) (j.fst.obj.fiber.obj (U (i j)))) → (fun (X : Type w) ↦ X) (j.fst.obj.fiber.obj X))
        (y j) =
      j.snd (β := fun (Φ : P.FullSubcategory) ↦ Φ.obj (P := P).fiber.obj X)
⊢ ∀ (i_1 : ι'), (Sieve.ofArrows U f).arrows (Y := U (i i_1)) (f (i i_1))

Tactic:
fun _ ↦ Sieve.ofArrows_mk _ _ _

Premises used: CategoryTheory.Sieve.ofArrows_mk