awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst_2 : LocallySmall.{w, v, u} C
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
i : ι
a : V ⟶ X i
hw :
  Eq (α := (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i)) (op V)) :
          (a : (fun (X : Type w) ↦ X) (c.pt.obj (op V))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op V)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation Cᵒᵖ (Type w)) (op V)) c))
                  { as := i : Discrete ι }) :
              (a :
                  (fun (X : Type w) ↦ X)
                    (((Discrete.functor fun (i : ι) ↦ shrinkYoneda.{w, v, u}.obj (X i)) ⋙
                          (evaluation Cᵒᵖ (Type w)).obj (op V)).obj
                      { as := i })) →
                (fun (X : Type w) ↦ X)
                  (((const (Discrete ι)).obj (((evaluation Cᵒᵖ (Type w)).obj (op V)).mapCocone c).pt).obj { as := i }))
            ((Equiv.symm shrinkYonedaObjObjEquiv :
                  (a : unop (op V) ⟶ X { as := i }.as) → (shrinkYoneda.{w, v, u}.obj (X { as := i }.as)).obj (op V))
                a :
              obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} (X { as := i : Discrete ι }.as)) (op V)) :
          (fun (X : Type w) ↦ X)
            (obj
              (obj (const (Discrete ι))
                (Cocone.pt (F :=
                  comp (D := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
                    (Discrete.functor fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i))
                    (obj (evaluation Cᵒᵖ (Type w)) (op V)))
                  (mapCocone (obj (evaluation Cᵒᵖ (Type w)) (op V)) c)))
              { as := i : Discrete ι })) :
      (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj shrinkYoneda.{w, v, u} S) v.op) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op U))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op V)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : U ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g :
          obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op U)) :
      (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))
⊢ ∃ (Y : C) (h : V ⟶ Y) (g_1 : Y ⟶ S), Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g

Tactic:
⟨_, a, _, ⟨i⟩, shrinkYonedaObjObjEquiv.symm.injective ?_⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, And.intro, CategoryTheory.shrinkYonedaObjObjEquiv, Exists.intro, Equiv.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst_2 : LocallySmall.{w, v, u} C
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
Y : C
i : ι
a : V ⟶ X i
fac : a ≫ f i = v ≫ g
⊢ Sieve.arrows
    (imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : U ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g))
    v

Tactic:
⟨(c.inj i).app (op V) (shrinkYonedaObjObjEquiv.symm a),
      (ConcreteCategory.congr_hom (NatTrans.congr_app
      ((Cofan.IsColimit.fac hc (fun i ↦ shrinkYoneda.{w}.map (f i))) i) (op V))
        (shrinkYonedaObjObjEquiv.symm a)).trans ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Cofan.inj, Opposite.op, CategoryTheory.shrinkYonedaObjObjEquiv, Exists.intro, Equiv.symm, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst_2 : LocallySmall.{w, v, u} C
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
Y : C
i : ι
a : V ⟶ X i
fac : a ≫ f i = v ≫ g
h :
  Eq (α := obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map shrinkYoneda.{w, v, u} (f i)) (op V)) :
          (a : (shrinkYoneda.{w, v, u}.obj (X i)).obj (op V)) → (shrinkYoneda.{w, v, u}.obj S).obj (op V))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op V) ⟶ X i) → (shrinkYoneda.{w, v, u}.obj (X i)).obj (op V))
            a :
          obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} (X i)) (op V)) :
      obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj shrinkYoneda.{w, v, u} S) v.op) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op U))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op V)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : U ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g :
          obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op U)) :
      (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))
⊢ Sieve.arrows
    (imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : U ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g))
    v

Tactic:
refine ⟨(c.inj i).app (op V) (shrinkYonedaObjObjEquiv.symm a),
      (ConcreteCategory.congr_hom (NatTrans.congr_app
      ((Cofan.IsColimit.fac hc (fun i ↦ shrinkYoneda.{w}.map (f i))) i) (op V))
        (shrinkYonedaObjObjEquiv.symm a)).trans ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst_2 : LocallySmall.{w, v, u} C
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
Y : C
i : ι
a : V ⟶ X i
fac : a ≫ f i = v ≫ g
h :
  Eq.{w + 1} (α := obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op V) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op V)) (v ≫ g) :
      obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj shrinkYoneda.{w, v, u} S) v.op) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op U))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op V)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : U ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g :
          obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op U)) :
      (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))
