awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
inst_4 : IsCofiltered.{v', u'} N
U : N
X : C
f₁ f₂ : p.obj U ⟶ X
hf : Eq.{w + 1} (α := (fiber p).obj X) (fiberMk f₁) (fiberMk f₂)
V : Nᵒᵖ
g : op U ⟶ V
hg :
  Eq (α := (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))
    ((hom (FC := TypeCat.Fun) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).map g) :
          (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj (op U))) →
            (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj V))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop (p.op.obj (op U)) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (p.op.obj (op U)))
            f₁ :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (p.op.obj (op U))) :
      (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))
    ((hom (FC := TypeCat.Fun) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).map g) :
          (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj (op U))) →
            (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj V))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop (p.op.obj (op U)) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (p.op.obj (op U)))
            f₂ :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (p.op.obj (op U))) :
      (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))
⊢ p.map g.unop ≫ f₁ = p.map g.unop ≫ f₂

Tactic:
simpa [shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm.{w}] using hg
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
U V : N
g : V ⟶ U
X : C
f : p.obj U ⟶ X
⊢ Eq.{w + 1} (α := (fiber p).obj X) (fiberMk (p.map g ≫ f)) (fiberMk f)

Tactic:
simp [fiberMk, ← dsimp% congr_hom (colimit.w (p.op ⋙ shrinkYoneda.{w}.obj X) g.op)
        (shrinkYonedaObjObjEquiv.symm f),
    fiber, shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm.{w}]

Premises used: CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
U V : N
g : V ⟶ U
⊢ Eq.{w + 1} (α := (fiber p).obj (p.obj U)) (fiberMk (p.map g)) (fiberMk (𝟙 (p.obj U)))

Tactic:
simpa using fiberMk_map_comp (p := p) g (𝟙 (p.obj U))

Premises used: CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_map_comp, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
U : N
X : C
f : p.obj U ⟶ X
Y : C
g : X ⟶ Y
⊢ Eq (α := colimit (p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} Y))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app (p.op.whiskerLeft (Functor.map shrinkYoneda.{w, v, u} g)) (op U) ≫
              colimit.ι (p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} Y) (op U)) :
          (a : (p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj (op U)) → colimit (p.op ⋙ shrinkYoneda.{w, v, u}.obj Y))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop (op (p.1 U)) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op (p.1 U)))
            f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op (p.1 U))) :
      colimit (p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} Y))
    (fiberMk (f ≫ g) : (fiber p).obj Y)

Tactic:
simp [fiberMk, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]

Premises used: CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
U V : N
f : U ⟶ V
⊢ (hom (FC := TypeCat.Fun) ((fiber p).map (p.map f)) :
        (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((fiber p).elementsMk (p.obj U) (fiberMk (𝟙 (p.obj U)))).fst)) →
          (fun (X : Type w) ↦ X) ((fiber p).obj ((fiber p).elementsMk (p.obj V) (fiberMk (𝟙 (p.obj V)))).fst))
      (((fiber p).elementsMk (p.obj U) (fiberMk (𝟙 (p.obj U)))).snd (β := fun (c : C) ↦ (fiber p).obj c)) =
    ((fiber p).elementsMk (p.obj V) (fiberMk (𝟙 (p.obj V)))).snd (β := fun (c : C) ↦ (fiber p).obj c)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
⊢ Functor.Initial (D := (fiber p).Elements) (functor p)

Tactic:
Functor.initial_of_exists_of_isCofiltered _ ?_ ?_

Premises used: CategoryTheory.Functor.initial_of_exists_of_isCofiltered
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
refine_1 : ∀ (d : (fiber p).Elements), ∃ (c : N), Nonempty.{v + 1} (Functor.obj (functor p) c ⟶ d)
refine_2 :
  ∀ {d : (fiber p).Elements} {c : N} (s s' : Functor.obj (functor p) c ⟶ d),
    ∃ (c' : N) (t : c' ⟶ c), Functor.map (functor p) t ≫ s = Functor.map (functor p) t ≫ s'
⊢ Functor.Initial (D := (fiber p).Elements) (functor p)

Tactic:
refine Functor.initial_of_exists_of_isCofiltered _ ?_ ?_

Premises used: CategoryTheory.Functor.initial_of_exists_of_isCofiltered
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
X : C
x : (fiber p).obj X
refine_1 :
  ∀ (U : N) (f : p.obj U ⟶ X),
    ∃ (c : N),
      Nonempty.{v + 1}
        (Quiver.Hom (V := (fiber p).Elements) (Functor.obj (functor p) c)
          (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))
⊢ ∃ (c : N), Nonempty.{v + 1} (Functor.obj (functor p) c ⟶ Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X x)

Tactic:
obtain ⟨U, f, rfl⟩ := fiberMk_jointly_surjective x

Premises used: CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
X : C
U : N
f : p.obj U ⟶ X
⊢ Eq (α :=
    (fun (X : Type w) ↦ X)
      ((fiber p).obj
        (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
    ((hom (FC := TypeCat.Fun) ((fiber p).map f) :
          (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((functor p).obj U).fst)) →
            (fun (X : Type w) ↦ X) ((fiber p).obj ⟨X, fiberMk f⟩.fst))
        (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) U)) :
      (fun (X : Type w) ↦ X)
        ((fiber p).obj
          (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
            (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
    (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)) :
      (fiber p).obj
        (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
X : C
U : N
f : p.obj U ⟶ X
⊢ ∃ (c : N),
    Nonempty.{v + 1}
      (Quiver.Hom (V := (fiber p).Elements) (Functor.obj (functor p) c)
        (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))

Tactic:
exact ⟨U, f, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
X : C
V U : N
f : p.obj U ⟶ X
φ₁ :
  Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V) ⟶
    Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f))
hφ₁ :
  Eq (α :=
    (fun (X : Type w) ↦ X)
      ((fiber p).obj
        (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
    ((hom (FC := TypeCat.Fun) ((fiber p).map φ₁) :
          (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((functor p).obj V).fst)) →
            (fun (X : Type w) ↦ X) ((fiber p).obj ⟨X, fiberMk f⟩.fst))
        (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V)) :
      (fun (X : Type w) ↦ X)
        ((fiber p).obj
          (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
            (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
    (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)) :
      (fiber p).obj
        (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f))))
φ₂ :
  Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V) ⟶
    Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f))
