awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
inst_1 : LocallySmall.{w, v, u} C
U T : C
f : U ⟶ T
inst_2 : Mono f
⊢ Function.Injective (α := (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) (β := (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f)) :
      (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
have rw : Mono (Φ.fiber.map f)
Tactic: rw [← mono_iff_injective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
inst_1 : LocallySmall.{w, v, u} C
U T : C
f : U ⟶ T
inst_2 : Mono f
hT : IsTerminal.{v, u} T
x x_1 : Φ.fiber.obj U
⊢ Eq (α := (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
        x :
      (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
        x_1 :
      (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
have have : ∀ (this : Unique (Φ.fiber.obj T)),
  Eq (α := (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
        x :
      (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
        x_1 :
      (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
Tactic: have := Φ.uniqueFiberObj T hT
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
B : Type u''
inst_2 : Category.{v'', u''} B
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v'', u''} B
F : Functor.{v', v'', u', u''} A B
inst_5 : LocallySmall.{w, v, u} C
inst_6 : PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F
X : C
x : Φ.fiber.obj X
P : Functor.{v, v', u, u'} Cᵒᵖ A
⊢ Eq (α := (P ⋙ F).obj (op X) ⟶ (Φ.presheafFiber ⋙ F).obj P)
    (CategoryStruct.comp (Y := Functor.obj Φ.presheafFiber (P ⋙ F)) (Φ.toPresheafFiber X x (P ⋙ F))
      (NatTrans.app (Iso.hom (Φ.presheafFiberCompIso F)) P))
    (F.map (Φ.toPresheafFiber X x P))
have this : PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ F
Tactic: haveI := Functor.Final.preservesColimitsOfShape_of_final
    (FinallySmall.fromFilteredFinalModel.{w} (Φ.fiber.Elementsᵒᵖ)) F
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
B : Type u''
inst_2 : Category.{v'', u''} B
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v'', u''} B
F : Functor.{v', v'', u', u''} A B
inst_5 : LocallySmall.{w, v, u} C
inst_6 : PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F
X : C
x : Φ.fiber.obj X
P : Functor.{v, v', u, u'} Cᵒᵖ A
this : PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ F
⊢ Eq (α := (P ⋙ F).obj (op X) ⟶ (Φ.presheafFiber ⋙ F).obj P)
    (CategoryStruct.comp (Y := Functor.obj Φ.presheafFiber (P ⋙ F)) (Φ.toPresheafFiber X x (P ⋙ F))
      (NatTrans.app (Iso.hom (Φ.presheafFiberCompIso F)) P))
    (F.map (Φ.toPresheafFiber X x P))
have simp : Eq (α := (P ⋙ F).obj (op X) ⟶ (Φ.presheafFiber ⋙ F).obj P)
  (CategoryStruct.comp (Y := Functor.obj Φ.presheafFiber (P ⋙ F)) (Φ.toPresheafFiber X x (P ⋙ F))
    (NatTrans.app
      (Iso.hom
        (Functor.isoWhiskerLeft
          (Functor.obj (Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A) (CategoryOfElements.π Φ.fiber).op)
          (Iso.symm (preservesColimitNatIso F))))
      P))
  (F.map (Φ.toPresheafFiber X x P))
Tactic: simp only [presheafFiberCompIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Comap (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
Φ : Point.{w, v_2, u_2} K
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : RepresentablyFlat F
J : GrothendieckTopology.{v_1, u_1} C
hF : CoverPreserving J K F
inst_3 : InitiallySmall (F ⋙ Φ.fiber).Elements
X : C
R : Sieve.{v_1, u_1} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
x : (F ⋙ Φ.fiber).obj X
⊢ ∃ (Y : C) (f : Y ⟶ X) (_ : R.arrows f) (y : (F ⋙ Φ.fiber).obj Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Φ.fiber).map f) :
          (a : (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj Y)) → (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj X))
        y =
      x
have obtain : ∀ (Y : D) (W : C) (g : W ⟶ X) (h : Y ⟶ F.obj W) (hg : R.arrows g) (y : Φ.fiber.obj Y),
  ∃ (Y_1 : C) (f : Y_1 ⟶ X) (_ : R.arrows f) (y_1 : (F ⋙ Φ.fiber).obj Y_1),
    Eq (α := (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Φ.fiber).map f) :
            (a : (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj Y_1)) → (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj X))
          y_1 :
        (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map (h ≫ F.map g)) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj (F.obj X)))
          y :
        (fun (X : Type w) ↦ X) (Φ.fiber.obj (F.obj X)))
Tactic: obtain ⟨Y, f, ⟨W, g, h, hg, rfl⟩, y, rfl⟩ :=
      Φ.jointly_surjective (Sieve.functorPushforward F R) (hF.cover_preserve hR) x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Comap (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
Φ : Point.{w, v_2, u_2} K
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : RepresentablyFlat F
J : GrothendieckTopology.{v_1, u_1} C
hF : CoverPreserving J K F
inst_3 : InitiallySmall (F ⋙ Φ.fiber).Elements
X : C
R : Sieve.{v_1, u_1} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
Y : D
W : C
g : W ⟶ X
h : Y ⟶ F.obj W
hg : R.arrows g
y : Φ.fiber.obj Y
⊢ ∃ (Y_1 : C) (f : Y_1 ⟶ X) (_ : R.arrows f) (y_1 : (F ⋙ Φ.fiber).obj Y_1),
    Eq (α := (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Φ.fiber).map f) :
            (a : (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj Y_1)) → (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj X))
          y_1 :
        (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map (h ≫ F.map g)) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj (F.obj X)))
          y :
        (fun (X : Type w) ↦ X) (Φ.fiber.obj (F.obj X)))
have h₁ : Eq (α := (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Φ.fiber).map g) :
        (a : (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj W)) → (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map h) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj (F.obj W)))
          y :
        (fun (X : Type w) ↦ X) (Φ.fiber.obj (F.obj W))) :
    (fun (X : Type w) ↦ X) ((F ⋙ Φ.fiber).obj X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map (h ≫ F.map g)) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj (F.obj X)))
      y :
    (fun (X : Type w) ↦ X) (Φ.fiber.obj (F.obj X)))
