awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
F : Sheaf C X
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)
f : F ⟶ 0 := IsZero.from_ ⋯ F
this : IsIso f
⊢ IsZero F

Tactic:
(isZero_zero _).of_iso (asIso f)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.asIso
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
F : Sheaf C X
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)
f : F ⟶ 0 := IsZero.from_ ⋯ F
this : IsIso f
⊢ IsZero F

Tactic:
exact (isZero_zero _).of_iso (asIso f)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.asIso
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
mp : S.Exact → ∀ (x : (↑X : Type u)), ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))
mpr : (∀ (x : (↑X : Type u)), ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))) → S.Exact
⊢ S.Exact ↔ ∀ (x : (↑X : Type u)), ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))

Tactic:
constructor
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
h : S.Exact
x : (↑X : Type u)
⊢ Functor.PreservesHomology (C := Sheaf C X) (forget C X ⋙ stalkFunctor C x) ↔
    ∀ (S : ShortComplex (Sheaf C X)), S.Exact → ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))

Tactic:
have := (forget C X ⋙ stalkFunctor C x).exact_tfae.out 2 1
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
h : S.Exact
x : (↑X : Type u)
this :
  Functor.PreservesHomology (C := Sheaf C X) (forget C X ⋙ stalkFunctor C x) ↔
    ∀ (S : ShortComplex (Sheaf C X)), S.Exact → ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))
⊢ ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))

Tactic:
this.mp inferInstance S h

Premises used: inferInstance, Iff.mp
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
h : S.Exact
x : (↑X : Type u)
this :
  Functor.PreservesHomology (C := Sheaf C X) (forget C X ⋙ stalkFunctor C x) ↔
    ∀ (S : ShortComplex (Sheaf C X)), S.Exact → ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))
⊢ ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))

Tactic:
exact this.mp inferInstance S h

Premises used: inferInstance, Iff.mp
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
h : ∀ (x : (↑X : Type u)), ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C x))
⊢ ∀ (x : (↑X : Type u)), IsZero.{u, v} (ShortComplex.homology (S.map (forget C X ⋙ stalkFunctor C x)))

Tactic:
simp_rw [ShortComplex.exact_iff_isZero_homology] at h

Premises used: CategoryTheory.ShortComplex.exact_iff_isZero_homology
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (ShortComplex.homology (S.map (forget C X ⋙ stalkFunctor C x)))
mpr : ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) S.homology)
⊢ S.Exact

Tactic:
rw [ShortComplex.exact_iff_isZero_homology, isZero_iff_stalkFunctor_obj_isZero S.homology]

Premises used: CategoryTheory.ShortComplex.exact_iff_isZero_homology, TopCat.Sheaf.isZero_iff_stalkFunctor_obj_isZero, CategoryTheory.ShortComplex.homology
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (ShortComplex.homology (S.map (forget C X ⋙ stalkFunctor C x)))
⊢ ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) S.homology)

Tactic:
fun x => (h x).of_iso
    (ShortComplex.mapHomologyIso S (forget C X ⋙ stalkFunctor C x)).symm

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ShortComplex.mapHomologyIso, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.symm, TopCat.Presheaf.stalkFunctor, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
S : ShortComplex (Sheaf C X)
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (ShortComplex.homology (S.map (forget C X ⋙ stalkFunctor C x)))
⊢ ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) S.homology)

Tactic:
exact fun x => (h x).of_iso
    (ShortComplex.mapHomologyIso S (forget C X ⋙ stalkFunctor C x)).symm

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ShortComplex.mapHomologyIso, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.symm, TopCat.Presheaf.stalkFunctor, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.AddCommGrpCat
Goal:
X : TopCat
U : Opens (↑X : Type u)
S : ShortComplex ((Opens (↑X : Type u))ᵒᵖ ⥤ AddCommGrpCat)
hS : S.Exact
s : (↑(S.X₂.obj (op U)) : Type u)
h :
  Eq (α := (↑(S.X₃.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 (op U)) (S.g.app (op U)) :
          (a : (↑(S.X₂.obj (op U)) : Type u)) → (↑(S.X₃.obj (op U)) : Type u))
        s :
      (↑(S.X₃.obj (op U)) : Type u))
    (0 : (↑(S.X₃.obj (op U)) : Type u))
