awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.EtaleSpace
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
hF_bij :
  ∀ (x : (↑X : Type v)),
    ∃ (U : Opens (↑X : Type v)),
      x ∈ U ∧
        ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
          Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
            (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU : x ∈ U
hU_bij :
  ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
⊢ ∀ (x_1 : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)),
    (↑((homeomorph (CC := CC) (FC := FC) U hU_bij x hxU :
                (a : (↑(base ⁻¹' (↑U : Set (↑X : Type v))) : Type v)) →
                  (↑(↑U : Set (↑X : Type v)) : Type v) × WithDiscreteTopology (ToType (F.stalk x)))
              x_1).1 :
        (↑X : Type v)) =
      (↑x_1 : F.EtaleSpace).base (CC := CC) (FC := FC)

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
C : Type v
inst : Category.{w, v} C
F : Presheaf.{u, w, v} C X
Y : TopCat
inst_1 : F.IsFlasque
f : X ⟶ Y
U V : (Opens (↑Y : Type u))ᵒᵖ
i : U ⟶ V
simp : Epi (F.map ((Opens.map f).map i.unop).op)
⊢ Epi ((Functor.obj (pushforward C f) F).map i)

Tactic:
simp only [pushforward_obj_obj, pushforward_obj_map]

Premises used: TopCat.Presheaf.pushforward_obj_obj, TopCat.Presheaf.pushforward_obj_map
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
C : Type v
inst : Category.{w, v} C
F : Presheaf.{u, w, v} C X
Y : TopCat
inst_1 : F.IsFlasque
f : X ⟶ Y
U V : (Opens (↑Y : Type u))ᵒᵖ
i : U ⟶ V
⊢ Epi (F.map ((Opens.map f).map i.unop).op)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
C : Type v
inst : Category.{w, v} C
Y : TopCat
F : Sheaf.{u, w, v} C X
inst_1 : F.IsFlasque
f : X ⟶ Y
⊢ (Functor.obj (pushforward C f) F).IsFlasque

Tactic:
Presheaf.IsFlasque.pushforward_isFlasque F.1 f

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ObjectProperty.FullSubcategory.obj, TopCat.Presheaf.IsFlasque.pushforward_isFlasque
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
U : Opens (↑X : Type u)
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : (↑(G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
c : Set (Under g s)
h : IsChain (fun (x y : Under g s) ↦ Nonempty.{u + 1} (y ⟶ x)) c
f : (↑c : Type u) → Opens (↑X : Type u) :=
  fun (x : (↑c : Type u)) ↦
    unop
      ((StructuredArrow.right (↑x : Under g s)).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c))
⊢ ∃! s_1 :
    ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (iSup f))),
    IsGluing (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u)))) f
      (fun (x : (↑c : Type u)) ↦
        (StructuredArrow.right (↑x : Under g s)).snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
                CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                  (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
            c))
      s_1

Tactic:
Sheaf.existsUnique_gluing F _ _ (fun i j ↦ ?_)

Premises used: TopCat.Sheaf.existsUnique_gluing
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
U : Opens (↑X : Type u)
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : (↑(G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
c : Set (Under g s)
h : IsChain (fun (x y : Under g s) ↦ Nonempty.{u + 1} (y ⟶ x)) c
f : (↑c : Type u) → Opens (↑X : Type u) :=
  fun (x : (↑c : Type u)) ↦
    unop
      ((StructuredArrow.right (↑x : Under g s)).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c))
i j : (↑c : Type u)
⊢ i = j ∨
    Nonempty.{u + 1} ((↑i : Under g s) ⟶ (↑j : Under g s)) ∨ Nonempty.{u + 1} ((↑j : Under g s) ⟶ (↑i : Under g s))

Tactic:
grind [Subtype.ext_iff, h i.property j.property]

Premises used: Subtype.ext_iff, Subtype.property
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
U : Opens (↑X : Type u)
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : (↑(G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
c : Set (Under g s)
h : IsChain (fun (x y : Under g s) ↦ Nonempty.{u + 1} (y ⟶ x)) c
f : (↑c : Type u) → Opens (↑X : Type u) :=
  fun (x : (↑c : Type u)) ↦
    unop
      ((StructuredArrow.right (↑x : Under g s)).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c))
i : (↑c : Type u)
⊢ Eq (α :=
    (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (f i ⊓ f i))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (Y :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj
              (op (f i ⊓ f i)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op ((f i).infLELeft (f i)))) :
          (a : (↑(F.obj.obj (op (f i))) : Type u)) → (↑(F.obj.obj (op (f i ⊓ f i))) : Type u))
        ((StructuredArrow.right (↑i : Under g s)).snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
                CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                  (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
            c)) :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (f i ⊓ f i))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (f i)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op ((f i).infLERight (f i)))) :
          (a : (↑(F.obj.obj (op (f i))) : Type u)) → (↑(F.obj.obj (op (f i ⊓ f i))) : Type u))
        ((StructuredArrow.right (↑i : Under g s)).snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
                CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                  (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
            c)) :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (f i ⊓ f i))) :
        Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
