awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
    NatTrans.app (Cone.π (Cocone.op (cocone U))) j =
      Iso.hom (Iso.refl (Cone.pt (Cocone.op (cocone U)))) ≫
        ((Cone.postcomposeEquivalence (NatIso.op (pairwiseDiagramIso U))).functor.obj
                (Cone.whisker (pairwiseToOpensLeCover U).op (opensLeCoverCocone U).op)).π.app
          j
⊢ ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
    NatTrans.app (Cone.π (Cocone.op (cocone U))) j =
      Iso.hom (Iso.refl (Cone.pt (Cocone.op (cocone U)))) ≫
        ((Cone.postcomposeEquivalence (NatIso.op (pairwiseDiagramIso U))).functor.obj
                (Cone.whisker (pairwiseToOpensLeCover U).op (opensLeCoverCocone U).op)).π.app
          j

Tactic:
cat_disch
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
⊢ F.IsSheafOpensLeCover ↔ F.IsSheafPairwiseIntersections

Tactic:
forall₂_congr fun _ U ↦ (F.isLimitOpensLeCoverEquivPairwise U).nonempty_congr

Premises used: TopCat.Presheaf.IsSheafOpensLeCover, TopCat.Presheaf.IsSheafPairwiseIntersections, TopCat.Presheaf.isLimitOpensLeCoverEquivPairwise, forall₂_congr, Equiv.nonempty_congr
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
h : F.IsSheaf
⊢ Nonempty (IsLimit (Functor.mapCone F (Cocone.op (Pairwise.cocone U))))

Tactic:
(h.isSheafOpensLeCover U).map (F.isLimitOpensLeCoverEquivPairwise _)

Premises used: TopCat.Presheaf.isLimitOpensLeCoverEquivPairwise, Nonempty.map, TopCat.Presheaf.IsSheaf.isSheafOpensLeCover, DFunLike.coe
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
rw : F.IsSheafOpensLeCover ↔ F.IsSheafPairwiseIntersections
rw₁ rw₂ : F.IsSheafPairwiseIntersections ↔ F.IsSheafPairwiseIntersections
⊢ F.IsSheaf ↔ F.IsSheafPairwiseIntersections

Tactic:
rw [isSheaf_iff_isSheafOpensLeCover, isSheafOpensLeCover_iff_isSheafPairwiseIntersections]

Premises used: TopCat.Presheaf.isSheafOpensLeCover_iff_isSheafPairwiseIntersections, TopCat.Presheaf.isSheaf_iff_isSheafOpensLeCover
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
h : F.IsSheaf
⊢ PreservesLimit (Functor.op (Pairwise.diagram U)) F

Tactic:
preservesLimit_of_preserves_limit_cone (Pairwise.coconeIsColimit U).op
    (h.isSheafPairwiseIntersections U).some

Premises used: Nonempty.some, CategoryTheory.Limits.IsColimit.op, CategoryTheory.Pairwise.coconeIsColimit, TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
⊢ F.IsSheaf ↔ F.IsSheafPreservesLimitPairwiseIntersections

Tactic:
⟨fun h U ↦ h.isSheafPreservesLimitPairwiseIntersections,
    fun h ↦ F.isSheaf_iff_isSheafPairwiseIntersections.mpr fun ι U ↦ ?_⟩

Premises used: Iff.mpr, TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections, TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections, Iff.intro
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
refine :
  ∀ (h : F.IsSheafPreservesLimitPairwiseIntersections) (ι : Type w) (U : ι → Opens (↑X : Type w)),
    Nonempty (IsLimit (Functor.mapCone F (Cocone.op (Pairwise.cocone U))))
⊢ F.IsSheaf ↔ F.IsSheafPreservesLimitPairwiseIntersections

Tactic:
refine ⟨fun h U ↦ h.isSheafPreservesLimitPairwiseIntersections,
    fun h ↦ F.isSheaf_iff_isSheafPairwiseIntersections.mpr fun ι U ↦ ?_⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
h : F.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens (↑X : Type w)
⊢ PreservesLimit (Functor.op (Pairwise.diagram U)) F

Tactic:
haveI := h U
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
h : F.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens (↑X : Type w)
this : PreservesLimit (Functor.op (Pairwise.diagram U)) F
⊢ Nonempty (IsLimit (Functor.mapCone F (Cocone.op (Pairwise.cocone U))))

Tactic:
⟨isLimitOfPreserves _ (Pairwise.coconeIsColimit U).op⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.IsColimit.op, CategoryTheory.Pairwise.coconeIsColimit, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
h : F.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens (↑X : Type w)
this : PreservesLimit (Functor.op (Pairwise.diagram U)) F
⊢ Nonempty (IsLimit (Functor.mapCone F (Cocone.op (Pairwise.cocone U))))

Tactic:
exact ⟨isLimitOfPreserves _ (Pairwise.coconeIsColimit U).op⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
rw :
  Eq (α :=
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V)) ⟶
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊓ V)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)))
⊢ Eq (α :=
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V)) ⟶
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊓ V)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯)) ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯)) ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
rw [← F.1.map_comp, ← F.1.map_comp]

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
⊢ Eq (α :=
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V)) ⟶
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊓ V)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)))

