awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
this : Mono f
U : Opens (↑X : Type w)
V : Opens (↑Y : Type w)
i : V ⟶ hf.functor.obj U
x : (↑Y : Type w)
h : Membership.mem (γ := Set (↑Y : Type w)) V.1 x
hF :
  ∀ w ∈ (↑U : Set (↑X : Type w)),
    ∀
      (h :
        Membership.mem (α := (↑Y : Type w)) (γ := Set (↑Y : Type w)) V.1
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                  f :
                (a : (↑X : Type w)) → (↑Y : Type w))
              w :
            (↑Y : Type w))),
      Membership.mem (α := (↑Y : Type w)) (γ := Set (↑Y : Type w))
        (Set.range (ι := (↑X : Type w))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC :=
                TopCat.carrier) f) :
            (a : (↑X : Type w)) → (↑Y : Type w)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                f :
              (a : (↑X : Type w)) → (↑Y : Type w))
            w :
          (↑Y : Type w))
⊢ Membership.mem (γ := Set (↑Y : Type w))
    (Set.range (ι := (↑X : Type w))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type w)) → (↑Y : Type w)))
    x

Tactic:
obtain ⟨_, _, rfl⟩ := i.le h

Premises used: Quiver.Hom.le, rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
this : Mono f
U : Opens (↑X : Type w)
V : Opens (↑Y : Type w)
i : V ⟶ hf.functor.obj U
w : (↑X : Type w)
left : w ∈ (↑U : Set (↑X : Type w))
h :
  Membership.mem (α := (↑Y : Type w)) (γ := Set (↑Y : Type w)) V.1
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f :
          (a : (↑X : Type w)) → (↑Y : Type w))
        w :
      (↑Y : Type w))
⊢ Membership.mem (α := (↑Y : Type w)) (γ := Set (↑Y : Type w))
    (Set.range (ι := (↑X : Type w))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type w)) → (↑Y : Type w)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f :
          (a : (↑X : Type w)) → (↑Y : Type w))
        w :
      (↑Y : Type w))

Tactic:
⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
this : Mono f
U : Opens (↑X : Type w)
V : Opens (↑Y : Type w)
i : V ⟶ hf.functor.obj U
w : (↑X : Type w)
left : w ∈ (↑U : Set (↑X : Type w))
h :
  Membership.mem (α := (↑Y : Type w)) (γ := Set (↑Y : Type w)) V.1
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f :
          (a : (↑X : Type w)) → (↑Y : Type w))
        w :
      (↑Y : Type w))
⊢ Membership.mem (α := (↑Y : Type w)) (γ := Set (↑Y : Type w))
    (Set.range (ι := (↑X : Type w))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type w)) → (↑Y : Type w)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f :
          (a : (↑X : Type w)) → (↑Y : Type w))
        w :
      (↑Y : Type w))

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
cover_preserve :
  ∀ {U : Opens (↑X : Type w)} {S : Sieve U},
    S ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U →
      Membership.mem (γ := Set (Sieve (hf.functor.obj U)))
        ((Opens.grothendieckTopology (↑Y : Type w) : (a : Opens (↑Y : Type w)) → Set (Sieve a)) (hf.functor.obj U))
        (Sieve.functorPushforward hf.functor S)
⊢ CoverPreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w)) hf.functor

Tactic:
constructor
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
U : Opens (↑X : Type w)
S : Sieve U
hU : S ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hx : x ∈ (↑U : Set (↑X : Type w))
cover_preserve :
  ∀ (V : Opens (↑X : Type w)) (i : V ⟶ U) (hV : S.arrows i) (hxV : x ∈ V),
    ∃ (U_1 : Opens (↑Y : Type w)) (f_1 : U_1 ⟶ hf.functor.obj U),
      (Sieve.functorPushforward hf.functor S).arrows f_1 ∧
        Membership.mem (α := (↑Y : Type w)) U_1
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                  f :
                (a : (↑X : Type w)) → (↑Y : Type w))
              x :
            (↑Y : Type w))
⊢ ∃ (U_1 : Opens (↑Y : Type w)) (f_1 : U_1 ⟶ hf.functor.obj U),
    (Sieve.functorPushforward hf.functor S).arrows f_1 ∧
      Membership.mem (α := (↑Y : Type w)) U_1
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                f :
              (a : (↑X : Type w)) → (↑Y : Type w))
            x :
          (↑Y : Type w))