U : Opens (↑X : Type u)
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : (↑(G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
c : Set (Under g s)
h : IsChain (fun (x y : Under g s) ↦ Nonempty.{u + 1} (y ⟶ x)) c
f : (↑c : Type u) → Opens (↑X : Type u) :=
  fun (x : (↑c : Type u)) ↦
    unop
      ((StructuredArrow.right (↑x : Under g s)).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c))
i j : (↑c : Type u)
h₁ : Nonempty.{u + 1} ((↑i : Under g s) ⟶ (↑j : Under g s))
⊢ Eq (α :=
    (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (f i ⊓ f j))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (Y :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj
              (op (f i ⊓ f j)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op ((f i).infLELeft (f j)))) :
          (a : (↑(F.obj.obj (op (f i))) : Type u)) → (↑(F.obj.obj (op (f i ⊓ f j))) : Type u))
        ((StructuredArrow.right (↑i : Under g s)).snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
          ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj c))) :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (f i ⊓ f j))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              ((↑h₁.some.right : (↑i : Under g s).right.fst ⟶ (↑j : Under g s).right.fst) ≫
                Quiver.Hom.op ((f i).infLERight (f j)))) :
          (a : (↑(F.obj.obj (↑i : Under g s).right.fst) : Type u)) → (↑(F.obj.obj (op (f i ⊓ f j))) : Type u))
        ((↑i : Under g s).right.snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
          ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj c))) :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (f i ⊓ f j))) :
        Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
U : Opens (↑X : Type u)
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : (↑(G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
c : Set (Under g s)
h : IsChain (fun (x y : Under g s) ↦ Nonempty.{u + 1} (y ⟶ x)) c
f : (↑c : Type u) → Opens (↑X : Type u) :=
  fun (x : (↑c : Type u)) ↦
    unop
      ((StructuredArrow.right (↑x : Under g s)).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c))
i j : (↑c : Type u)
h₁ : Nonempty.{u + 1} ((↑j : Under g s) ⟶ (↑i : Under g s))
⊢ Eq (α :=
    (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (f i ⊓ f j))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (Y :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj
              (op (f i ⊓ f j)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              ((↑h₁.some.right : (↑j : Under g s).right.fst ⟶ (↑i : Under g s).right.fst) ≫
                Quiver.Hom.op ((f i).infLELeft (f j)))) :
          (a : (↑(F.obj.obj (↑j : Under g s).right.fst) : Type u)) → (↑(F.obj.obj (op (f i ⊓ f j))) : Type u))
        ((↑j : Under g s).right.snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
          ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj c))) :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (f i ⊓ f j))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (f j)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op ((f i).infLERight (f j)))) :
          (a : (↑(F.obj.obj (op (f j))) : Type u)) → (↑(F.obj.obj (op (f i ⊓ f j))) : Type u))
        ((StructuredArrow.right (↑j : Under g s)).snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
          ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj c))) :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (f i ⊓ f j))) :
        Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
U : Opens (↑X : Type u)
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : (↑(G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
c : Set (Under g s)
h : IsChain (fun (x y : Under g s) ↦ Nonempty.{u + 1} (y ⟶ x)) c
f : (↑c : Type u) → Opens (↑X : Type u) :=
  fun (x : (↑c : Type u)) ↦
    unop
      ((StructuredArrow.right (↑x : Under g s)).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c))
t :
  ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (iSup f)))
ht :
  IsGluing (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u)))) f
    (fun (x : (↑c : Type u)) ↦
      (StructuredArrow.right (↑x : Under g s)).snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c))
    t