Tactic:
congr 1
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
⊢ (F.interUnionPullbackCone U V).pt =
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
⊢ (F.interUnionPullbackCone U V).fst =
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
⊢ (F.interUnionPullbackCone U V).snd =
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
h : ∀ (x : (↑X : Type w)), x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) ↔ x ∈ (↑(iSup ι) : Set (↑X : Type w))
⊢ U ⊔ V = iSup ι

Tactic:
ext
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
x : (↑X : Type w)
h :
  x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) ↔
    ∃ (i : ULift.{w, 0} WalkingPair),
      x ∈
        (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) i.down U V :
              Opens (↑X : Type w)) :
          Set (↑X : Type w))
⊢ x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) ↔ x ∈ (↑(iSup ι) : Set (↑X : Type w))

Tactic:
rw [Opens.coe_iSup, Set.mem_iUnion]

Premises used: TopologicalSpace.Opens.coe_iSup, Set.mem_iUnion
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
x : (↑X : Type w)
h :
  x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) →
    ∃ (i : ULift.{w, 0} WalkingPair),
      x ∈
        (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) i.down U V :
              Opens (↑X : Type w)) :
          Set (↑X : Type w))
h₁ :
  (∃ (i : ULift.{w, 0} WalkingPair),
      x ∈
        (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) i.down U V :
              Opens (↑X : Type w)) :
          Set (↑X : Type w))) →
    x ∈ (↑(U ⊔ V) : Set (↑X : Type w))
⊢ x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) ↔
    ∃ (i : ULift.{w, 0} WalkingPair),
      x ∈
        (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) i.down U V :
              Opens (↑X : Type w)) :
          Set (↑X : Type w))

Tactic:
constructor
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
x : (↑X : Type w)
h : x ∈ (↑U : Set (↑X : Type w))
⊢ ∃ (i : ULift.{w, 0} WalkingPair),
    x ∈
      (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) i.down U V : Opens (↑X : Type w)) :
        Set (↑X : Type w))

Tactic:
⟨⟨WalkingPair.left⟩, h⟩

Premises used: Exists.intro, ULift.up, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
x : (↑X : Type w)
h : x ∈ (↑V : Set (↑X : Type w))
⊢ ∃ (i : ULift.{w, 0} WalkingPair),
    x ∈
      (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) i.down U V : Opens (↑X : Type w)) :
        Set (↑X : Type w))

Tactic:
⟨⟨WalkingPair.right⟩, h⟩

Premises used: CategoryTheory.Limits.WalkingPair.right, Exists.intro, ULift.up
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
x : (↑X : Type w)
h : x ∈ (↑U : Set (↑X : Type w))
⊢ ∃ (i : ULift.{w, 0} WalkingPair),
    x ∈
      (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) i.down U V : Opens (↑X : Type w)) :
        Set (↑X : Type w))

Tactic:
exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩]
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
x : (↑X : Type w)
h :
  x ∈
    (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w))
            (ULift.down.{w, 0} { down := WalkingPair.left : ULift.{w, 0} WalkingPair }) U V :
          Opens (↑X : Type w)) :
      Set (↑X : Type w))
⊢ x ∈ (↑(U ⊔ V) : Set (↑X : Type w))

Tactic:
Or.inl h

Premises used: Set.union, Set.Mem, setOf, Or.inl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
x : (↑X : Type w)
h :
  x ∈
    (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w))
            (ULift.down.{w, 0} { down := WalkingPair.right : ULift.{w, 0} WalkingPair }) U V :
          Opens (↑X : Type w)) :
      Set (↑X : Type w))
⊢ x ∈ (↑(U ⊔ V) : Set (↑X : Type w))

Tactic:
Or.inr h

Premises used: Set.union, Set.Mem, setOf, Or.inr
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
x : (↑X : Type w)
h :
  x ∈
    (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w))
            (ULift.down.{w, 0} { down := WalkingPair.left : ULift.{w, 0} WalkingPair }) U V :
          Opens (↑X : Type w)) :
      Set (↑X : Type w))
⊢ x ∈ (↑(U ⊔ V) : Set (↑X : Type w))

Tactic:
exacts [Or.inl h, Or.inr h]

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
⊢ U ⊔ V = iSup ι

Tactic:
have hι : U ⊔ V = iSup ι := by
    ext
    rw [Opens.coe_iSup, Set.mem_iUnion]
    constructor
    · rintro (h | h)
      exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩]
    · rintro ⟨⟨_ | _⟩, h⟩
      exacts [Or.inl h, Or.inr h]
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
hι : U ⊔ V = iSup ι
⊢ Functor.obj.{w, v_1, w, u_1} (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
      (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair })) ⟶
    (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.left }))

Tactic:
exacts [s.fst, s.snd, s.fst ≫ F.1.map (homOfLE inf_le_left).op,
      s.snd ≫ F.1.map (homOfLE inf_le_left).op]

Premises used: Quiver.Hom.op, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, CategoryTheory.homOfLE, CategoryTheory.Limits.PullbackCone.snd, inf_le_left
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
hι : U ⊔ V = iSup ι
i j : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)
f : op i ⟶ op j
g : j ⟶ i := f.unop
⊢ f = g.op

Tactic:
have : f = g.op := rfl