awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
rw :
  IsIso (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι ↔
    IsIso (C := Sheaf J (Type w)) (X := image f) (Y := G) { hom := (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι }
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f.hom ↔ IsIso (imageι f)

Tactic:
rw [Sheaf.imageι, Presheaf.isLocallySurjective_iff_range_sheafify_eq_top',
    Subfunctor.eq_top_iff_isIso]

Premises used: CategoryTheory.Sheaf.imageι, CategoryTheory.Subfunctor.eq_top_iff_isIso, CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top'
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι ↔
    IsIso (C := Sheaf J (Type w)) (X := image f) (Y := G) { hom := (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι }

Tactic:
isIso_iff_of_reflects_iso (f := Sheaf.imageι f) (F := sheafToPresheaf J (Type w))

Premises used: CategoryTheory.Sheaf.imageι, Set.Mem, setOf, CategoryTheory.Subfunctor.toFunctor, CategoryTheory.Subfunctor.ι, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι ↔
    IsIso (C := Sheaf J (Type w)) (X := image f) (Y := G) { hom := (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι }

Tactic:
exact isIso_iff_of_reflects_iso (f := Sheaf.imageι f) (F := sheafToPresheaf J (Type w))
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F₁_1 F₂_1 F₃ : Sheaf.{v, v', u, u'} J A
φ_1 : F₁_1 ⟶ F₂_1
ψ : F₂_1 ⟶ F₃
inst_4 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst_5 : IsLocallySurjective (FA := TypeCat.Fun) φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
h₁ :
  ∀ (X : Cᵒᵖ) (x : F₂.obj (P := Presheaf.IsSheaf J).obj X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app X)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.hom.app X)).toFun x
⊢ f₁ = f₂

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F₁_1 F₂_1 F₃ : Sheaf.{v, v', u, u'} J A
φ_1 : F₁_1 ⟶ F₂_1
ψ : F₂_1 ⟶ F₃
inst_4 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst_5 : IsLocallySurjective (FA := TypeCat.Fun) φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj (P := Presheaf.IsSheaf J).obj X
h₁ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop X⦄,
    (Presheaf.imageSieve (FA := TypeCat.Fun) φ.hom x).arrows f →
      Eq (α := (fun (X : Type w) ↦ X) (Z.obj (P := Presheaf.IsSheaf J).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Z.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : (fun (X : Type w) ↦ X) (Z.obj.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (Z.obj.obj (op Y)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app X)).toFun x) :
          (fun (X : Type w) ↦ X) (Z.obj (P := Presheaf.IsSheaf J).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Z.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : (fun (X : Type w) ↦ X) (Z.obj.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (Z.obj.obj (op Y)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.hom.app X)).toFun x) :
          (fun (X : Type w) ↦ X) (Z.obj (P := Presheaf.IsSheaf J).obj (op Y)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.hom.app X)).toFun x

Tactic:
apply (((isSheaf_iff_isSheaf_of_type _ _).1 Z.2).isSeparated _
      (Presheaf.imageSieve_mem J φ.hom x)).ext

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.isSheaf_iff_isSheaf_of_type, Iff.mp, CategoryTheory.Presieve.IsSheaf.isSeparated, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Presheaf.imageSieve_mem
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F₁_1 F₂_1 F₃ : Sheaf.{v, v', u, u'} J A
φ_1 : F₁_1 ⟶ F₂_1
ψ : F₂_1 ⟶ F₃
inst_4 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst_5 : IsLocallySurjective (FA := TypeCat.Fun) φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj (P := Presheaf.IsSheaf J).obj X
Y : C
f : Y ⟶ unop X
s : F₁.obj (P := Presheaf.IsSheaf J).obj (op Y)
hs :
  Eq (α := (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.hom.app (op Y)) :
          (a : (fun (X : Type w) ↦ X) (F₁.obj.obj (op Y))) → (fun (X : Type w) ↦ X) (F₂.obj.obj (op Y)))
        s :
      (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (fun (X : Type w) ↦ X) (F₂.obj.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (F₂.obj.obj (op Y)))
        x :
      (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
h₁ :
  Eq (α := Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Z.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : Z.obj.obj X) → Z.obj.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app X) : (a : F₂.obj.obj X) → Z.obj.obj X) x :
          Z.obj (P := Presheaf.IsSheaf J).obj X) :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Z.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : Z.obj.obj X) → Z.obj.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.hom.app X) : (a : F₂.obj.obj X) → Z.obj.obj X) x :
          Z.obj (P := Presheaf.IsSheaf J).obj X) :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