Tactic:
obtain ⟨V, i, hV, hxV⟩ := hU x hx
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
U : Opens (↑X : Type w)
S : Sieve U
hU : S ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hx : x ∈ (↑U : Set (↑X : Type w))
V : Opens (↑X : Type w)
i : V ⟶ U
hV : S.arrows i
hxV : x ∈ V
⊢ ∃ (U_1 : Opens (↑Y : Type w)) (f_1 : U_1 ⟶ hf.functor.obj U),
    (Sieve.functorPushforward hf.functor S).arrows f_1 ∧
      Membership.mem (α := (↑Y : Type w)) U_1
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                f :
              (a : (↑X : Type w)) → (↑Y : Type w))
            x :
          (↑Y : Type w))

Tactic:
⟨_, hf.functor.map i, ⟨_, i, 𝟙 _, hV, rfl⟩, Set.mem_image_of_mem f hxV⟩

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, Set.mem_image_of_mem, IsOpenMap.functor, And.intro, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
U : Opens (↑X : Type w)
S : Sieve U
hU : S ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hx : x ∈ (↑U : Set (↑X : Type w))
V : Opens (↑X : Type w)
i : V ⟶ U
hV : S.arrows i
hxV : x ∈ V
⊢ ∃ (U_1 : Opens (↑Y : Type w)) (f_1 : U_1 ⟶ hf.functor.obj U),
    (Sieve.functorPushforward hf.functor S).arrows f_1 ∧
      Membership.mem (α := (↑Y : Type w)) U_1
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                f :
              (a : (↑X : Type w)) → (↑Y : Type w))
            x :
          (↑Y : Type w))

Tactic:
exact ⟨_, hf.functor.map i, ⟨_, i, 𝟙 _, hV, rfl⟩, Set.mem_image_of_mem f hxV⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
h :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
hF₁ : CompatiblePreserving (Opens.grothendieckTopology (↑Y : Type w)) h.functor
hF₂ : CoverPreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w)) h.functor
⊢ h.functor.IsContinuous (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w))

Tactic:
apply Functor.isContinuous_of_coverPreserving

Premises used: CategoryTheory.Functor.isContinuous_of_coverPreserving
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
h :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
⊢ CompatiblePreserving (Opens.grothendieckTopology (↑Y : Type w)) h.functor

Tactic:
h.compatiblePreserving

Premises used: Topology.IsOpenEmbedding.compatiblePreserving
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
h :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
⊢ CompatiblePreserving (Opens.grothendieckTopology (↑Y : Type w)) h.functor

Tactic:
exact h.compatiblePreserving

Premises used: Topology.IsOpenEmbedding.compatiblePreserving
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
h :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
⊢ CoverPreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w)) h.functor

Tactic:
h.isOpenMap.coverPreserving

Premises used: Topology.IsOpenEmbedding.isOpenMap, IsOpenMap.coverPreserving
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
h :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
⊢ CoverPreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w)) h.functor

Tactic:
exact h.isOpenMap.coverPreserving

Premises used: Topology.IsOpenEmbedding.isOpenMap, IsOpenMap.coverPreserving
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Presheaf.{w, v, u} C Y
h :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
hF : F.IsSheaf
⊢ h.functor.IsContinuous (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w))

Tactic:
have := h.functor_isContinuous
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Presheaf.{w, v, u} C Y
h :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
hF : F.IsSheaf
this : h.functor.IsContinuous (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w))
⊢ IsSheaf (h.functor.op ⋙ F)

Tactic:
Functor.op_comp_isSheaf _ _ _ ⟨_, hF⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, TopCat.Presheaf.IsSheaf, CategoryTheory.Functor.op_comp_isSheaf
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Presheaf.{w, v, u} C Y
h :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
hF : F.IsSheaf
this : h.functor.IsContinuous (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w))
⊢ IsSheaf (h.functor.op ⋙ F)

Tactic:
exact Functor.op_comp_isSheaf _ _ _ ⟨_, hF⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Functor.op_comp_isSheaf
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
cofiltered : ∀ (X_1 : Opens (↑X : Type w)), IsCofiltered.{w, w} (StructuredArrow X_1 (Opens.map f))
⊢ RepresentablyFlat (Opens.map f)