F : ((Opens (↑X : Type u))ᵒᵖ ⥤ AddCommGrpCat) ⥤ AddCommGrpCat :=
  Functor.obj (evaluation (Opens (↑X : Type u))ᵒᵖ AddCommGrpCat) (op U)
⊢ ∃ (t : (↑(S.X₁.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 (op U)) (S.f.app (op U)) :
          (a : (↑(S.X₁.obj (op U)) : Type u)) → (↑(S.X₂.obj (op U)) : Type u))
        t =
      s

Tactic:
(ShortComplex.ab_exact_iff (S.map F)).mp (((Functor.exact_tfae F).out 1 3 rfl rfl).mpr
    ⟨inferInstance, inferInstance⟩ S hS) _ h

Premises used: Iff.mpr, inferInstance, CategoryTheory.ShortComplex.ab_exact_iff, List.TFAE.out, And.intro, Iff.mp, CategoryTheory.ShortComplex.map, OfNat.ofNat, CategoryTheory.Functor.exact_tfae, rfl
-- Module: Mathlib.Topology.Sheaves.AddCommGrpCat
Goal:
X : TopCat
U : Opens (↑X : Type u)
S : ShortComplex ((Opens (↑X : Type u))ᵒᵖ ⥤ AddCommGrpCat)
hS : S.Exact
s : (↑(S.X₂.obj (op U)) : Type u)
h :
  Eq (α := (↑(S.X₃.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 (op U)) (S.g.app (op U)) :
          (a : (↑(S.X₂.obj (op U)) : Type u)) → (↑(S.X₃.obj (op U)) : Type u))
        s :
      (↑(S.X₃.obj (op U)) : Type u))
    (0 : (↑(S.X₃.obj (op U)) : Type u))
F : ((Opens (↑X : Type u))ᵒᵖ ⥤ AddCommGrpCat) ⥤ AddCommGrpCat :=
  Functor.obj (evaluation (Opens (↑X : Type u))ᵒᵖ AddCommGrpCat) (op U)
⊢ ∃ (t : (↑(S.X₁.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 (op U)) (S.f.app (op U)) :
          (a : (↑(S.X₁.obj (op U)) : Type u)) → (↑(S.X₂.obj (op U)) : Type u))
        t =
      s

Tactic:
exact (ShortComplex.ab_exact_iff (S.map F)).mp (((Functor.exact_tfae F).out 1 3 rfl rfl).mpr
    ⟨inferInstance, inferInstance⟩ S hS) _ h

Premises used: Iff.mpr, inferInstance, CategoryTheory.ShortComplex.ab_exact_iff, List.TFAE.out, And.intro, Iff.mp, CategoryTheory.ShortComplex.map, OfNat.ofNat, CategoryTheory.Functor.exact_tfae, rfl
-- Module: Mathlib.Topology.Sheaves.AddCommGrpCat
Goal:
X : TopCat
U : Opens (↑X : Type u)
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.Exact
hf : Mono S.f
s : (↑(S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
h :
  Eq (α :=
    (↑(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))
        s :
      (↑(S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
        Type u))
    (0 :
      (↑(S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
        Type u))
⊢ ∃ (t :
    (↑(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.f.hom.app (op U)) :
          (a : (↑(S.X₁.obj.obj (op U)) : Type u)) → (↑(S.X₂.obj.obj (op U)) : Type u))
        t =
      s

Tactic:
Presheaf.sections_exact_of_exact
    (((Functor.preservesFiniteLimits_tfae (Sheaf.forget ..)).out 1 3 rfl rfl).mpr
    inferInstance S ⟨hS, hf⟩).left h

Premises used: Iff.mpr, inferInstance, CategoryTheory.Functor.preservesFiniteLimits_tfae, List.TFAE.out, And.left, And.intro, OfNat.ofNat, TopCat.Sheaf.forget, rfl, TopCat.Presheaf.sections_exact_of_exact
-- Module: Mathlib.Topology.Sheaves.AddCommGrpCat
Goal:
X : TopCat
U V : Opens (↑X : Type u)
F : Presheaf AddCommGrpCat X
h : V ≤ U
s t : (↑(F.obj (op U)) : Type u_1)
delta :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
          AddCommGrpCat.carrier) (F.map (homOfLE h).op) :
        (a : (↑(F.obj (op U)) : Type u_1)) → (↑(F.obj (op V)) : Type u_1))
      (s + t) =
    HAdd.hAdd (α :=
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
        AddCommGrpCat.carrier) (F.obj (op V)))
      (β :=
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
        AddCommGrpCat.carrier) (F.obj (op V)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
              AddCommGrpCat.carrier) (F.map (homOfLE h).op) :
            (a : (↑(F.obj (op U)) : Type u_1)) → (↑(F.obj (op V)) : Type u_1))
          s :
        (↑(F.obj (op V)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
              AddCommGrpCat.carrier) (F.map (homOfLE h).op) :
            (a : (↑(F.obj (op U)) : Type u_1)) → (↑(F.obj (op V)) : Type u_1))
          t :
        (↑(F.obj (op V)) : Type u_1))
⊢ restrictOpen (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
      AddCommGrpCat.carrier) (s + t) V h =
    HAdd.hAdd (α :=
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
        AddCommGrpCat.carrier) (F.obj (op V)))
      (restrictOpen (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
        AddCommGrpCat.carrier) s V h)
      (restrictOpen (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
        AddCommGrpCat.carrier) t V h)

Tactic:
delta Presheaf.restrictOpen Presheaf.restrict

Premises used: TopCat.Presheaf.restrict, TopCat.Presheaf.restrictOpen
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F : X ⥤ C
x : X
rw : IsUpperSet.{v} (α := X) {y : X | x ≤ y}
⊢ IsOpen[inst] {y : X | x ≤ y}

Tactic:
rw [IsUpperSet.isOpen_iff_isUpperSet]

Premises used: Topology.IsUpperSet.isOpen_iff_isUpperSet
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F : X ⥤ C
x y z : X
h1 : y ≤ z
h2 : Membership.mem (γ := Set X) {y : X | x ≤ y} y
⊢ Membership.mem (γ := Set X) {y : X | x ≤ y} z

Tactic:
le_trans h2 h1

Premises used: Set.Mem, setOf, le_trans
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F : X ⥤ C
x y z : X
h1 : y ≤ z
h2 : Membership.mem (γ := Set X) {y : X | x ≤ y} y
⊢ Membership.mem (γ := Set X) {y : X | x ≤ y} z

Tactic:
exact le_trans h2 h1

Premises used: le_trans
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
x : X
⊢ Membership.mem (γ := Opens X) (principalOpen x) x

Tactic:
le_refl _

Premises used: le_refl, Set.Mem, setOf
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
x : X
U : Opens X
⊢ principalOpen x ≤ U ↔ x ∈ U

Tactic:
⟨fun h => h <| self_mem_principalOpen _, fun hx y hy => ?_⟩

Premises used: Alexandrov.self_mem_principalOpen, Iff.intro
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
x : X
U : Opens X
refine : ∀ (hx : x ∈ U) (y : X) (hy : Membership.mem (γ := Opens X) (principalOpen x) y), y ∈ U
⊢ principalOpen x ≤ U ↔ x ∈ U

Tactic:
refine ⟨fun h => h <| self_mem_principalOpen _, fun hx y hy => ?_⟩
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : Membership.mem (γ := Opens X) (principalOpen x) y
⊢ IsOpen[inst] (↑U : Set X)

Tactic:
have := U.isOpen
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : Membership.mem (γ := Opens X) (principalOpen x) y
this : IsOpen[inst] (↑U : Set X)
⊢ IsUpperSet (↑U : Set X)

Tactic:
rw [IsUpperSet.isOpen_iff_isUpperSet] at this

Premises used: Topology.IsUpperSet.isOpen_iff_isUpperSet
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : Membership.mem (γ := Opens X) (principalOpen x) y
this : IsUpperSet (↑U : Set X)
⊢ y ∈ U

Tactic:
this hy hx
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : Membership.mem (γ := Opens X) (principalOpen x) y
this : IsUpperSet (↑U : Set X)
⊢ y ∈ U

Tactic:
exact this hy hx
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
x y : X
h : x ≤ y
⊢ LE.le (α := Opens X) (principalOpen y) (principalOpen x)

Tactic:
fun _ hc => le_trans h hc

Premises used: Set.Mem, setOf, le_trans
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
ι : Type v
x : X
Us : ι → Opens X
h : principalOpen x ≤ iSup Us
⊢ ∃ (i : ι), principalOpen x ≤ Us i

Tactic:
grind [principalOpen_le_iff, Opens.mem_iSup]

Premises used: Alexandrov.principalOpen_le_iff, TopologicalSpace.Opens.mem_iSup
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F : X ⥤ C
α : Type v
Us : α → Opens X
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑(of X) : Type v)) fun (V : Opens (↑(of X) : Type v)) ↦
        ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑(of X) : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