right :
  ∀
    (y :
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (iSup f)))),
    (fun
            (s_1 :
              ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj
                  (op (iSup f)))) ↦
          IsGluing (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u)))) f
            (fun (x : (↑c : Type u)) ↦
              (StructuredArrow.right (↑x : Under g s)).snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
                      CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                        (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
                  c))
            s_1)
        y →
      y = t
⊢ iSup f ≤ U

Tactic:
have le₁ : iSup f ≤ U := iSup_le <| fun j => leOfHom j.1.hom.1.unop
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
U : Opens (↑X : Type u)
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
⊢ Epi (X := S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U))
    (S.g.hom.app (op U))

Tactic:
(AddCommGrpCat.epi_iff_surjective _).mpr (fun s ↦ ?_)

Premises used: Iff.mpr, AddCommGrpCat.epi_iff_surjective
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
U : Opens (↑X : Type u)
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
refine :
  ∀
    (s :
      (↑(S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
        Type u)),
    ∃ (a :
      (↑(S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
        Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) (X :=
              S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U))
              (S.g.hom.app (op U)) :
            (a : (↑(S.X₂.obj.obj (op U)) : Type u)) → (↑(S.X₃.obj.obj (op U)) : Type u))
          a =
        s
⊢ Epi (X := S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U))
    (S.g.hom.app (op U))

Tactic:
refine (AddCommGrpCat.epi_iff_surjective _).mpr (fun s ↦ ?_)

Premises used: Iff.mpr, AddCommGrpCat.epi_iff_surjective
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
U : Opens (↑X : Type u)
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
s : (↑(S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
obtain :
  ∀ (t : Under S.g s) (ht : ∀ (a : Under S.g s), Nonempty.{u + 1} (a ⟶ t) → Nonempty.{u + 1} (t ⟶ a)),
    ∃ (a :
      (↑(S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
        Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) (X :=
              S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U))
              (S.g.hom.app (op U)) :
            (a : (↑(S.X₂.obj.obj (op U)) : Type u)) → (↑(S.X₃.obj.obj (op U)) : Type u))
          a =
        s
⊢ ∃ (a :
    (↑(S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
      Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U))
            (S.g.hom.app (op U)) :
          (a : (↑(S.X₂.obj.obj (op U)) : Type u)) → (↑(S.X₃.obj.obj (op U)) : Type u))
        a =
      s

Tactic:
obtain ⟨t, ht⟩ := exists_maximal_of_chains_bounded
    (structured_arrows_elements_sheaf_chains_bounded S.g s)
    (fun ⟨f⟩ ⟨g⟩ ↦ ⟨g ≫ f⟩)

Premises used: exists_maximal_of_chains_bounded, Quiver.Hom, Nonempty.intro, TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_bounded, CategoryTheory.CategoryStruct.comp, Nonempty, _private.0.TopCat.Sheaf.IsFlasque.epi_of_shortExact.match_1, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
U : Opens (↑X : Type u)
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
s : (↑(S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty.{u + 1} (a ⟶ t) → Nonempty.{u + 1} (t ⟶ a)
⊢ unop
      ((StructuredArrow.right t).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c)) ≤
    U

Tactic:
have tle : t.right.1.unop ≤ U := leOfHom t.hom.1.unop
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
inst_1 : S.X₂.IsFlasque
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
rw :
  Epi (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i ≫ S.g.hom.app V)
⊢ Epi (S.g.hom.app U ≫ S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i)

Tactic:
rw [← S.g.hom.naturality i]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
inst_1 : S.X₂.IsFlasque
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
⊢ Epi (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i ≫ S.g.hom.app V)

Tactic:
CategoryTheory.epi_comp' inferInstance (epi_of_shortExact hS)

Premises used: CategoryTheory.epi_comp', inferInstance, TopCat.Sheaf.IsFlasque.epi_of_shortExact
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
inst_1 : S.X₂.IsFlasque
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
⊢ Epi (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i ≫ S.g.hom.app V)

Tactic:
exact CategoryTheory.epi_comp' inferInstance (epi_of_shortExact hS)

Premises used: CategoryTheory.epi_comp', inferInstance, TopCat.Sheaf.IsFlasque.epi_of_shortExact
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
inst_1 : S.X₂.IsFlasque
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
⊢ Epi (S.g.hom.app U ≫ S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i)

Tactic:
have : Epi (S.g.1.app U ≫ S.X₃.obj.map i) := by
      rw [← S.g.hom.naturality i]
      exact CategoryTheory.epi_comp' inferInstance (epi_of_shortExact hS)