awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (limit.lift_π _ _).trans (limit.w
        (StructuredArrow.proj _ (principals X) ⋙ F) ee).symm

Premises used: CategoryTheory.Functor.comp, Alexandrov.principals, Eq.symm, CategoryTheory.StructuredArrow.proj, CategoryTheory.Limits.limit.lift_π, Eq.trans, CategoryTheory.Limits.limit.w
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
V : Opens (↑X : Type v)
i : α
hV : V ≤ Us i
left : Discrete PUnit.{1}
x : (↑X : Type v)
f : obj (fromPUnit (Opposite.op V)) left ⟶ obj (principals (↑X : Type v)) x
⊢ principalOpen x ≤ V

Tactic:
have e : principalOpen x ≤ V := f.unop.le
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
V : Opens (↑X : Type v)
i : α
hV : V ≤ Us i
left : Discrete PUnit.{1}
x : (↑X : Type v)
f : obj (fromPUnit (Opposite.op V)) left ⟶ obj (principals (↑X : Type v)) x
e : principalOpen x ≤ V
VV : OpensLeCover Us := ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) V ⋯
xx : OpensLeCover Us :=
  ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) (principalOpen x) ⋯
ee : xx ⟶ VV := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) e.hom
⊢ Eq (α :=
    obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
        (Opposite.op VV) ⟶
      F.obj x)
    (CategoryTheory.Functor.map
        (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
        ee.op ≫
      limit.π (generator (principalOpen x) ⋙ F)
        { left := { as := PUnit.unit }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) })
    (limit.π (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F)
      { left := left, right := x, hom := f })

Tactic:
exact (limit.lift_π _ _).trans (by aesop)

Premises used: CategoryTheory.Limits.limit.lift_π, Eq.trans
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
m :
  S.pt ⟶
    Cone.pt (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
hm :
  ∀
    (j :
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
          ∃ (i : α), V ≤ Us i)ᵒᵖ),
    m ≫ NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)) j = S.π.app j
dsimp : m = limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S)
⊢ m = limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S)

Tactic:
dsimp
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
m :
  S.pt ⟶
    Cone.pt (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
hm :
  ∀
    (j :
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
          ∃ (i : α), V ≤ Us i)ᵒᵖ),
    m ≫ NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)) j = S.π.app j
symm : limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S) = m
⊢ m = limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S)

Tactic:
symm
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
m :
  S.pt ⟶
    Cone.pt (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
hm :
  ∀
    (j :
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
          ∃ (i : α), V ≤ Us i)ᵒᵖ),
    m ≫ NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)) j = S.π.app j
w :
  ∀ (left : Discrete PUnit.{1}) (x : (↑X : Type v))
    (f : obj (fromPUnit (Opposite.op (iSup Us))) left ⟶ obj (principals (↑X : Type v)) x),
    CategoryStruct.comp (Y :=
        limit (J := StructuredArrow (Opposite.op (iSup Us)) (principals (↑X : Type v))) (generator (iSup Us) ⋙ F))
        (limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S))
        (limit.π (generator (iSup Us) ⋙ F)
          { left := left, right := x, hom := f :
            Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) }) =
      m ≫ limit.π (generator (iSup Us) ⋙ F) { left := left, right := x, hom := f }
⊢ limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S) = m

Tactic:
ext ⟨_, x, f⟩
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
m :
  S.pt ⟶
    Cone.pt (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
hm :
  ∀
    (j :
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
          ∃ (i : α), V ≤ Us i)ᵒᵖ),
    m ≫ NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)) j = S.π.app j
left : Discrete PUnit.{1}
x : (↑X : Type v)
f : obj (fromPUnit (Opposite.op (iSup Us))) left ⟶ obj (principals (↑X : Type v)) x
w : principalOpen x ≤ iSup Us
⊢ ∃ (i : α), principalOpen x ≤ Us i

Tactic:
apply exists_le_of_le_sup

Premises used: Alexandrov.exists_le_of_le_sup
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
m :
  S.pt ⟶
    Cone.pt (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
hm :
  ∀
    (j :
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
          ∃ (i : α), V ≤ Us i)ᵒᵖ),
    m ≫ NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)) j = S.π.app j
left : Discrete PUnit.{1}
x : (↑X : Type v)
f : obj (fromPUnit (Opposite.op (iSup Us))) left ⟶ obj (principals (↑X : Type v)) x
⊢ principalOpen x ≤ iSup Us

Tactic:
f.unop.le

Premises used: Set.Mem, Quiver.Hom.le, Quiver.Hom.unop
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
m :
  S.pt ⟶
    Cone.pt (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
hm :
  ∀
    (j :
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
          ∃ (i : α), V ≤ Us i)ᵒᵖ),
    m ≫ NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)) j = S.π.app j
left : Discrete PUnit.{1}
x : (↑X : Type v)
f : obj (fromPUnit (Opposite.op (iSup Us))) left ⟶ obj (principals (↑X : Type v)) x
⊢ principalOpen x ≤ iSup Us

Tactic:
exact f.unop.le

Premises used: Quiver.Hom.le, Quiver.Hom.unop
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
X : TopCat
inst_2 : Preorder (↑X : Type v)
inst_3 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
rw : IsSheafOpensLeCover (principalsKanExtension F)
⊢ TopCat.Presheaf.IsSheaf (principalsKanExtension F)

