awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Point.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Φ : Point.{w, v, u} J
X : C
x : Φ.fiber.obj X
U : Over.{v, u} X
u : (Over.forget X ⋙ Φ.fiber).obj U
hu : u ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U
R : Sieve.{v, u} U.left
hR : Membership.mem (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left) R
obtain :
  ∀ (Y : C) (f : Y ⟶ U.left) (hf : R.arrows f) (v : Φ.fiber.obj Y)
    (hu :
      Membership.mem (α := (Over.forget X ⋙ Φ.fiber).obj U) ((FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
              (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
            v :
          (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))),
    ∃ (Y_1 : Over.{v, u} X) (f_1 : Y_1 ⟶ U) (_ :
      Sieve.arrows (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) R) f_1) (y :
      (FunctorToTypes.fromOverFunctor Φ.fiber x).obj Y_1),
      Eq (α := (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj U))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((FunctorToTypes.fromOverFunctor Φ.fiber x).map f_1) :
              (a : (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj Y_1)) →
                (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj U))
            y :
          (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj U))
        (Subtype.mk (p := fun (x_2 : (Over.forget X ⋙ Φ.fiber).obj U) ↦
            x_2 ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
                (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
              v)
            hu :
          { x_2 : (Over.forget X ⋙ Φ.fiber).obj U // x_2 ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U })
⊢ ∃ (Y : Over.{v, u} X) (f : Y ⟶ U) (_ : Sieve.arrows (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) R) f)
    (y : (FunctorToTypes.fromOverFunctor Φ.fiber x).obj Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((FunctorToTypes.fromOverFunctor Φ.fiber x).map f) :
          (a : (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj Y)) →
            (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj U))
        y =
      Subtype.mk (p := fun (x_2 : (Over.forget X ⋙ Φ.fiber).obj U) ↦
        x_2 ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U) u hu

Tactic:
obtain ⟨Y, f, hf, v, rfl⟩ := Φ.jointly_surjective R hR u

Premises used: CategoryTheory.GrothendieckTopology.Point.jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Φ : Point.{w, v, u} J
X : C
x : Φ.fiber.obj X
U : Over.{v, u} X
R : Sieve.{v, u} U.left
hR : Membership.mem (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left) R
Y : C
f : Y ⟶ U.left
hf : R.arrows f
v : Φ.fiber.obj Y
hu :
  Membership.mem (α := (Over.forget X ⋙ Φ.fiber).obj U) ((FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
        v :
      (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
⊢ ∃ (Y_1 : Over.{v, u} X) (f_1 : Y_1 ⟶ U) (_ :
    Sieve.arrows (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) R) f_1) (y :
    (FunctorToTypes.fromOverFunctor Φ.fiber x).obj Y_1),
    Eq (α := (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj U))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((FunctorToTypes.fromOverFunctor Φ.fiber x).map f_1) :
            (a : (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj Y_1)) →
              (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj U))
          y :
        (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj U))
      (Subtype.mk (p := fun (x_2 : (Over.forget X ⋙ Φ.fiber).obj U) ↦
          x_2 ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
              (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
            v)
          hu :
        { x_2 : (Over.forget X ⋙ Φ.fiber).obj U // x_2 ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U })

Tactic:
⟨Over.mk (f ≫ U.hom), Over.homMk f, hf, ⟨v, ?_⟩, rfl⟩

Premises used: CategoryTheory.Over.mk, Subtype.mk, CategoryTheory.Over.homMk, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Over.hom, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Φ : Point.{w, v, u} J
X : C
x : Φ.fiber.obj X
U : Over.{v, u} X
R : Sieve.{v, u} U.left
hR : Membership.mem (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left) R
Y : C
f : Y ⟶ U.left
hf : R.arrows f
v : Φ.fiber.obj Y
hu :
  Membership.mem (α := (Over.forget X ⋙ Φ.fiber).obj U) ((FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
        v :
      (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
refine :
  Membership.mem (γ := Set ((Over.forget X ⋙ Φ.fiber).obj (Over.mk (f ≫ U.hom))))
    ((FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj (Over.mk (f ≫ U.hom))) v
⊢ ∃ (Y_1 : Over.{v, u} X) (f_1 : Y_1 ⟶ U) (_ :
    Sieve.arrows (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) R) f_1) (y :
    (FunctorToTypes.fromOverFunctor Φ.fiber x).obj Y_1),
    Eq (α := (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj U))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((FunctorToTypes.fromOverFunctor Φ.fiber x).map f_1) :
            (a : (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj Y_1)) →
              (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj U))
          y :
        (fun (X : Type w) ↦ X) ((FunctorToTypes.fromOverFunctor Φ.fiber x).obj U))
      (Subtype.mk (p := fun (x_2 : (Over.forget X ⋙ Φ.fiber).obj U) ↦
          x_2 ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
              (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
            v)
          hu :
        { x_2 : (Over.forget X ⋙ Φ.fiber).obj U // x_2 ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U })

Tactic:
refine ⟨Over.mk (f ≫ U.hom), Over.homMk f, hf, ⟨v, ?_⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Point.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Φ : Point.{w, v, u} J
X : C
x : Φ.fiber.obj X
U : Over.{v, u} X
R : Sieve.{v, u} U.left
hR : Membership.mem (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left) R
Y : C
f : Y ⟶ U.left
hf : R.arrows f
v : Φ.fiber.obj Y
hu :
  Membership.mem (α := (Over.forget X ⋙ Φ.fiber).obj U) ((FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
        v :
      (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
rw :
  ∀
    (hu :
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map U.hom) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
                (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
              v :
            (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left)) =
        x),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map (Over.mk (f ≫ U.hom)).hom) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (Over.mk (f ≫ U.hom)).left)) →
            (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
        v =
      x
⊢ Membership.mem (γ := Set ((Over.forget X ⋙ Φ.fiber).obj (Over.mk (f ≫ U.hom))))
    ((FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj (Over.mk (f ≫ U.hom))) v

Tactic:
rw [FunctorToTypes.mem_fromOverSubfunctor_iff] at hu ⊢

Premises used: CategoryTheory.FunctorToTypes.mem_fromOverSubfunctor_iff
-- Module: Mathlib.CategoryTheory.Sites.Point.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Φ : Point.{w, v, u} J
X : C
x : Φ.fiber.obj X
U : Over.{v, u} X
R : Sieve.{v, u} U.left
hR : Membership.mem (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left) R
Y : C
f : Y ⟶ U.left
hf : R.arrows f
v : Φ.fiber.obj Y
hu :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map U.hom) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left))
          v :
        (fun (X : Type w) ↦ X) (Φ.fiber.obj U.left)) =
    x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map (Over.mk (f ≫ U.hom)).hom) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (Over.mk (f ≫ U.hom)).left)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
      v =
    x

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Sites.Point.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Φ : Point.{w, v, u} J
X_1 : C
x : Φ.fiber.obj X_1
inst_2 : J.HasEnoughPoints
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
inst_4 : HasSheafify J (Type w)
X : C
inst_5 : HasSheafify (J.over X) (Type w)
obtain :
  ∀ (P : ObjectProperty (Point.{w, v, u} J)),
    ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P →
      ∀ (hP : P.IsConservativeFamilyOfPoints), (J.over X).HasEnoughPoints
⊢ (J.over X).HasEnoughPoints

Tactic:
obtain ⟨P, _, hP⟩ := HasEnoughPoints.exists_objectProperty J

Premises used: CategoryTheory.GrothendieckTopology.HasEnoughPoints.exists_objectProperty
-- Module: Mathlib.CategoryTheory.Sites.Point.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Φ : Point.{w, v, u} J
X_1 : C
x : Φ.fiber.obj X_1
inst_2 : J.HasEnoughPoints
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
inst_4 : HasSheafify J (Type w)
X : C
inst_5 : HasSheafify (J.over X) (Type w)
P : ObjectProperty (Point.{w, v, u} J)
left : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
hP : P.IsConservativeFamilyOfPoints
⊢ (J.over X).HasEnoughPoints

Tactic:
⟨_, inferInstance, hP.over X⟩

Premises used: inferInstance, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.over, And.intro, Exists.intro, CategoryTheory.GrothendieckTopology.HasEnoughPoints.mk
-- Module: Mathlib.CategoryTheory.Sites.Point.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Φ : Point.{w, v, u} J
X_1 : C
x : Φ.fiber.obj X_1
inst_2 : J.HasEnoughPoints
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
inst_4 : HasSheafify J (Type w)
X : C
inst_5 : HasSheafify (J.over X) (Type w)
P : ObjectProperty (Point.{w, v, u} J)
left : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
hP : P.IsConservativeFamilyOfPoints
⊢ (J.over X).HasEnoughPoints

Tactic:
exact ⟨_, inferInstance, hP.over X⟩
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X U : C
R : Sieve.{v, u} U
hR : R ∈ (⊥ : (a : C) → Set (Sieve a)) U
x : Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) U
⊢ R = ⊤

Tactic:
simpa using hR
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X U : C
R : Sieve.{v, u} U
hR : R ∈ (⊥ : (a : C) → Set (Sieve a)) U
x : Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) U
obtain :
  ∀ (hR : ⊤ ∈ (⊥ : (a : C) → Set (Sieve a)) U),
    ∃ (Y : C) (f : Y ⟶ U) (_ : Sieve.arrows ⊤ f) (y :
      Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun)
              (Functor.map (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) f) :
            (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.flip.obj (op X)).obj Y)) →
              (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U))
          y =
        x