⊢ Eq (α := obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map shrinkYoneda.{w, v, u} (f i)) (op V)) :
          (a : (shrinkYoneda.{w, v, u}.obj (X i)).obj (op V)) → (shrinkYoneda.{w, v, u}.obj S).obj (op V))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op V) ⟶ X i) → (shrinkYoneda.{w, v, u}.obj (X i)).obj (op V))
            a :
          obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} (X i)) (op V)) :
      obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj shrinkYoneda.{w, v, u} S) v.op) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op U))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op V)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : U ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g :
          obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op U)) :
      (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))

Tactic:
rw [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm a (f i), fac]

Premises used: CategoryTheory.shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst_2 : LocallySmall.{w, v, u} C
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
Y : C
i : ι
a : V ⟶ X i
fac : a ≫ f i = v ≫ g
⊢ Eq.{w + 1} (α := obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op V) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op V)) (v ≫ g) :
      obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj shrinkYoneda.{w, v, u} S) v.op) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op U))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op V)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : U ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g :
          obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op U)) :
      (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))

Tactic:
(shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm v.op g).symm

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst_2 : LocallySmall.{w, v, u} C
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
Y : C
i : ι
a : V ⟶ X i
fac : a ≫ f i = v ≫ g
⊢ Eq.{w + 1} (α := obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op V) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op V)) (v ≫ g) :
      obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj shrinkYoneda.{w, v, u} S) v.op) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op U))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op V)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : U ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g :
          obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op U)) :
      (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))

Tactic:
exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm v.op g).symm

Premises used: Quiver.Hom.op, CategoryTheory.shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst_2 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
⊢ Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S ↔
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))

Tactic:
⟨fun hf ↦ ⟨fun {U u} ↦ ?_⟩, fun hf ↦ ?_⟩

Premises used: CategoryTheory.Presheaf.IsLocallySurjective.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst_2 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
refine_1 :
  ∀ (hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S) {U : C}
    {u : ToType (FC := TypeCat.Fun) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op U))},
    Presheaf.imageSieve (FA := TypeCat.Fun) (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i)) u ∈
      (J : (a : C) → Set (Sieve a)) U
refine_2 :
  ∀
    (hf :
      Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
        (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))),
    Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
⊢ Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S ↔
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))

Tactic:
refine ⟨fun hf ↦ ⟨fun {U u} ↦ ?_⟩, fun hf ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst_2 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
U : C
u : ToType (FC := TypeCat.Fun) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op U))
refine_1 :
  ∀ (u : unop (op U) ⟶ S),
    Presheaf.imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
        (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) u) ∈
      (J : (a : C) → Set (Sieve a)) U
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i)) u ∈
    (J : (a : C) → Set (Sieve a)) U

Tactic:
obtain ⟨u, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective u

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst_2 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
U : C
u : unop (op U) ⟶ S
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop (op U)))) ((J : (a : C) → Set (Sieve a)) (unop (op U)))
    (Sieve.pullback u (Sieve.ofArrows X f))

Tactic:
replace hf := J.pullback_stable u hf
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst_2 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
U : C
u : unop (op U) ⟶ S
hf :
  Membership.mem (γ := Set (Sieve.{v, u} (unop (op U)))) ((J : (a : C) → Set (Sieve a)) (unop (op U)))
    (Sieve.pullback u (Sieve.ofArrows X f))
refine_1 refine_1₁ refine_1₂ refine_1₃ :
  ∀
    (hf :
      Membership.mem (γ := Set (Sieve.{v, u} (unop (op U)))) ((J : (a : C) → Set (Sieve a)) (unop (op U)))
        (Presheaf.imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
          (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
          ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop (op (unop (op U))) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op (unop (op U))))
            u))),
    Presheaf.imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
        (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) u) ∈
      (J : (a : C) → Set (Sieve a)) U
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) u) ∈
    (J : (a : C) → Set (Sieve a)) U