Tactic:
constructor
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
⊢ IsCofiltered.{w, w} (StructuredArrow U (Opens.map f))

Tactic:
@IsCofiltered.mk _ _ ?_ ?_

Premises used: CategoryTheory.IsCofiltered.mk
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
cofiltered : IsCofilteredOrEmpty.{w, w} (StructuredArrow U (Opens.map f))
cofiltered₁ : Nonempty.{w + 1} (StructuredArrow U (Opens.map f))
⊢ IsCofiltered.{w, w} (StructuredArrow U (Opens.map f))

Tactic:
refine @IsCofiltered.mk _ _ ?_ ?_

Premises used: CategoryTheory.IsCofiltered.mk
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
cofiltered :
  ∀ (X_1 Y_1 : StructuredArrow U (Opens.map f)),
    ∃ (W : StructuredArrow U (Opens.map f)) (x : W ⟶ X_1) (x : W ⟶ Y_1), True
cofiltered₁ :
  ∀ ⦃X_1 Y_1 : StructuredArrow U (Opens.map f)⦄ (f_1 g : X_1 ⟶ Y_1),
    ∃ (W : StructuredArrow U (Opens.map f)) (h : W ⟶ X_1), h ≫ f_1 = h ≫ g
⊢ IsCofilteredOrEmpty.{w, w} (StructuredArrow U (Opens.map f))

Tactic:
constructor
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
V W : StructuredArrow U (Opens.map f)
⊢ ∃ (W_1 : StructuredArrow U (Opens.map f)) (x : W_1 ⟶ V) (x : W_1 ⟶ W), True

Tactic:
⟨⟨⟨PUnit.unit⟩, V.right ⊓ W.right, homOfLE <| le_inf V.hom.le W.hom.le⟩,
        StructuredArrow.homMk (homOfLE inf_le_left),
        StructuredArrow.homMk (homOfLE inf_le_right), trivial⟩

Premises used: CategoryTheory.StructuredArrow.homMk, trivial, Quiver.Hom.le, inf_le_right, CategoryTheory.StructuredArrow.hom, le_inf, CategoryTheory.Discrete.mk, CategoryTheory.homOfLE, Exists.intro, CategoryTheory.Comma.mk, CategoryTheory.StructuredArrow.right, PUnit.unit, inf_le_left, Min.min
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
V W : StructuredArrow U (Opens.map f)
⊢ ∃ (W_1 : StructuredArrow U (Opens.map f)) (x : W_1 ⟶ V) (x : W_1 ⟶ W), True

Tactic:
exact ⟨⟨⟨PUnit.unit⟩, V.right ⊓ W.right, homOfLE <| le_inf V.hom.le W.hom.le⟩,
        StructuredArrow.homMk (homOfLE inf_le_left),
        StructuredArrow.homMk (homOfLE inf_le_right), trivial⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
x x_1 : StructuredArrow U (Opens.map f)
x_2 x_3 : x ⟶ x_1
⊢ 𝟙 x ≫ x_2 = 𝟙 x ≫ x_3

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
⊢ ∀ ⦃X_1 Y_1 : StructuredArrow U (Opens.map f)⦄ (f_1 g : X_1 ⟶ Y_1),
    ∃ (W : StructuredArrow U (Opens.map f)) (h : W ⟶ X_1), h ≫ f_1 = h ≫ g

Tactic:
exact fun _ _ _ _ ↦ ⟨_, 𝟙 _, by simp [eq_iff_true_of_subsingleton]⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
⊢ Nonempty.{w + 1} (StructuredArrow U (Opens.map f))

Tactic:
⟨StructuredArrow.mk <| show U ⟶ (Opens.map f).obj ⊤ from homOfLE le_top⟩

Premises used: Nonempty.intro, le_top, CategoryTheory.homOfLE, CategoryTheory.StructuredArrow.mk
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
⊢ Nonempty.{w + 1} (StructuredArrow U (Opens.map f))

Tactic:
exact ⟨StructuredArrow.mk <| show U ⟶ (Opens.map f).obj ⊤ from homOfLE le_top⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ CompatiblePreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)

Tactic:
compatiblePreservingOfFlat _ _

