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)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_7 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
hJ : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
inst_8 : HasWeakSheafify.{v, v', u, u'} J A
inst_9 : HasProducts.{w, v', u'} A
⊢ (∀ (i : P.FullSubcategory),
      IsIso (X :=
        Functor.obj (GrothendieckTopology.Point.sheafFiber.{w, v, v', u, u'} (i.obj (P := P)))
          (Functor.obj (presheafToSheaf J A) F))
        (Functor.map (GrothendieckTopology.Point.sheafFiber.{w, v, v', u, u'} (i.obj (P := P)))
          (Functor.map (presheafToSheaf J A) f))) ↔
    ∀ (Φ : P.FullSubcategory),
      IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber F) (Functor.map Φ.obj (P := P).presheafFiber f)

Tactic:
forall_congr'
    (fun Φ ↦ (MorphismProperty.isomorphisms A).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (Φ.obj.presheafToSheafCompSheafFiberIso A)).app (Arrow.mk f)))

Premises used: CategoryTheory.GrothendieckTopology.Point.presheafToSheafCompSheafFiberIso, CategoryTheory.Functor, Opposite, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, forall_congr', CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso
-- 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)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_7 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
hJ : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
inst_8 : HasWeakSheafify.{v, v', u, u'} J A
inst_9 : HasProducts.{w, v', u'} A
⊢ (∀ (i : P.FullSubcategory),
      IsIso (X :=
        Functor.obj (GrothendieckTopology.Point.sheafFiber.{w, v, v', u, u'} (i.obj (P := P)))
          (Functor.obj (presheafToSheaf J A) F))
        (Functor.map (GrothendieckTopology.Point.sheafFiber.{w, v, v', u, u'} (i.obj (P := P)))
          (Functor.map (presheafToSheaf J A) f))) ↔
    ∀ (Φ : P.FullSubcategory),
      IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber F) (Functor.map Φ.obj (P := P).presheafFiber f)

Tactic:
exact forall_congr'
    (fun Φ ↦ (MorphismProperty.isomorphisms A).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (Φ.obj.presheafToSheafCompSheafFiberIso A)).app (Arrow.mk f)))

Premises used: CategoryTheory.Functor, Opposite, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, forall_congr', CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso
-- 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)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
inst_7 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
inst_8 : HasSheafify J (Type w)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective.{w + 1, w + 1} (α := CC (Functor.obj Φ.obj (P := P).presheafFiber X)) (β :=
      CC (Functor.obj Φ.obj (P := P).presheafFiber Y))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : CC (Φ.obj.presheafFiber.obj X)) → CC (Φ.obj.presheafFiber.obj Y))
⊢ ∀ (Φ : P.FullSubcategory),
    Epi.{w, w + 1} (X := CC (Functor.obj Φ.obj (P := P).presheafFiber X)) (Y :=
      CC (Functor.obj Φ.obj (P := P).presheafFiber Y))
      (↾(⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.obj (P := P).presheafFiber f)) :
          (a : CC (Φ.obj.presheafFiber.obj X)) → CC (Φ.obj.presheafFiber.obj Y)))

Tactic:
simp only [← ofHom_epi_iff_surjective] at hf

Premises used: CategoryTheory.ofHom_epi_iff_surjective
-- 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)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
inst_7 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
inst_8 : HasSheafify J (Type w)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
hf :
  ∀ (Φ : P.FullSubcategory),
    Epi.{w, w + 1} (X := CC (Functor.obj Φ.obj (P := P).presheafFiber X)) (Y :=
      CC (Functor.obj Φ.obj (P := P).presheafFiber Y))
      (↾(⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.obj (P := P).presheafFiber f)) :
          (a : CC (Φ.obj.presheafFiber.obj X)) → CC (Φ.obj.presheafFiber.obj Y)))
rw :
  ∀ (i : P.FullSubcategory),
    Epi (X :=
      Functor.obj i.obj (P := P).sheafFiber
        (Functor.obj (presheafToSheaf J (Type w)) (X ⋙ forget A (FC := FC) (CC := CC))))
      (Functor.map i.obj (P := P).sheafFiber
        (Functor.map (presheafToSheaf J (Type w)) (Functor.whiskerRight f (forget A (FC := FC) (CC := CC)))))
⊢ Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f

Tactic:
rw [Presheaf.isLocallySurjective_iff_whisker_forget,
    ← Presheaf.isLocallySurjective_presheafToSheaf_map_iff,
    Sheaf.isLocallySurjective_iff_epi,
    (hP.jointlyReflectEpimorphisms (Type w)).epi_iff]

