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
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F₁ ⟶ F₂
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) → (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₂))
hF₂ : ∃ (U : C), F₂ = Functor.obj shrinkYoneda.{w, v, u} U
obtain :
  ∀ (U : C) (f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U) [Mono f]
    (hf :
      ∀ (Φ : P.FullSubcategory),
        Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
          (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
              (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))),
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f

Tactic:
obtain ⟨U, rfl⟩ := hF₂

Premises used: 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
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
this :
  Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U)) ∈
    (J : (a : C) → Set (Sieve a)) U
V : C
g : ToType (FC := TypeCat.Fun) (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op V))
obtain :
  ∀ (g : unop (op V) ⟶ U),
    Presheaf.imageSieve (FA := TypeCat.Fun) f
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op V) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op V)) g) ∈
      (J : (a : C) → Set (Sieve a)) V
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f g ∈ (J : (a : C) → Set (Sieve a)) V

Tactic:
obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv, Equiv.surjective, 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
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
this :
  Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U)) ∈
    (J : (a : C) → Set (Sieve a)) U
V : C
g : unop (op V) ⟶ U
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop (op V)))) ((J : (a : C) → Set (Sieve a)) (unop (op V)))
    (Sieve.pullback g
      (Presheaf.imageSieve (FA := TypeCat.Fun) f
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U))
          (𝟙 U))))

Tactic:
replace this := J.pullback_stable g this
-- 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
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
V : C
g : unop (op V) ⟶ U
this :
  Membership.mem (γ := Set (Sieve.{v, u} (unop (op V)))) ((J : (a : C) → Set (Sieve a)) (unop (op V)))
    (Sieve.pullback g
      (Presheaf.imageSieve (FA := TypeCat.Fun) f
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U))
          (𝟙 U))))
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop (op V)))) ((J : (a : C) → Set (Sieve a)) (unop (op V)))
    (Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v, u} U) g.op) :
          (a : (shrinkYoneda.{w, v, u}.obj U).obj (op U)) → (shrinkYoneda.{w, v, u}.obj U).obj (op (unop (op V))))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U))
            (𝟙 U) :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op U))))

Tactic:
rw [Presheaf.pullback_imageSieve] at this

Premises used: CategoryTheory.Presheaf.pullback_imageSieve
-- 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
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
V : C
g : unop (op V) ⟶ U
this :
  Membership.mem (γ := Set (Sieve.{v, u} (unop (op V)))) ((J : (a : C) → Set (Sieve a)) (unop (op V)))
    (Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v, u} U) g.op) :
          (a : (shrinkYoneda.{w, v, u}.obj U).obj (op U)) → (shrinkYoneda.{w, v, u}.obj U).obj (op (unop (op V))))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U))
            (𝟙 U) :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op U))))
hg :
  Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v, u} U) g.op) :
          (a : (shrinkYoneda.{w, v, u}.obj U).obj (op U)) → (shrinkYoneda.{w, v, u}.obj U).obj (op V))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : U ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U) :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op U)) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op V))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : V ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op V)) g :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op V))
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op V) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op V)) g) ∈
    (J : (a : C) → Set (Sieve a)) V

Tactic:
simpa [← hg]
-- 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
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
suffices :
  Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U)) ∈
    (J : (a : C) → Set (Sieve a)) U
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f

Tactic:
suffices Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U)) ∈ J U from ⟨by
    intro V g
    obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g
    replace this := J.pullback_stable g this
    rw [Presheaf.pullback_imageSieve] at this
    have hg := shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op (𝟙 _)
    simp only [Quiver.Hom.unop_op, Category.comp_id] at hg
    simpa [← hg]⟩
-- 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
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U)) ∈
    (J : (a : C) → Set (Sieve a)) U

Tactic:
hP _ (fun Φ u ↦ ?_)
-- 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
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
refine :
  ∀ (Φ : P.FullSubcategory) (u : Φ.obj (P := P).fiber.obj U),
    ∃ (Y : C) (g : Y ⟶ U) (_ :
      Sieve.arrows
        (Presheaf.imageSieve (FA := TypeCat.Fun) f
          ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U))
            (𝟙 U)))
        g)
      (y : Φ.obj (P := P).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj U))
          y =
        u
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U)) ∈
    (J : (a : C) → Set (Sieve a)) U