hφ₂ :
  Eq (α :=
    (fun (X : Type w) ↦ X)
      ((fiber p).obj
        (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
    ((hom (FC := TypeCat.Fun) ((fiber p).map φ₂) :
          (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((functor p).obj V).fst)) →
            (fun (X : Type w) ↦ X) ((fiber p).obj ⟨X, fiberMk f⟩.fst))
        (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V)) :
      (fun (X : Type w) ↦ X)
        ((fiber p).obj
          (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
            (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
    (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)) :
      (fiber p).obj
        (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f))))
⊢ Eq.{w + 1} (α :=
    (fiber p).obj
      (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f))))
    (fiberMk φ₁) (fiberMk φ₂)

Tactic:
simpa using hφ₁.trans hφ₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
⊢ InitiallySmall (fiber p).Elements

Tactic:
initiallySmall_of_initial_of_initiallySmall (functor.{w} p)

Premises used: CategoryTheory.initiallySmall_of_initial_of_initiallySmall, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
⊢ IsCofiltered (fiber p).Elements

Tactic:
IsCofiltered.of_initial (functor.{w} p)

Premises used: CategoryTheory.IsCofiltered.of_initial, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
hp :
  ∀ ⦃X : C⦄,
    ∀ R ∈ (J : (a : C) → Set (Sieve a)) X,
      ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), a ≫ g = p.map q ≫ f
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
x : (ofIsCofiltered.fiber p).obj X
obtain :
  ∀ (U : N) (f : p.obj U ⟶ X),
    ∃ (Y : C) (f_1 : Y ⟶ X) (_ : R.arrows f_1) (y : (ofIsCofiltered.fiber p).obj Y),
      Eq (α := (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
        ((hom (FC := TypeCat.Fun) ((ofIsCofiltered.fiber p).map f_1) :
              (a : (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj Y)) →
                (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
            y :
          (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
        (fiberMk f : (ofIsCofiltered.fiber p).obj X)
⊢ ∃ (Y : C) (f : Y ⟶ X) (_ : R.arrows f) (y : (ofIsCofiltered.fiber p).obj Y),
    (hom (FC := TypeCat.Fun) ((ofIsCofiltered.fiber p).map f) :
          (a : (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj Y)) →
            (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
        y =
      x

Tactic:
obtain ⟨U, f, rfl⟩ := fiberMk_jointly_surjective x

Premises used: CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
hp :
  ∀ ⦃X : C⦄,
    ∀ R ∈ (J : (a : C) → Set (Sieve a)) X,
      ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), a ≫ g = p.map q ≫ f
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
U : N
f : p.obj U ⟶ X
obtain :
  ∀ (Y : C) (g : Y ⟶ X) (hg : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y) (ha : a ≫ g = p.map q ≫ f),
    ∃ (Y : C) (f_1 : Y ⟶ X) (_ : R.arrows f_1) (y : (ofIsCofiltered.fiber p).obj Y),
      Eq (α := (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
        ((hom (FC := TypeCat.Fun) ((ofIsCofiltered.fiber p).map f_1) :
              (a : (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj Y)) →
                (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
            y :
          (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
        (fiberMk f : (ofIsCofiltered.fiber p).obj X)
⊢ ∃ (Y : C) (f_1 : Y ⟶ X) (_ : R.arrows f_1) (y : (ofIsCofiltered.fiber p).obj Y),
    Eq (α := (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
      ((hom (FC := TypeCat.Fun) ((ofIsCofiltered.fiber p).map f_1) :
            (a : (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj Y)) →
              (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
          y :
        (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
      (fiberMk f : (ofIsCofiltered.fiber p).obj X)

Tactic:
obtain ⟨Y, g, hg, V, q, a, ha⟩ := hp R hR f
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
hp :
  ∀ ⦃X : C⦄,
    ∀ R ∈ (J : (a : C) → Set (Sieve a)) X,
      ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), a ≫ g = p.map q ≫ f
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
U : N
f : p.obj U ⟶ X
Y : C
g : Y ⟶ X
hg : R.arrows g
V : N
q : V ⟶ U
a : p.obj V ⟶ Y
ha : a ≫ g = p.map q ≫ f
⊢ Eq (α := (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
    ((hom (FC := TypeCat.Fun) ((ofIsCofiltered.fiber p).map g) :
          (a : (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj Y)) →
            (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
        (fiberMk a) :
      (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
    (fiberMk f : (ofIsCofiltered.fiber p).obj X)

Tactic:
simp [ha]
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
hp :
  ∀ ⦃X : C⦄,
    ∀ R ∈ (J : (a : C) → Set (Sieve a)) X,
      ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), a ≫ g = p.map q ≫ f
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
U : N
f : p.obj U ⟶ X
Y : C
g : Y ⟶ X
hg : R.arrows g
V : N
q : V ⟶ U
a : p.obj V ⟶ Y
ha : a ≫ g = p.map q ≫ f
⊢ ∃ (Y : C) (f_1 : Y ⟶ X) (_ : R.arrows f_1) (y : (ofIsCofiltered.fiber p).obj Y),
    Eq (α := (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
      ((hom (FC := TypeCat.Fun) ((ofIsCofiltered.fiber p).map f_1) :
            (a : (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj Y)) →
              (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
          y :
        (fun (X : Type w) ↦ X) ((ofIsCofiltered.fiber p).obj X))
      (fiberMk f : (ofIsCofiltered.fiber p).obj X)

Tactic:
exact ⟨Y, g, hg, fiberMk a, by simp [ha]⟩
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
hp :
  ∀ ⦃X : C⦄,
    ∀ R ∈ (J : (a : C) → Set (Sieve a)) X,
      ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), a ≫ g = p.map q ≫ f
A : Type u''
inst_5 : Category.{v'', u''} A
inst_6 : HasColimitsOfSize.{w, w, v'', u''} A
V U : N
f : V ⟶ U
P : Functor.{v, v'', u, u''} Cᵒᵖ A
⊢ Eq (α := P.obj (op (p.obj U)) ⟶ Functor.obj (ofIsCofiltered p hp).presheafFiber P)
    (P.map (p.map f).op ≫ toPresheafFiberOfIsCofiltered p hp V P) (toPresheafFiberOfIsCofiltered p hp U P)

Tactic:
simp [toPresheafFiberOfIsCofiltered]

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
inst_4 : IsCofiltered.{v', u'} N
hp :
  ∀ ⦃X : C⦄,
    ∀ R ∈ (J : (a : C) → Set (Sieve a)) X,
      ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), a ≫ g = p.map q ≫ f
A : Type u''
inst_5 : Category.{v'', u''} A
inst_6 : HasColimitsOfSize.{w, w, v'', u''} A
P Q : Functor.{v, v'', u, u''} Cᵒᵖ A
g : P ⟶ Q
U : N
⊢ Eq (α := P.obj (op (p.obj U)) ⟶ Functor.obj (ofIsCofiltered p hp).presheafFiber Q)
    (toPresheafFiberOfIsCofiltered p hp U P ≫ Functor.map (ofIsCofiltered p hp).presheafFiber g)
    (g.app (op (p.obj U)) ≫ toPresheafFiberOfIsCofiltered p hp U Q)

Tactic:
simp [toPresheafFiberOfIsCofiltered]

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered
-- 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 U
hR : R ∈ (J.over X : (a : Over X) → Set (Sieve a)) U
u : (Over.forget X ⋙ Φ.fiber).obj U
hu : u ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U
obtain :
  ∀ (R : Sieve.{v, u} U.left)
    (hR :
      Membership.mem (α := Sieve U) ((J.over X : (a : Over X) → Set (Sieve a)) U)
        (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) R : Sieve 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
⊢ ∃ (Y : Over.{v, u} X) (f : Y ⟶ U) (_ : R.arrows 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 ⟨R, rfl⟩ := (Sieve.overEquiv _).symm.surjective R

Premises used: CategoryTheory.Sieve.overEquiv, Equiv.surjective, Equiv.symm, 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
u : (Over.forget X ⋙ Φ.fiber).obj U
hu : u ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U
R : Sieve.{v, u} U.left
hR :
  Membership.mem (α := Sieve U) ((J.over X : (a : Over X) → Set (Sieve a)) U)
    (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) R : Sieve U)
⊢ Membership.mem (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left) R

Tactic:
simp only [mem_over_iff, Equiv.apply_symm_apply] at hR

Premises used: Equiv.apply_symm_apply, CategoryTheory.GrothendieckTopology.mem_over_iff