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
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 ι
⊢ 𝟙 s.pt ≫ s.fst = s.fst ≫ F.presheaf.map (𝟙 (op (ι { down := WalkingPair.left })))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_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)
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 ι
down : WalkingPair
⊢ Eq (α := s.pt ⟶ F.presheaf.obj (op (ι { down := WalkingPair.left } ⊓ ι { down := down })))
    (𝟙 s.pt ≫
      s.fst ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE ⋯)))
    (s.fst ≫ F.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_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)
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 ι
⊢ Eq (α := s.pt ⟶ F.presheaf.obj (op (ι { down := WalkingPair.left } ⊓ ι { down := WalkingPair.left })))
    (𝟙 s.pt ≫
      s.fst ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE ⋯)))
    (s.fst ≫ F.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_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)
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 ι
refine_2 :
  Eq (α := s.pt ⟶ F.presheaf.obj (op (V ⊓ U)))
    (s.snd ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯)))
    (s.fst ≫ F.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ Eq (α := s.pt ⟶ F.presheaf.obj (op (ι { down := WalkingPair.right } ⊓ ι { down := WalkingPair.left })))
    (𝟙 s.pt ≫
      s.snd ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE ⋯)))
    (s.fst ≫ F.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_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)
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 ι
⊢ 𝟙 s.pt ≫ s.snd = s.snd ≫ F.presheaf.map (𝟙 (op (ι { down := WalkingPair.right })))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_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)
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 ι
⊢ Eq (α := s.pt ⟶ F.presheaf.obj (op (ι { down := WalkingPair.left } ⊓ ι { down := WalkingPair.right })))
    (𝟙 s.pt ≫
      s.fst ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE ⋯)))
    (s.snd ≫ F.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_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)
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 ι
down : WalkingPair
⊢ Eq (α := s.pt ⟶ F.presheaf.obj (op (ι { down := WalkingPair.right } ⊓ ι { down := down })))
    (𝟙 s.pt ≫
      s.snd ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE ⋯)))
    (s.snd ≫ F.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_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)
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 ι
⊢ Eq (α := s.pt ⟶ F.presheaf.obj (op (ι { down := WalkingPair.right } ⊓ ι { down := WalkingPair.right })))
    (𝟙 s.pt ≫
      s.snd ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE ⋯)))
    (s.snd ≫ F.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_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)
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 ι
down : WalkingPair
⊢ 𝟙 s.pt ≫
      s.fst ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE ⋯)) =
    (s.fst ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE ⋯))) ≫
      F.presheaf.map
        (𝟙
          (op
            (ι { down := WalkingPair.left : ULift.{w, 0} WalkingPair } ⊓
              ι { down := down : ULift.{w, 0} WalkingPair })))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_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)
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 ι
down : WalkingPair
⊢ 𝟙 s.pt ≫
      s.snd ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE ⋯)) =
    (s.snd ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE ⋯))) ≫
      F.presheaf.map
        (𝟙
          (op
            (ι { down := WalkingPair.right : ULift.{w, 0} WalkingPair } ⊓
              ι { down := down : ULift.{w, 0} WalkingPair })))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_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)
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 ι
refine_2 :
  Eq (α :=
    s.pt ⟶ F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊓ V)))
    (s.snd ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯)))
    (s.fst ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯)))
⊢ Eq (α := s.pt ⟶ F.presheaf.obj (op (V ⊓ U)))
    (s.snd ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯)))
    (s.fst ≫ F.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
rw [← cancel_mono (F.1.map (eqToHom <| inf_comm U V : U ⊓ V ⟶ _).op), Category.assoc,
    Category.assoc, ← F.1.map_comp, ← F.1.map_comp]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.op, CategoryTheory.eqToHom, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.cancel_mono, inf_comm, CategoryTheory.Functor.map, 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)
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 ι
⊢ Eq (α :=
    s.pt ⟶ F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊓ V)))
    (s.snd ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯)))
    (s.fst ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯)))

Tactic:
s.condition.symm

Premises used: CategoryTheory.Limits.PullbackCone.condition, Set.Mem, CategoryTheory.homOfLE, Eq.symm
-- 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 ι
⊢ Eq (α :=
    s.pt ⟶ F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊓ V)))
    (s.snd ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯)))
    (s.fst ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯)))

Tactic:
exact s.condition.symm

Premises used: CategoryTheory.Limits.PullbackCone.condition, Eq.symm
-- 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 (x : ULift.{w, 0} WalkingPair) ↦
    match (motive := ULift.{w, 0} WalkingPair → Opens (↑X : Type w)) x with
    | { down := j } => WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j 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 (x : ULift.{w, 0} WalkingPair) ↦
    match (motive := ULift.{w, 0} WalkingPair → Opens (↑X : Type w)) x with
    | { down := j } => WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j U V
x : (↑X : Type w)
h :
  x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) ↔
    ∃ (i : ULift.{w, 0} WalkingPair),
      x ∈
        (↑(match (motive := ULift.{w, 0} WalkingPair → Opens (↑X : Type w)) i with
              | { down := j } => WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j 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