Premises used: CategoryTheory.compatiblePreservingOfFlat
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
cover_preserve :
  ∀ {U : Opens (↑Y : Type w)} {S : Sieve U},
    S ∈ (Opens.grothendieckTopology (↑Y : Type w) : (a : Opens (↑Y : Type w)) → Set (Sieve a)) U →
      Membership.mem (γ := Set (Sieve ((Opens.map f).obj U)))
        ((Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) ((Opens.map f).obj U))
        (Sieve.functorPushforward (Opens.map f) S)
⊢ CoverPreserving (Opens.grothendieckTopology (↑Y : Type w)) (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)

Tactic:
constructor
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
U : Opens (↑Y : Type w)
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology (↑Y : Type w) : (a : Opens (↑Y : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hx : x ∈ (Opens.map f).obj U
cover_preserve :
  ∀ (V : Opens (↑Y : Type w)) (i : V ⟶ U) (hi : S.arrows i)
    (hxV :
      Membership.mem (α := (↑Y : Type w)) V
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                f :
              (a : (↑X : Type w)) → (↑Y : Type w))
            x :
          (↑Y : Type w))),
    ∃ (U_1 : Opens (↑X : Type w)) (f_1 : U_1 ⟶ (Opens.map f).obj U),
      (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f_1 : U_1 ⟶ (Opens.map f).obj U),
    (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1

Tactic:
obtain ⟨V, i, hi, hxV⟩ := hS (f x) hx

Premises used: CategoryTheory.ConcreteCategory.hom, DFunLike.coe
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
U : Opens (↑Y : Type w)
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology (↑Y : Type w) : (a : Opens (↑Y : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hx : x ∈ (Opens.map f).obj U
V : Opens (↑Y : Type w)
i : V ⟶ U
hi : S.arrows i
hxV :
  Membership.mem (α := (↑Y : Type w)) V
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f :
          (a : (↑X : Type w)) → (↑Y : Type w))
        x :
      (↑Y : Type w))
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f_1 : U_1 ⟶ (Opens.map f).obj U),
    (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1

Tactic:
⟨_, (Opens.map f).map i, ⟨_, _, 𝟙 _, hi, Subsingleton.elim _ _⟩, hxV⟩

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, And.intro, Exists.intro, TopologicalSpace.Opens.map, Subsingleton.elim
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
U : Opens (↑Y : Type w)
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology (↑Y : Type w) : (a : Opens (↑Y : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hx : x ∈ (Opens.map f).obj U
V : Opens (↑Y : Type w)
i : V ⟶ U
hi : S.arrows i
hxV :
  Membership.mem (α := (↑Y : Type w)) V
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f :
          (a : (↑X : Type w)) → (↑Y : Type w))
        x :
      (↑Y : Type w))
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f_1 : U_1 ⟶ (Opens.map f).obj U),
    (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1

Tactic:
exact ⟨_, (Opens.map f).map i, ⟨_, _, 𝟙 _, hi, Subsingleton.elim _ _⟩, hxV⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
hF₁ : CompatiblePreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)
hF₂ :
  CoverPreserving (Opens.grothendieckTopology (↑Y : Type w)) (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)
⊢ (Opens.map f).IsContinuous (Opens.grothendieckTopology (↑Y : Type w)) (Opens.grothendieckTopology (↑X : Type w))

Tactic:
apply Functor.isContinuous_of_coverPreserving

Premises used: CategoryTheory.Functor.isContinuous_of_coverPreserving
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
⊢ CompatiblePreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)

Tactic:
compatiblePreserving_opens_map f

Premises used: compatiblePreserving_opens_map
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
⊢ CompatiblePreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)

Tactic:
exact compatiblePreserving_opens_map f

Premises used: compatiblePreserving_opens_map
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
⊢ CoverPreserving (Opens.grothendieckTopology (↑Y : Type w)) (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)

Tactic:
coverPreserving_opens_map f

Premises used: coverPreserving_opens_map
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
⊢ CoverPreserving (Opens.grothendieckTopology (↑Y : Type w)) (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)

Tactic:
exact coverPreserving_opens_map f

Premises used: coverPreserving_opens_map
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens (↑X : Type w)
F_1 : Presheaf.{w, v, u} C X
F' F : Sheaf.{w, v, u} C X
U : Opens (↑X : Type w)
h : U = ⊥
⊢ Limits.IsTerminal.{v, u}
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))

Tactic:
convert! F.isTerminalOfEmpty

Premises used: TopCat.Sheaf.isTerminalOfEmpty