Tactic:
rwa [← Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map f hc u] at hf

Premises used: CategoryTheory.Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst_2 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
hf :
  Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
    (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
refine_2 :
  Presheaf.imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op S) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op S)) (𝟙 S)) ∈
    (J : (a : C) → Set (Sieve a)) S
⊢ Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S

Tactic:
rw [← Sieve.pullback_id (S := Sieve.ofArrows X f),
      ← Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map f hc (𝟙 S)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map, CategoryTheory.Sieve.pullback_id
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst_2 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
hf :
  Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
    (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op S) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op S)) (𝟙 S)) ∈
    (J : (a : C) → Set (Sieve a)) S

Tactic:
Presheaf.imageSieve_mem J (Cofan.IsColimit.desc hc (fun i ↦ shrinkYoneda.{w}.map (f i)))
      (shrinkYonedaObjObjEquiv.symm (𝟙 S))

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, Set.Mem, CategoryTheory.shrinkYoneda, CategoryTheory.Functor.map, CategoryTheory.Presheaf.imageSieve_mem
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst_2 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
hf :
  Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
    (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op S) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op S)) (𝟙 S)) ∈
    (J : (a : C) → Set (Sieve a)) S

Tactic:
exact Presheaf.imageSieve_mem J (Cofan.IsColimit.desc hc (fun i ↦ shrinkYoneda.{w}.map (f i)))
      (shrinkYonedaObjObjEquiv.symm (𝟙 S))
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Cᵒᵖ ⥤ Type (max w v)) fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i)
hc : IsColimit c
e : Iso (C := Discrete ι ⥤ Cᵒᵖ ⥤ Type (max w v)) (Discrete.functor fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i))
  (Discrete.functor fun (i : ι) ↦ obj shrinkYoneda.{max w v, v, u} (X i)) :=
  Discrete.natIso fun (i : Discrete ι) ↦ Iso.app uliftYonedaIsoShrinkYoneda (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
rw :
  Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{max w v, v, u} S)
      (Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max w v, v, u} (f i)) ↔
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj uliftYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i))
⊢ Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S ↔
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj uliftYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i))

Tactic:
rw [ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map.{max w v} J f hc']
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Cᵒᵖ ⥤ Type (max w v)) fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i)
hc : IsColimit c
e : Iso (C := Discrete ι ⥤ Cᵒᵖ ⥤ Type (max w v)) (Discrete.functor fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i))
  (Discrete.functor fun (i : ι) ↦ obj shrinkYoneda.{max w v, v, u} (X i)) :=
  Discrete.natIso fun (i : Discrete ι) ↦ Iso.app uliftYonedaIsoShrinkYoneda (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
i : ι
rw :
  Eq (α :=
    Quiver.Hom (V := Cᵒᵖ ⥤ Type (max w v)) (obj uliftYoneda.{w, v, u} (X i)) (obj shrinkYoneda.{max w v, v, u} S))
    (NatTrans.app (Iso.hom uliftYonedaIsoShrinkYoneda) (X i) ≫
      Cofan.inj ((Cocone.precompose e.inv).obj c) i ≫
        Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max v w, v, u} (f i))
    (c.inj i ≫ Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max v w, v, u} (f i))
⊢ c.inj i ≫
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i)) ≫
        NatTrans.app (Iso.hom uliftYonedaIsoShrinkYoneda) S =
    c.inj i ≫ Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max v w, v, u} (f i)

Tactic:
rw [Cofan.IsColimit.fac_assoc, NatTrans.naturality,
        ← Cofan.IsColimit.fac hc' (fun i ↦ shrinkYoneda.map (f i)) i]

Premises used: CategoryTheory.shrinkYoneda, CategoryTheory.Functor.map, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.Cofan.IsColimit.fac_assoc, CategoryTheory.Limits.Cofan.IsColimit.fac