awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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 (α := (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)))
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (hypothesis)
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) (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))
have 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))
Tactic: have h₁ := ConcreteCategory.congr_hom (f₁.hom.naturality f.op) x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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)
⊢ IsLocallySurjective (FA := TypeCat.Fun) φ ↔ Epi φ
have mp : IsLocallySurjective (FA := TypeCat.Fun) φ → Epi φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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 φ
⊢ IsLocallySurjective (FA := TypeCat.Fun) φ ↔ Epi φ
have mpr : Epi φ → IsLocallySurjective (FA := TypeCat.Fun) φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (hypothesis)
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 φ
⊢ IsLocallySurjective (FA := TypeCat.Fun) φ
have this : Epi (imageι φ)
Tactic: have := epi_of_epi_fac (Sheaf.toImage_ι φ)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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ι φ)
⊢ IsLocallySurjective (FA := TypeCat.Fun) φ
have mpr : IsIso (imageι φ)
Tactic: rw [isLocallySurjective_iff_isIso φ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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
⊢ 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)
have 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
Tactic: ext V v
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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 : unop (op U) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g))
      v ↔
    (Sieve.pullback g (Sieve.ofArrows X f)).arrows v
have 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
Tactic: simp only [Sieve.pullback_apply, Sieve.generate_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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
have 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
Tactic: refine ⟨fun hv ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun hv ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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
⊢ ∃ (Y : C) (h : V ⟶ Y) (g_1 : Y ⟶ S), Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g
have 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
Tactic: obtain ⟨w, hw⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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
have 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)))
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 ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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 (α := 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)))
have 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)))
Tactic: rw [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm a (f i), fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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))
have 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
Tactic: refine ⟨fun hf ↦ ⟨fun {U u} ↦ ?_⟩, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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
⊢ 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))
have 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
Tactic: refine ⟨fun hf ↦ ⟨fun {U u} ↦ ?_⟩, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
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))
⊢ 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
have 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
Tactic: obtain ⟨u, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (hypothesis)
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
⊢ 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
have 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))
Tactic: replace hf := J.pullback_stable u hf
Cleared hypotheses: hf