Tactic: use W, g, hg, Φ.fiber.map h y
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
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))
K L : Sheaf.{v, v', u, u'} J A
f : K ⟶ L
h :
  ∀ (i : P.FullSubcategory),
    IsIso (X := Functor.obj (GrothendieckTopology.Point.sheafFiber.{w, v, v', u, u'} (i.obj (P := P))) K)
      (Functor.map (GrothendieckTopology.Point.sheafFiber.{w, v, v', u, u'} (i.obj (P := P))) f)
⊢ IsIso f
have rw : ∀ (i : P.FullSubcategory),
  IsIso (X := Functor.obj i.obj (P := P).sheafFiber (Functor.obj (sheafCompose J (forget A (FC := FC) (CC := CC))) K))
    (Functor.map i.obj (P := P).sheafFiber (Functor.map (sheafCompose J (forget A (FC := FC) (CC := CC))) f))
Tactic: rw [← isIso_iff_of_reflects_iso _ (sheafCompose J (forget A)),
      hP.jointlyReflectIsomorphisms_type.isIso_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
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
⊢ J.W f ↔
    ∀ (Φ : P.FullSubcategory),
      IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber F) (Functor.map Φ.obj (P := P).presheafFiber f)
have rw : (∀ (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: rw [GrothendieckTopology.W_iff, (hP.jointlyReflectIsomorphisms A).isIso_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (hypothesis)
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))
⊢ Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f
have 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)))
Tactic: simp only [← ofHom_epi_iff_surjective] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
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)))
⊢ Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f
have 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)))))
Tactic: rw [Presheaf.isLocallySurjective_iff_whisker_forget,
    ← Presheaf.isLocallySurjective_presheafToSheaf_map_iff,
    Sheaf.isLocallySurjective_iff_epi,
    (hP.jointlyReflectEpimorphisms (Type w)).epi_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
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
have 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
Tactic: refine ⟨fun hf Φ x ↦ ?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun hf Φ x ↦ ?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
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
⊢ ∃ (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
have 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))
Tactic: obtain ⟨Z, _, ⟨_, p, _, ⟨i⟩, rfl⟩, z, rfl⟩ := Φ.obj.jointly_surjective _ hf x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
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
⊢ Sieve.ofArrows U f ∈ (J : (a : C) → Set (Sieve a)) X
have 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))
Tactic: rw [J.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
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))
have 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
Tactic: refine hP.jointly_reflect_isLocallySurjective _ (fun Φ x ↦ ?_)