awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
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:
subsingleton
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
⊢ PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ F

Tactic:
haveI := Functor.Final.preservesColimitsOfShape_of_final
    (FinallySmall.fromFilteredFinalModel.{w} (Φ.fiber.Elementsᵒᵖ)) F
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
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))
⊢ 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))

Tactic:
simp only [presheafFiberCompIso]

Premises used: CategoryTheory.GrothendieckTopology.Point.presheafFiberCompIso
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
          (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:
ι_preservesColimitIso_inv F ((CategoryOfElements.π Φ.fiber).op ⋙ P) _

Premises used: CategoryTheory.Functor.op, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber, CategoryTheory.Functor.comp, CategoryTheory.CategoryOfElements.π, CategoryTheory.Limits.colimit, CategoryTheory.ι_preservesColimitIso_inv, CategoryTheory.GrothendieckTopology.Point.fiber
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
          (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:
exact ι_preservesColimitIso_inv F ((CategoryOfElements.π Φ.fiber).op ⋙ P) _

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.comp, CategoryTheory.CategoryOfElements.π, CategoryTheory.ι_preservesColimitIso_inv, CategoryTheory.GrothendieckTopology.Point.fiber
-- Module: Mathlib.CategoryTheory.Sites.Point.Category
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ₁ Φ₂ : Point.{w, v, u} J
f g : Φ₁ ⟶ Φ₂
h : f.hom = g.hom
⊢ f = g

Tactic:
Hom.ext h

Premises used: CategoryTheory.GrothendieckTopology.Point.Hom.ext
-- Module: Mathlib.CategoryTheory.Sites.Point.Category
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
⊢ Hom.hom (𝟙 Φ) = 𝟙 Φ.fiber

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.Category
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ₁ Φ₂ Φ₃ : Point.{w, v, u} J
f : Φ₁ ⟶ Φ₂
g : Φ₂ ⟶ Φ₃
⊢ (f ≫ g).hom = g.hom ≫ f.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.Comap
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
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)))
⊢ ∃ (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

Tactic:
obtain ⟨Y, f, ⟨W, g, h, hg, rfl⟩, y, rfl⟩ :=
      Φ.jointly_surjective (Sieve.functorPushforward F R) (hF.cover_preserve hR) x

Premises used: CategoryTheory.GrothendieckTopology.W, CategoryTheory.GrothendieckTopology.Point.jointly_surjective, CategoryTheory.Sieve.functorPushforward, CategoryTheory.CoverPreserving.cover_preserve, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.Comap
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
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)))
⊢ ∃ (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:
use W, g, hg, Φ.fiber.map h y

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, DFunLike.coe, CategoryTheory.GrothendieckTopology.Point.fiber
-- Module: Mathlib.CategoryTheory.Sites.Point.Comap
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
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)
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))
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ (sheafCompose J (forget A)),
      hP.jointlyReflectIsomorphisms_type.isIso_iff]

Premises used: CategoryTheory.sheafCompose, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms_type, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.forget, CategoryTheory.JointlyReflectIsomorphisms.isIso_iff
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : 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)
⊢ ∀ (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:
fun Φ ↦ ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (Φ.obj.sheafFiberCompIso (forget A))).app (Arrow.mk f))).2
          (inferInstanceAs (IsIso ((forget A).map (Φ.obj.sheafFiber.map f))))

Premises used: Iff.mpr, CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.Limits.colimit, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.forget, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map, CategoryTheory.Iso.app, CategoryTheory.Sheaf, CategoryTheory.Arrow.mk, _private.0.CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms._proof_1, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_7 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
hJ : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
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)
⊢ ∀ (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:
exact fun Φ ↦ ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (Φ.obj.sheafFiberCompIso (forget A))).app (Arrow.mk f))).2
          (inferInstanceAs (IsIso ((forget A).map (Φ.obj.sheafFiber.map f))))

Premises used: Iff.mpr, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.app, CategoryTheory.Sheaf, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_7 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
hJ : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
inst_8 : AB5OfSize.{w, w, v', u'} A
inst_9 : HasFiniteLimits.{v', u'} A
⊢ JointlyReflectMonomorphisms (C := Sheaf.{v, v', u, u'} J A) (D := fun (Φ : P.FullSubcategory) ↦ A)
    fun (Φ : P.FullSubcategory) ↦ GrothendieckTopology.Point.sheafFiber.{w, v, v', u, u'} (Φ.obj (P := P))

Tactic:
(hP.jointlyReflectIsomorphisms A).jointlyReflectMonomorphisms

Premises used: CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectMonomorphisms, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_7 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
hJ : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
inst_8 : HasWeakSheafify.{v, v', u, u'} J A
inst_9 : HasProducts.{w, v', u'} A
⊢ JointlyReflectEpimorphisms (C := Sheaf.{v, v', u, u'} J A) (D := fun (Φ : P.FullSubcategory) ↦ A)
    fun (Φ : P.FullSubcategory) ↦ GrothendieckTopology.Point.sheafFiber.{w, v, v', u, u'} (Φ.obj (P := P))

Tactic:
(hP.jointlyReflectIsomorphisms A).jointlyReflectEpimorphisms

Premises used: CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms, CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectEpimorphisms
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_7 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
hJ : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
inst_8 : AB5OfSize.{w, w, v', u'} A
inst_9 : HasFiniteLimits.{v', u'} A
⊢ JointlyFaithful (C := Sheaf.{v, v', u, u'} J A) (D := fun (Φ : P.FullSubcategory) ↦ A) fun (Φ : P.FullSubcategory) ↦
    GrothendieckTopology.Point.sheafFiber.{w, v, v', u, u'} (Φ.obj (P := P))

Tactic:
(hP.jointlyReflectIsomorphisms A).jointlyFaithful

Premises used: CategoryTheory.JointlyReflectIsomorphisms.jointlyFaithful, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms
-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_4 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_6 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_7 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
hJ : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
inst_8 : HasWeakSheafify.{v, v', u, u'} J A
inst_9 : HasProducts.{w, v', u'} A
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)
⊢ J.W 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]

Premises used: CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms, CategoryTheory.GrothendieckTopology.W_iff, CategoryTheory.JointlyReflectIsomorphisms.isIso_iff