Tactic:
rw [isSheaf_iff_isSheafOpensLeCover]

Premises used: TopCat.Presheaf.isSheaf_iff_isSheafOpensLeCover
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
X : TopCat
inst_2 : Preorder (↑X : Type v)
inst_3 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
ι : Type v
Us : ι → Opens (↑X : Type v)
val :
  IsLimit (F :=
    Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : ι), V ≤ Us i) ⋙ principalsKanExtension F)
    (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
⊢ Nonempty
    (IsLimit (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : ι), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op))

Tactic:
constructor
-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
X : TopCat
inst_2 : Preorder (↑X : Type v)
inst_3 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
ι : Type v
Us : ι → Opens (↑X : Type v)
⊢ IsLimit (F :=
    Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : ι), V ≤ Us i) ⋙ principalsKanExtension F)
    (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)

Tactic:
apply isLimit

Premises used: Alexandrov.isLimit
-- 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
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
⊢ P.IsRightKanExtension η

Tactic:
assumption
-- 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
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
⊢ IsRightKanExtension (principalsKanExtension F) γ

Tactic:
assumption
-- 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
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
have : ∀ (this : P ≅ principalsKanExtension F), CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology X) P
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology X) P

Tactic:
have : P ≅ principalsKanExtension F :=
    @rightKanExtensionUnique _ _ _ _ _ _ _ _ _ _ (by assumption) _ _ (by assumption)
-- 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
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
this : P ≅ principalsKanExtension F
change : TopCat.Presheaf.IsSheaf.{v, v, u} (C := C) (X := of X) P
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology X) P

Tactic:
change TopCat.Presheaf.IsSheaf (X := TopCat.of X) P

Premises used: TopCat.Presheaf.IsSheaf
-- 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
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
this : P ≅ principalsKanExtension F
rw : TopCat.Presheaf.IsSheaf.{v, v, u} (C := C) (X := of X) (principalsKanExtension F)
⊢ TopCat.Presheaf.IsSheaf.{v, v, u} (C := C) (X := of X) P

Tactic:
rw [isSheaf_iso_iff this]

Premises used: TopCat.Presheaf.isSheaf_iso_iff
-- 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
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
this : P ≅ principalsKanExtension F
x : Preorder (↑(of X) : Type v) := inst_1
⊢ Topology.IsUpperSet.{v} (↑(of X) : Type v)

Tactic:
have _ : Topology.IsUpperSet (TopCat.of X) := inferInstanceAs <| Topology.IsUpperSet X
-- 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
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
this : P ≅ principalsKanExtension F
x : Preorder (↑(of X) : Type v) := inst_1
h_1 : Topology.IsUpperSet.{v} (↑(of X) : Type v)
⊢ TopCat.Presheaf.IsSheaf.{v, v, u} (C := C) (X := of X) (principalsKanExtension F)

Tactic:
isSheaf_principalsKanExtension (X := TopCat.of X) F

Premises used: Set.Mem, Alexandrov.isSheaf_principalsKanExtension
-- 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
P : CategoryTheory.Functor.{v, v, v, u} (Opens X)ᵒᵖ C
η : principals X ⋙ P ⟶ F
inst_5 : P.IsRightKanExtension η
γ : comp (D := (Opens X)ᵒᵖ) (principals X) (principalsKanExtension F) ⟶ F :=
  pointwiseRightKanExtensionCounit (principals X) F
h : IsRightKanExtension (principalsKanExtension F) γ := ⋯
this : P ≅ principalsKanExtension F
x : Preorder (↑(of X) : Type v) := inst_1
h_1 : Topology.IsUpperSet.{v} (↑(of X) : Type v)
⊢ TopCat.Presheaf.IsSheaf.{v, v, u} (C := C) (X := of X) (principalsKanExtension F)

Tactic:
exact isSheaf_principalsKanExtension (X := TopCat.of X) F

Premises used: Alexandrov.isSheaf_principalsKanExtension
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
F : Presheaf CommRingCat X
h :
  IsSheaf
    (F ⋙
      forget CommRingCat (FC := fun (R S : CommRingCat.{u₁}) ↦ (↑R : Type u₁) →+* (↑S : Type u₁)) (CC :=
        CommRingCat.carrier))
⊢ F.IsSheaf

Tactic:
(isSheaf_iff_isSheaf_comp (forget CommRingCat) F).mpr h

Premises used: Iff.mpr, CommRingCat, TopCat.Presheaf.isSheaf_iff_isSheaf_comp, CategoryTheory.forget
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
F : Presheaf CommRingCat X
V : Opens (↑X : Type w)
f : (↑(F.obj (op V)) : Type u_1)
U : Opens (↑X : Type w)
e : U ≤ V
⊢ Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
      (F.obj (op U)))
    (restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) f U e)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (F.map (homOfLE e).op) :
        (a : (↑(F.obj (op V)) : Type u_1)) → (↑(F.obj (op U)) : Type u_1))
      f)

Tactic:
rfl

Premises used: TopCat.Presheaf.restrict, rfl
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens (↑X : Type w))ᵒᵖ
simp_rw :
  CommRingCat.ofHom (IsLocalization.map (T := G.obj U) (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj U)) (CommRingCat.Hom.hom (F.map (𝟙 U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))

Tactic:
simp_rw [F.map_id]

Premises used: CategoryTheory.Functor.map_id