⊢ Eq (α := (fun (X : Type w) ↦ X) (Z.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Z.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (fun (X : Type w) ↦ X) (Z.obj.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (Z.obj.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app X)).toFun x) :
      (fun (X : Type w) ↦ X) (Z.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Z.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (fun (X : Type w) ↦ X) (Z.obj.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (Z.obj.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.hom.app X)).toFun x) :
      (fun (X : Type w) ↦ X) (Z.obj (P := Presheaf.IsSheaf J).obj (op Y)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F₁_1 F₂_1 F₃ : Sheaf.{v, v', u, u'} J A
φ_1 : F₁_1 ⟶ F₂_1
ψ : F₂_1 ⟶ F₃
inst_4 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst_5 : IsLocallySurjective (FA := TypeCat.Fun) φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj (P := Presheaf.IsSheaf J).obj X
Y : C
f : Y ⟶ unop X
s : F₁.obj (P := Presheaf.IsSheaf J).obj (op Y)
hs :
  Eq (α := (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.hom.app (op Y)) :
          (a : (fun (X : Type w) ↦ X) (F₁.obj.obj (op Y))) → (fun (X : Type w) ↦ X) (F₂.obj.obj (op Y)))
        s :
      (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (fun (X : Type w) ↦ X) (F₂.obj.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (F₂.obj.obj (op Y)))
        x :
      (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
⊢ Eq (α := Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.obj (P := Presheaf.IsSheaf J).map f.op ≫ f₁.hom.app (op Y)) :
          (a : F₂.obj.obj (op (unop X))) → Z.obj.obj (op Y))
        x :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app (op (unop X)) ≫ Z.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : F₂.obj.obj (op (unop X))) → Z.obj.obj (op Y))
        x :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))

Tactic:
have h₁ := ConcreteCategory.congr_hom (f₁.hom.naturality f.op) x
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F₁_1 F₂_1 F₃ : Sheaf.{v, v', u, u'} J A
φ_1 : F₁_1 ⟶ F₂_1
ψ : F₂_1 ⟶ F₃
inst_4 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst_5 : IsLocallySurjective (FA := TypeCat.Fun) φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj (P := Presheaf.IsSheaf J).obj X
Y : C
f : Y ⟶ unop X
s : F₁.obj (P := Presheaf.IsSheaf J).obj (op Y)
hs :
  Eq (α := (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.hom.app (op Y)) :
          (a : (fun (X : Type w) ↦ X) (F₁.obj.obj (op Y))) → (fun (X : Type w) ↦ X) (F₂.obj.obj (op Y)))
        s :
      (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (fun (X : Type w) ↦ X) (F₂.obj.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (F₂.obj.obj (op Y)))
        x :
      (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
h₁ :
  Eq (α := Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.obj (P := Presheaf.IsSheaf J).map f.op ≫ f₁.hom.app (op Y)) :
          (a : F₂.obj.obj (op (unop X))) → Z.obj.obj (op Y))
        x :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app (op (unop X)) ≫ Z.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : F₂.obj.obj (op (unop X))) → Z.obj.obj (op Y))
        x :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
⊢ Eq (α := Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.obj (P := Presheaf.IsSheaf J).map f.op ≫ f₂.hom.app (op Y)) :
          (a : F₂.obj.obj (op (unop X))) → Z.obj.obj (op Y))
        x :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.hom.app (op (unop X)) ≫ Z.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : F₂.obj.obj (op (unop X))) → Z.obj.obj (op Y))
        x :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))