⊢ ∃ (Y : C) (f : Y ⟶ U) (_ : R.arrows f) (y :
    Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) f) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.flip.obj (op X)).obj Y)) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U))
        y =
      x

Tactic:
obtain rfl : R = ⊤ := by simpa using hR

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X U : C
x : Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) U
hR : ⊤ ∈ (⊥ : (a : C) → Set (Sieve a)) U
⊢ Sieve.arrows.{v, u} ⊤ (𝟙 U)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X U : C
x : Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) U
hR : ⊤ ∈ (⊥ : (a : C) → Set (Sieve a)) U
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) (𝟙 U)) :
        (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U)) →
          (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U))
      x =
    x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X U : C
x : Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) U
hR : ⊤ ∈ (⊥ : (a : C) → Set (Sieve a)) U
⊢ ∃ (Y : C) (f : Y ⟶ U) (_ : Sieve.arrows ⊤ f) (y :
    Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map (Functor.obj (Functor.flip shrinkYoneda.{w, v, u}) (op X)) f) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.flip.obj (op X)).obj Y)) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U))
        y =
      x

Tactic:
exact ⟨U, 𝟙 _, by simp, x, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
A : Type u_1
inst_2 : Category.{u_2, u_1} A
inst_3 : HasColimitsOfSize.{w, w, u_2, u_1} A
rw :
  ∀ (X_1 : Functor.{v, u_2, u, u_1} Cᵒᵖ A),
    IsIso (Y := Functor.obj (Point.presheafFiber (pointBot X)) X_1)
      (NatTrans.app
        (Point.toPresheafFiberNatTrans (pointBot X) X
          ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
            (𝟙 X)))
        X_1)