Premises used: CategoryTheory.Sheaf.isLocallySurjective_iff_epi, CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, CategoryTheory.Presheaf.isLocallySurjective_presheafToSheaf_map_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)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
inst_7 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
inst_8 : HasSheafify J (Type w)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
hf :
  ∀ (Φ : P.FullSubcategory),
    Epi.{w, w + 1} (X := CC (Functor.obj Φ.obj (P := P).presheafFiber X)) (Y :=
      CC (Functor.obj Φ.obj (P := P).presheafFiber Y))
      (↾(⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.obj (P := P).presheafFiber f)) :
          (a : CC (Φ.obj.presheafFiber.obj X)) → CC (Φ.obj.presheafFiber.obj Y)))
⊢ ∀ (i : P.FullSubcategory),
    Epi (X :=
      Functor.obj i.obj (P := P).sheafFiber
        (Functor.obj (presheafToSheaf J (Type w)) (X ⋙ forget A (FC := FC) (CC := CC))))
      (Functor.map i.obj (P := P).sheafFiber
        (Functor.map (presheafToSheaf J (Type w)) (Functor.whiskerRight f (forget A (FC := FC) (CC := CC)))))

Tactic:
fun Φ ↦ ((MorphismProperty.epimorphisms (Type w)).arrow_mk_iso_iff
    (((Functor.mapArrowFunctor _ _).mapIso
      ((Φ.obj.presheafFiberCompIso (forget A)).symm ≪≫
        Functor.isoWhiskerLeft _ (Φ.obj.presheafToSheafCompSheafFiberIso (Type w)).symm)).app
          (Arrow.mk f))).1 (hf Φ)

Premises used: CategoryTheory.GrothendieckTopology.Point.presheafToSheafCompSheafFiberIso, CategoryTheory.Functor, Opposite, CategoryTheory.Functor.comp, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Limits.colimit, CategoryTheory.Functor.whiskeringRight, CategoryTheory.GrothendieckTopology.Point.presheafFiberCompIso, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Functor.whiskerRight, CategoryTheory.MorphismProperty.epimorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.forget, Iff.mp, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj
-- 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)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
inst_7 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
inst_8 : HasSheafify J (Type w)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
hf :
  ∀ (Φ : P.FullSubcategory),
    Epi.{w, w + 1} (X := CC (Functor.obj Φ.obj (P := P).presheafFiber X)) (Y :=
      CC (Functor.obj Φ.obj (P := P).presheafFiber Y))
      (↾(⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.obj (P := P).presheafFiber f)) :
          (a : CC (Φ.obj.presheafFiber.obj X)) → CC (Φ.obj.presheafFiber.obj Y)))
⊢ ∀ (i : P.FullSubcategory),
    Epi (X :=
      Functor.obj i.obj (P := P).sheafFiber
        (Functor.obj (presheafToSheaf J (Type w)) (X ⋙ forget A (FC := FC) (CC := CC))))
      (Functor.map i.obj (P := P).sheafFiber
        (Functor.map (presheafToSheaf J (Type w)) (Functor.whiskerRight f (forget A (FC := FC) (CC := CC)))))

Tactic:
exact fun Φ ↦ ((MorphismProperty.epimorphisms (Type w)).arrow_mk_iso_iff
    (((Functor.mapArrowFunctor _ _).mapIso
      ((Φ.obj.presheafFiberCompIso (forget A)).symm ≪≫
        Functor.isoWhiskerLeft _ (Φ.obj.presheafToSheafCompSheafFiberIso (Type w)).symm)).app
          (Arrow.mk f))).1 (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
X : C
ι : Type u_1
inst_4 : Small.{w, 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
X : C
ι : Type u_1
inst_4 : Small.{w, 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
X : C
ι : Type u_1
inst_4 : Small.{w, 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
X : C
ι : Type u_1
inst_4 : Small.{w, 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
X : C
ι : Type u_1
inst_4 : Small.{w, 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
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
refine_2 :
  Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (F := ∐ fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i))
    (G := Functor.obj shrinkYoneda.{w, v, u} X) (Sigma.desc fun (i : ι) ↦ Functor.map shrinkYoneda.{w, v, u} (f i))
⊢ Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
rw [J.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map]

Premises used: CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map
-- 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
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (F := ∐ fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i))
    (G := Functor.obj shrinkYoneda.{w, v, u} X) (Sigma.desc fun (i : ι) ↦ Functor.map shrinkYoneda.{w, v, u} (f i))

Tactic:
hP.jointly_reflect_isLocallySurjective _ (fun Φ x ↦ ?_)

Premises used: CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_isLocallySurjective
-- 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
refine_2 :
  ∀ (Φ : P.FullSubcategory) (x : Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} 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
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (F := ∐ fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i))
    (G := Functor.obj shrinkYoneda.{w, v, u} X) (Sigma.desc fun (i : ι) ↦ Functor.map shrinkYoneda.{w, v, u} (f i))

Tactic:
refine hP.jointly_reflect_isLocallySurjective _ (fun Φ x ↦ ?_)

Premises used: CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_isLocallySurjective