Tactic:
have h₂ := ConcreteCategory.congr_hom (f₂.hom.naturality f.op) x
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F₁ F₂ F₃ : Sheaf.{v, v', u, u'} J A
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst_4 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
inst_5 : IsLocallySurjective (FA := FA) (CA := CA) φ
⊢ Epi φ

Tactic:
(sheafCompose J (forget A)).epi_of_epi_map inferInstance

Premises used: CategoryTheory.sheafCompose, inferInstance, CategoryTheory.forget, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst_1 : HasSheafify J (Type w)
mp : IsLocallySurjective (FA := TypeCat.Fun) φ → Epi φ
mpr : Epi φ → IsLocallySurjective (FA := TypeCat.Fun) φ
⊢ IsLocallySurjective (FA := TypeCat.Fun) φ ↔ Epi φ

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst_1 : HasSheafify J (Type w)
h : IsLocallySurjective (FA := TypeCat.Fun) φ
⊢ Epi φ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst_1 : HasSheafify J (Type w)
h : Epi φ
⊢ Epi (imageι φ)

Tactic:
have := epi_of_epi_fac (Sheaf.toImage_ι φ)
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst_1 : HasSheafify J (Type w)
h : Epi φ
this : Epi (imageι φ)
mpr : IsIso (imageι φ)
⊢ IsLocallySurjective (FA := TypeCat.Fun) φ

Tactic:
rw [isLocallySurjective_iff_isIso φ]

Premises used: CategoryTheory.Sheaf.isLocallySurjective_iff_isIso
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst_1 : HasSheafify J (Type w)
h : Epi φ
this : Epi (imageι φ)
⊢ IsIso (imageι φ)

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
R R' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
φ : R ⟶ R'
X : Cᵒᵖ
r' : R'.obj X
⊢ ((localPreimage φ r').map (R := (Presheaf.imageSieve (FA := TypeCat.Fun) φ r').arrows) φ).IsAmalgamation (R :=
    (Presheaf.imageSieve (FA := TypeCat.Fun) φ r').arrows) r'

Tactic:
fun _ f hf => (Presheaf.app_localPreimage φ r' f hf).symm

Premises used: CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation
-- 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
h :
  ∀ ⦃V : C⦄ (v : V ⟶ U),
    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 : unop (op U) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g))
        v ↔
      (Sieve.pullback g (Sieve.ofArrows X f)).arrows v
⊢ 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)) g) =
    Sieve.pullback g (Sieve.ofArrows X f)

Tactic:
ext V v
-- 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
h :
  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 ↔
    ∃ (Y : C) (h : V ⟶ Y) (g_1 : Y ⟶ S), Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = 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 : unop (op U) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g))
      v ↔
    (Sieve.pullback g (Sieve.ofArrows X f)).arrows v

Tactic:
simp only [Sieve.pullback_apply, Sieve.generate_apply]

Premises used: CategoryTheory.Sieve.pullback_apply, CategoryTheory.Sieve.generate_apply
-- 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
⊢ 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 ↔
    ∃ (Y : C) (h : V ⟶ Y) (g_1 : Y ⟶ S), Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g

Tactic:
⟨fun hv ↦ ?_, ?_⟩

Premises used: Iff.intro
-- 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
h :
  ∀
    (hv :
      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),
    ∃ (Y : C) (h : V ⟶ Y) (g_1 : Y ⟶ S), Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g
h₁ :
  (∃ (Y : C) (h : V ⟶ Y) (g_1 : Y ⟶ S), Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = 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
⊢ 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 ↔
    ∃ (Y : C) (h : V ⟶ Y) (g_1 : Y ⟶ S), Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g

Tactic:
refine ⟨fun hv ↦ ?_, ?_⟩
-- 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
hv :
  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
h :
  ∀ (w : ToType (FC := TypeCat.Fun) (c.pt.obj (op V)))
    (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)))
            w :
          (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
⊢ ∃ (Y : C) (h : V ⟶ Y) (g_1 : Y ⟶ S), Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g

Tactic:
obtain ⟨w, hw⟩ := hv

Premises used: CategoryTheory.Presheaf.w