⊢ IsIso (C := Functor.{v, u_2, u, u_1} Cᵒᵖ A ⥤ A) (Y := Point.presheafFiber (pointBot X))
    (Point.toPresheafFiberNatTrans (pointBot X) X
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (𝟙 X)))

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
A : Type u_1
inst_2 : Category.{u_2, u_1} A
inst_3 : HasColimitsOfSize.{w, w, u_2, u_1} A
⊢ ∀ (X_1 : Functor.{v, u_2, u, u_1} Cᵒᵖ A),
    IsIso (Y := Functor.obj (Point.presheafFiber (pointBot X)) X_1)
      (NatTrans.app
        (Point.toPresheafFiberNatTrans (pointBot X) X
          ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
            (𝟙 X)))
        X_1)

Tactic:
fun _ ↦ (colimit.isColimit _).isIso_ι_app_of_isTerminal _
    (Functor.Elements.isInitialElementsMkShrinkYonedaObjObjEquivId X).op

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.flip, CategoryTheory.Functor.Elements, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber, CategoryTheory.shrinkYoneda, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.Elements.isInitialElementsMkShrinkYonedaObjObjEquivId, CategoryTheory.CategoryOfElements.π, CategoryTheory.Limits.colimit, Opposite.op, CategoryTheory.shrinkYonedaObjObjEquiv, CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal, Sigma.mk, CategoryTheory.GrothendieckTopology.pointBot, CategoryTheory.Limits.IsInitial.op, Equiv.symm, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.GrothendieckTopology.Point.fiber, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : Small.{w, u} C
⊢ ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} (C := Point.{w, v, u} (C := C) ⊥)
    (ObjectProperty.ofObj pointBot)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
