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
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:
exact fun _ ↦ Sieve.ofArrows_mk _ _ _

Premises used: CategoryTheory.Sieve.ofArrows_mk
-- 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 :
  ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i_1 : ι') (y : Φ.obj (P := P).fiber.obj (U (i i_1))),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f (i i_1))) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U (i i_1)))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
⊢ (Sieve.ofArrows (fun (i' : ι') ↦ U (i i')) fun (i' : ι') ↦ f (i i')) ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
rw [hP.jointly_reflect_ofArrows_mem]

Premises used: CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem
-- 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)
⊢ ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i_1 : ι') (y : Φ.obj (P := P).fiber.obj (U (i i_1))),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f (i i_1))) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U (i i_1)))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x

Tactic:
fun Φ x ↦ ⟨_, _, hy ⟨Φ, x⟩⟩

Premises used: Exists.intro, Sigma.mk
-- 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)
⊢ ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i_1 : ι') (y : Φ.obj (P := P).fiber.obj (U (i i_1))),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f (i i_1))) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U (i i_1)))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x

Tactic:
exact fun Φ x ↦ ⟨_, _, hy ⟨Φ, x⟩⟩
-- 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₂))
inr :
  ∀
    (this :
      ∀ {F₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)} (f : F₁ ⟶ F₂) [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),
        Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f)
    (hF₂ : ¬∃ (U : C), F₂ = Functor.obj shrinkYoneda.{w, v, u} U), Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
wlog :
  ∀ {F₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)} (f : F₁ ⟶ F₂) [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), Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f

Tactic:
wlog hF₂ : ∃ (U : C), F₂ = shrinkYoneda.obj U generalizing F₁ F₂
-- 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₂))
this :
  ∀ {F₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)} (f : F₁ ⟶ F₂) [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), Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
hF₂ : ¬∃ (U : C), F₂ = Functor.obj shrinkYoneda.{w, v, u} U
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f

Tactic:
⟨fun {U} s ↦ ?_⟩

Premises used: CategoryTheory.Presheaf.IsLocallySurjective.mk
-- 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₂))
this :
  ∀ {F₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)} (f : F₁ ⟶ F₂) [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), Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
hF₂ : ¬∃ (U : C), F₂ = Functor.obj shrinkYoneda.{w, v, u} U
inr :
  ∀ {U : C} (s : ToType (FC := TypeCat.Fun) (F₂.obj (op U))),
    Presheaf.imageSieve (FA := TypeCat.Fun) f s ∈ (J : (a : C) → Set (Sieve a)) U
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f

Tactic:
refine ⟨fun {U} s ↦ ?_⟩
-- 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₂))
this :
  ∀ {F₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)} (f : F₁ ⟶ F₂) [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), Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
hF₂ : ¬∃ (U : C), F₂ = Functor.obj shrinkYoneda.{w, v, u} U
U : C
s : ToType (FC := TypeCat.Fun) (F₂.obj (op U))
f' : pullback (Y := Functor.obj shrinkYoneda.{w, v, u} U) f
    ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s) ⟶
  Functor.obj shrinkYoneda.{w, v, u} U :=
  pullback.snd f ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)
Φ : 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₂))

Tactic:
replace hf := 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
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
this :
  ∀ {F₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)} (f : F₁ ⟶ F₂) [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), Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
hF₂ : ¬∃ (U : C), F₂ = Functor.obj shrinkYoneda.{w, v, u} U
U : C
s : ToType (FC := TypeCat.Fun) (F₂.obj (op U))
f' : pullback (Y := Functor.obj shrinkYoneda.{w, v, u} U) f
    ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s) ⟶
  Functor.obj shrinkYoneda.{w, v, u} U :=
  pullback.snd f ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)
Φ : P.FullSubcategory
hf : Epi (X := Functor.obj Φ.obj (P := P).presheafFiber F₁) (Functor.map Φ.obj (P := P).presheafFiber f)
⊢ Epi (X :=
    Functor.obj Φ.obj (P := P).presheafFiber
      (pullback (Y := Functor.obj shrinkYoneda.{w, v, u} U) f
        ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)))
    (Functor.map Φ.obj (P := P).presheafFiber f')

Tactic:
(MorphismProperty.epimorphisms _).of_isPullback
        ((IsPullback.of_hasPullback f (shrinkYonedaEquiv.{w}.symm s)).map
          Φ.obj.presheafFiber) (.infer_property _)

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.shrinkYonedaEquiv, CategoryTheory.GrothendieckTopology.Point.presheafFiber, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.MorphismProperty.epimorphisms.infer_property, CategoryTheory.IsPullback.map, Equiv.symm, DFunLike.coe
-- 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
this :
  ∀ {F₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)} (f : F₁ ⟶ F₂) [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), Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
hF₂ : ¬∃ (U : C), F₂ = Functor.obj shrinkYoneda.{w, v, u} U
U : C
s : ToType (FC := TypeCat.Fun) (F₂.obj (op U))
f' : pullback (Y := Functor.obj shrinkYoneda.{w, v, u} U) f
    ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s) ⟶
  Functor.obj shrinkYoneda.{w, v, u} U :=
  pullback.snd f ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)
Φ : P.FullSubcategory
hf : Epi (X := Functor.obj Φ.obj (P := P).presheafFiber F₁) (Functor.map Φ.obj (P := P).presheafFiber f)
⊢ Epi (X :=
    Functor.obj Φ.obj (P := P).presheafFiber
      (pullback (Y := Functor.obj shrinkYoneda.{w, v, u} U) f
        ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)))
    (Functor.map Φ.obj (P := P).presheafFiber f')

Tactic:
exact (MorphismProperty.epimorphisms _).of_isPullback
        ((IsPullback.of_hasPullback f (shrinkYonedaEquiv.{w}.symm s)).map
          Φ.obj.presheafFiber) (.infer_property _)