awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X)
this :
  ∀ (X : C)
    (y : ToType (FC := TypeCat.Fun) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
      ToType (FC := TypeCat.Fun) ((F.obj (op n.succ)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))),
      Eq (α := (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map (homOfLE ⋯).op).hom.app (op X')) :
              (a : (F.obj (op n.succ)).obj.obj (op X')) → (F.obj (op n)).obj.obj (op X'))
            x :
          (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map (op φ)) :
              (a : (F.obj (op n)).obj.obj (op X)) → (F.obj (op n)).obj.obj (op X'))
            y :
          (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
    (F.obj (op (n + 1))).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')),
    Eq (α := (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (InducedCategory.Hom.hom (F.map (Quiver.Hom.op (homOfLE ⋯)))) (op X')) :
            (a : (fun (X : Type v) ↦ X) ((F.obj (op (n + 1))).obj.obj (op X'))) →
              (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X')))
          x :
        (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map φ.op) :
            (a : (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X))) →
              (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X')))
          y :
        (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))

Tactic:
this X y

Premises used: Quiver.Hom.op
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X)
this :
  ∀ (X : C)
    (y : ToType (FC := TypeCat.Fun) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
      ToType (FC := TypeCat.Fun) ((F.obj (op n.succ)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))),
      Eq (α := (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map (homOfLE ⋯).op).hom.app (op X')) :
              (a : (F.obj (op n.succ)).obj.obj (op X')) → (F.obj (op n)).obj.obj (op X'))
            x :
          (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map (op φ)) :
              (a : (F.obj (op n)).obj.obj (op X)) → (F.obj (op n)).obj.obj (op X'))
            y :
          (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
    (F.obj (op (n + 1))).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')),
    Eq (α := (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (InducedCategory.Hom.hom (F.map (Quiver.Hom.op (homOfLE ⋯)))) (op X')) :
            (a : (fun (X : Type v) ↦ X) ((F.obj (op (n + 1))).obj.obj (op X'))) →
              (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X')))
          x :
        (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map φ.op) :
            (a : (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X))) →
              (fun (X : Type v) ↦ X) ((F.obj (op n)).obj.obj (op X')))
          y :
        (fun (X : Type v) ↦ X) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X')))

Tactic:
exact this X y
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
X : C
y : (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X)
n : ℕ
⊢ Eq (α :=
    Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) (limit (preimageDiagram hF X y)) ⟶ F.obj (op n))
    (CategoryStruct.comp (Y :=
      Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) ((preimageDiagram hF X y).obj (op (n + 1))))
      (Functor.map (GrothendieckTopology.yoneda (coherentTopology C)) (limit.π (preimageDiagram hF X y) (op (n + 1))))
      (Functor.map (GrothendieckTopology.yoneda (coherentTopology C))
          ((preimageDiagram hF X y).map (Quiver.Hom.op (homOfLE ⋯))) ≫
        (Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology C)) :
            (a : (F.obj (op n)).obj.obj (op ((preimageDiagram hF X y).obj (op n)))) →
              (coherentTopology C).yoneda.obj ((preimageDiagram hF X y).obj (op n)) ⟶ F.obj (op n))
          (struct.x (preimageStruct hF X y) n)))
    (CategoryStruct.comp (Y :=
      Functor.obj (GrothendieckTopology.yoneda (coherentTopology C)) ((preimageDiagram hF X y).obj (op (n + 1))))
      (Functor.map (GrothendieckTopology.yoneda (coherentTopology C)) (limit.π (preimageDiagram hF X y) (op (n + 1))))
      (CategoryStruct.comp (Y := F.obj (op (n + 1)))
        ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology C)) :
            (a : (F.obj (op (n + 1))).obj.obj (op ((preimageDiagram hF X y).obj (op (n + 1))))) →
              (coherentTopology C).yoneda.obj ((preimageDiagram hF X y).obj (op (n + 1))) ⟶ F.obj (op (n + 1)))
          (struct.x (preimageStruct hF X y) (n + 1)))
        (F.map (Quiver.Hom.op (homOfLE ⋯)))))

Tactic:
simp [GrothendieckTopology.yonedaEquiv_symm_naturality_left,
      GrothendieckTopology.yonedaEquiv_symm_naturality_right,
      preimageDiagram, (preimageStruct hF X y).w n]

Premises used: _private.0.CategoryTheory.coherentTopology.preimageDiagram, _private.0.CategoryTheory.coherentTopology.preimageStruct, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_left, _private.0.CategoryTheory.coherentTopology.struct.w, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
rw :
  ∀ (X : C)
    (y : ToType (FC := TypeCat.Fun) ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
      ToType (FC := TypeCat.Fun)
        ((Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)).obj (P :=
              Presheaf.IsSheaf (coherentTopology C)).obj
          (op X'))),
      Eq (α := (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (InducedCategory.Hom.hom (c.π.app (op 0))) (op X')) :
              (a : (((Functor.const ℕᵒᵖ).obj c.pt).obj (op 0)).obj.obj (op X')) → (F.obj (op 0)).obj.obj (op X'))
            x :
          (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map (op φ)) :
              (a : (F.obj (op 0)).obj.obj (op X)) → (F.obj (op 0)).obj.obj (op X'))
            y :
          (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
⊢ Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F₁ :=
    Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)) (c.π.app (op 0))

Tactic:
rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff]

Premises used: CategoryTheory.regularTopology.isLocallySurjective_iff, CategoryTheory.coherentTopology.isLocallySurjective_iff
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
X : C
y : ToType (FC := TypeCat.Fun) ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))
n : ℕ
⊢ EffectiveEpi ((preimageDiagram hF X y).map (homOfLE ⋯).op)

Tactic:
simpa [preimageDiagram] using (preimageStruct hF X y).effectiveEpi n

Premises used: _private.0.CategoryTheory.coherentTopology.preimageDiagram, _private.0.CategoryTheory.coherentTopology.preimageStruct, _private.0.CategoryTheory.coherentTopology.struct.effectiveEpi
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
X : C
y : ToType (FC := TypeCat.Fun) ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))
⊢ EffectiveEpi (X := (preimageDiagram hF X y).obj (op 0)) (Y := limit (preimageDiagram hF X y))
    (limit.π (preimageDiagram hF X y) (op 0))

Tactic:
have hh : EffectiveEpi (limit.π (preimageDiagram hF X y) ⟨0⟩) :=
    h _ fun n ↦ by simpa [preimageDiagram] using (preimageStruct hF X y).effectiveEpi n
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
X : C
y : ToType (FC := TypeCat.Fun) ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))
hh :
  EffectiveEpi (X := (preimageDiagram hF X y).obj (op 0)) (Y := limit (preimageDiagram hF X y))
    (limit.π (preimageDiagram hF X y) (op 0))
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
    ToType (FC := TypeCat.Fun)
      ((Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)).obj (P :=
            Presheaf.IsSheaf (coherentTopology C)).obj
        (op X'))),
    Eq (α := (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (InducedCategory.Hom.hom (c.π.app (op 0))) (op X')) :
            (a : (((Functor.const ℕᵒᵖ).obj c.pt).obj (op 0)).obj.obj (op X')) → (F.obj (op 0)).obj.obj (op X'))
          x :
        (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map (op φ)) :
            (a : (F.obj (op 0)).obj.obj (op X)) → (F.obj (op 0)).obj.obj (op X'))
          y :
        (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))

Tactic:
⟨limit (preimageDiagram hF X y), limit.π (preimageDiagram hF X y) ⟨0⟩, hh,
    (coherentTopology C).yonedaEquiv (hc.lift (cone hF X y )),
    (?_ : (c.π.app (op 0)).hom.app _ _ = _)⟩

Premises used: CategoryTheory.Limits.limit.π, _private.0.CategoryTheory.coherentTopology.preimageDiagram, CategoryTheory.GrothendieckTopology.yonedaEquiv, CategoryTheory.Limits.limit, Opposite.op, Exists.intro, OfNat.ofNat, DFunLike.coe, _private.0.CategoryTheory.coherentTopology.cone, CategoryTheory.Limits.IsLimit.lift, CategoryTheory.coherentTopology
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
X : C
y : ToType (FC := TypeCat.Fun) ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))
hh :
  EffectiveEpi (X := (preimageDiagram hF X y).obj (op 0)) (Y := limit (preimageDiagram hF X y))
    (limit.π (preimageDiagram hF X y) (op 0))
⊢ Eq (α := (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op (limit (preimageDiagram hF X y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (InducedCategory.Hom.hom
                ((Equiv.symm (GrothendieckTopology.yonedaEquiv (coherentTopology C)) :
                    (a : (F.obj (op 0)).obj.obj (op ((preimageDiagram hF X y).obj (op 0)))) →
                      (coherentTopology C).yoneda.obj ((preimageDiagram hF X y).obj (op 0)) ⟶ F.obj (op 0))
                  (struct.x (preimageStruct hF X y) 0)))
              (op (limit (preimageDiagram hF X y)))) :
          (a :
              ((coherentTopology C).yoneda.obj ((preimageDiagram hF X y).obj (op 0))).obj.obj
                (op (limit (preimageDiagram hF X y)))) →
            (F.obj (op 0)).obj.obj (op (limit (preimageDiagram hF X y))))
        (limit.π (preimageDiagram hF X y) (op 0)) :
      (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op (limit (preimageDiagram hF X y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map
              (op (limit.π (preimageDiagram hF X y) (op 0)))) :
          (a : (F.obj (op 0)).obj.obj (op X)) → (F.obj (op 0)).obj.obj (op (limit (preimageDiagram hF X y))))
        y :
      (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op (limit (preimageDiagram hF X y))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
inst_4 : HasSheafify (coherentTopology C) (Type v)
inst_5 : Balanced (Sheaf (coherentTopology C) (Type v))
inst_6 : GrothendieckTopology.WEqualsLocallyBijective (coherentTopology C) (Type v) (FA := TypeCat.Fun)
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
simp_rw :
  ∀ (hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)),
    Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F₁ :=
      Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)) (c.π.app (op 0))
⊢ Epi (X := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)) (c.π.app (op 0))

Tactic:
simp_rw [← Sheaf.isLocallySurjective_iff_epi'] at hF ⊢

Premises used: CategoryTheory.Sheaf.isLocallySurjective_iff_epi'
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
inst_4 : HasSheafify (coherentTopology C) (Type v)
inst_5 : Balanced (Sheaf (coherentTopology C) (Type v))
inst_6 : GrothendieckTopology.WEqualsLocallyBijective (coherentTopology C) (Type v) (FA := TypeCat.Fun)
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
⊢ Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F₁ :=
    Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)) (c.π.app (op 0))

Tactic:
isLocallySurjective_π_app_zero_of_isLocallySurjective_map hc hF h

Premises used: CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
inst_4 : HasSheafify (coherentTopology C) (Type v)
inst_5 : Balanced (Sheaf (coherentTopology C) (Type v))
inst_6 : GrothendieckTopology.WEqualsLocallyBijective (coherentTopology C) (Type v) (FA := TypeCat.Fun)
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
⊢ Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F₁ :=
    Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)) (c.π.app (op 0))

Tactic:
exact isLocallySurjective_π_app_zero_of_isLocallySurjective_map hc hF h

Premises used: CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
⊢ F.IsCoverDense (coherentTopology D)

Tactic:
F.isCoverDense_of_generate_singleton_functor_π_mem _ fun B ↦ ⟨_, F.effectiveEpiOver B, ?_⟩

Premises used: CategoryTheory.Functor.EffectivelyEnough.presentation, Nonempty.some, CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_mem, Exists.intro, CategoryTheory.Functor.effectiveEpiOver, CategoryTheory.Functor.EffectivePresentation.p
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
refine :
  ∀ (B : D),
    Sieve.generate
        (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
          (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B)) ∈
      (coherentTopology D : (a : D) → Set (Sieve a)) B
⊢ F.IsCoverDense (coherentTopology D)

Tactic:
refine F.isCoverDense_of_generate_singleton_functor_π_mem _ fun B ↦ ⟨_, F.effectiveEpiOver B, ?_⟩

Premises used: CategoryTheory.Functor.EffectivelyEnough.presentation, Nonempty.some, CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_mem, Exists.intro, CategoryTheory.Functor.effectiveEpiOver, CategoryTheory.Functor.EffectivePresentation.p
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B : D
hS :
  Membership.mem (γ := Set (Presieve.{v_2, u_2} B))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage D)) B)
    (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B))
⊢ Sieve.generate
      (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
        (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B)) ∈
    (coherentTopology D : (a : D) → Set (Sieve a)) B

Tactic:
apply Coverage.Saturate.of

Premises used: CategoryTheory.Coverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B : D
⊢ Membership.mem (γ := Set (Presieve.{v_2, u_2} B))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage D)) B)
    (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B))

Tactic:
⟨Unit, inferInstance, fun _ => F.effectiveEpiOverObj B,
    fun _ => F.effectiveEpiOver B, ?_, ?_⟩

Premises used: Set.Mem, setOf, inferInstance, CategoryTheory.Functor.effectiveEpiOverObj, Unit, And.intro, Exists.intro, CategoryTheory.Functor.effectiveEpiOver