S : Sieve.{v, u} X
hS :
  ∀ (Φ : ObjectProperty.FullSubcategory (C := Point.{w, v, u} (C := C) ⊥) (pointsBot C))
    (x : Φ.obj (P := pointsBot C).fiber.obj X),
    ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := pointsBot C).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsBot C).fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
obtain :
  ∀ (Y : C) (a : Y ⟶ X) (ha : S.arrows a)
    (b :
      Functor.obj.{v, w, u, w + 1}
        (Point.fiber
          (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
            (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) ⋯)))
        Y)
    (hb :
      Eq (α :=
        (fun (X : Type w) ↦ X)
          (Functor.obj.{v, w, u, w + 1}
            (Point.fiber
              (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
                (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) ⋯)))
            X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Functor.map
                  (Point.fiber
                    (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
                      (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) ⋯)))
                  a) :
              (a : (fun (X : Type w) ↦ X) ({ obj := pointBot X, property := ⋯ }.obj.fiber.obj Y)) →
                (fun (X : Type w) ↦ X) ({ obj := pointBot X, property := ⋯ }.obj.fiber.obj X))
            b :
          (fun (X : Type w) ↦ X)
            (Functor.obj.{v, w, u, w + 1}
              (Point.fiber
                (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
                  (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) ⋯)))
              X))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
            (𝟙 X) :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))),
    S ∈ (⊥ : (a : C) → Set (Sieve a)) X
⊢ S ∈ (⊥ : (a : C) → Set (Sieve a)) X

Tactic:
obtain ⟨Y, a, ha, b, hb⟩ := hS ⟨_, ⟨X⟩⟩ (shrinkYonedaObjObjEquiv.symm (𝟙 X))

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.CategoryStruct.id, CategoryTheory.ObjectProperty.ofObj.mk, CategoryTheory.shrinkYonedaObjObjEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
S : Sieve.{v, u} X
hS :
  ∀ (Φ : ObjectProperty.FullSubcategory (C := Point.{w, v, u} (C := C) ⊥) (pointsBot C))
    (x : Φ.obj (P := pointsBot C).fiber.obj X),
    ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := pointsBot C).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsBot C).fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
Y : C
a : Y ⟶ X
ha : S.arrows a
b : X ⟶ Y
hb :
  Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map shrinkYoneda.{w, v, u} a) (op X)) :
          (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : X ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) b :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : X ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (𝟙 X) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
⊢ b ≫ a = 𝟙 X

Tactic:
have : b ≫ a = 𝟙 _ :=
      shrinkYonedaObjObjEquiv.symm.injective (by
        rw [← hb, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm])
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
S : Sieve.{v, u} X
hS :
  ∀ (Φ : ObjectProperty.FullSubcategory (C := Point.{w, v, u} (C := C) ⊥) (pointsBot C))
    (x : Φ.obj (P := pointsBot C).fiber.obj X),
    ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := pointsBot C).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsBot C).fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
Y : C
a : Y ⟶ X
ha : S.arrows a
b : X ⟶ Y
hb :
  Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map shrinkYoneda.{w, v, u} a) (op X)) :
          (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : X ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) b :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : X ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (𝟙 X) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
this : b ≫ a = 𝟙 X
⊢ S ∈ (⊥ : (a : C) → Set (Sieve a)) X

Tactic:
simpa only [bot_covering, ← Sieve.id_mem_iff_eq_top, this]
      using S.downward_closed ha b

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.GrothendieckTopology.bot_covering, CategoryTheory.Sieve.id_mem_iff_eq_top
-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : LocallySmall.{w, v, u} C_1
C : Type w
inst_2 : SmallCategory C
⊢ HasEnoughPoints.{w, w, w} (C := C) ⊥

Tactic:
⟨_, inferInstance, isConservative_pointsBot C⟩

Premises used: inferInstance, CategoryTheory.GrothendieckTopology.isConservative_pointsBot, And.intro, Exists.intro, CategoryTheory.GrothendieckTopology.HasEnoughPoints.mk