x y : StructuredArrow (Opposite.op (iSup Us)) (principals X)
e : x ⟶ y
xx : StructuredArrow (D := (Opens X)ᵒᵖ) (Opposite.op (principalOpen x.right)) (principals X) :=
  { left := { as := PUnit.unit }, right := x.right,
    hom := 𝟙 (obj (fromPUnit (Opposite.op (principalOpen x.right))) { as := PUnit.unit : Discrete PUnit.{1} }) }
yy : StructuredArrow (D := (Opens X)ᵒᵖ) (Opposite.op (principalOpen x.right)) (principals X) :=
  { left := { as := PUnit.unit }, right := y.right, hom := Quiver.Hom.op (LE.le.hom ⋯) }
ee : xx ⟶ yy := { left := 𝟙 xx.left, right := StructuredArrow.Hom.right e, w := ⋯ }
⊢ Eq (α :=
    obj
        (Functor.op (ObjectProperty.ι fun (V : Opens (↑(of X) : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙
          principalsKanExtension F)
        (obj (projSup Us) x) ⟶
      F.obj (obj (generator (iSup Us)) y))
    (CategoryTheory.Functor.map
        (Functor.op (ObjectProperty.ι fun (V : Opens (↑(of X) : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙
          principalsKanExtension F)
        (CategoryTheory.Functor.map (projSup Us) e) ≫
      limit.π (generator (principalOpen y.right) ⋙ F)
        { left := { as := PUnit.unit }, right := y.right, hom := 𝟙 (Opposite.op (principalOpen y.right)) })
    (CategoryStruct.comp (Y := F.obj (obj (generator (iSup Us)) x))
      (limit.π (generator (principalOpen x.right) ⋙ F)
          { left := { as := PUnit.unit }, right := x.right, hom := 𝟙 (Opposite.op (principalOpen x.right)) } :
        limit (J := StructuredArrow (D := (Opens X)ᵒᵖ) (Opposite.op (principalOpen x.right)) (principals X))
            (generator (principalOpen x.right) ⋙ F) ⟶
          obj (C := StructuredArrow (D := (Opens X)ᵒᵖ) (Opposite.op (principalOpen x.right)) (principals X))
            (generator (principalOpen x.right) ⋙ F)
            { left := { as := PUnit.unit }, right := x.right, hom := 𝟙 (Opposite.op (principalOpen x.right)) })
      (F.map (CategoryTheory.Functor.map (generator (iSup Us)) e)))

Tactic:
(limit.lift_π _ _).trans (limit.w
        (StructuredArrow.proj _ (principals X) ⋙ F) ee).symm

Premises used: Set.Mem, setOf, CategoryTheory.Functor.comp, CategoryTheory.Limits.limit, Alexandrov.principals, CategoryTheory.Limits.limit.lift, Alexandrov.principalOpen, Eq.symm, CategoryTheory.StructuredArrow.proj, CategoryTheory.Limits.limit.lift_π, Eq.trans, CategoryTheory.Limits.limit.w