Tactic:
refine hP _ (fun Φ u ↦ ?_)
-- 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)
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
x x_1 : Sheaf J (Type w)
f : x ⟶ x_1
h : Mono f
hf :
  ∀ (i : P.FullSubcategory),
    IsIso (X := Functor.obj i.obj (P := P).sheafFiber x) (Functor.map i.obj (P := P).sheafFiber f)
rw : Sheaf.IsLocallySurjective (FA := TypeCat.Fun) f
⊢ Epi f

Tactic:
rw [← Sheaf.isLocallySurjective_iff_epi]

Premises used: CategoryTheory.Sheaf.isLocallySurjective_iff_epi
-- 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)
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
x x_1 : Sheaf J (Type w)
f : x ⟶ x_1
h : Mono f
hf :
  ∀ (i : P.FullSubcategory),
    IsIso (X := Functor.obj i.obj (P := P).sheafFiber x) (Functor.map i.obj (P := P).sheafFiber f)
⊢ Sheaf.IsLocallySurjective (FA := TypeCat.Fun) f

Tactic:
mk'.isLocallySurjective hP _
            (fun Φ ↦ ((isIso_iff_bijective _).1 (hf Φ)).2)

Premises used: CategoryTheory.isIso_iff_bijective, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, And.right, Iff.mp, _private.0.CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.mk'.isLocallySurjective, CategoryTheory.GrothendieckTopology.Point.sheafFiber
-- 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)
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
x x_1 : Sheaf J (Type w)
f : x ⟶ x_1
h : Mono f
hf :
  ∀ (i : P.FullSubcategory),
    IsIso (X := Functor.obj i.obj (P := P).sheafFiber x) (Functor.map i.obj (P := P).sheafFiber f)
⊢ Sheaf.IsLocallySurjective (FA := TypeCat.Fun) f

Tactic:
exact mk'.isLocallySurjective hP _
            (fun Φ ↦ ((isIso_iff_bijective _).1 (hf Φ)).2)

Premises used: CategoryTheory.isIso_iff_bijective, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, And.right, Iff.mp, _private.0.CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.mk'.isLocallySurjective, CategoryTheory.GrothendieckTopology.Point.sheafFiber
-- 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)
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
x x_1 : Sheaf J (Type w)
f : x ⟶ x_1
h : Mono f
hf :
  ∀ (i : P.FullSubcategory),
    IsIso (X := Functor.obj i.obj (P := P).sheafFiber x) (Functor.map i.obj (P := P).sheafFiber f)
⊢ Epi f

Tactic:
have : Epi f := by
          rw [← Sheaf.isLocallySurjective_iff_epi]
          exact mk'.isLocallySurjective hP _
            (fun Φ ↦ ((isIso_iff_bijective _).1 (hf Φ)).2)
-- 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)
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
x x_1 : Sheaf J (Type w)
f : x ⟶ x_1
h : Mono f
hf :
  ∀ (i : P.FullSubcategory),
    IsIso (X := Functor.obj i.obj (P := P).sheafFiber x) (Functor.map i.obj (P := P).sheafFiber f)
this : Epi f
⊢ IsIso f

Tactic:
Balanced.isIso_of_mono_of_epi f

Premises used: CategoryTheory.Balanced.isIso_of_mono_of_epi
-- 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)
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
x x_1 : Sheaf J (Type w)
f : x ⟶ x_1
h : Mono f
hf :
  ∀ (i : P.FullSubcategory),
    IsIso (X := Functor.obj i.obj (P := P).sheafFiber x) (Functor.map i.obj (P := P).sheafFiber f)
this : Epi f
⊢ IsIso f

Tactic:
exact Balanced.isIso_of_mono_of_epi f

Premises used: CategoryTheory.Balanced.isIso_of_mono_of_epi