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 (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))
h₁ :
  (∃ (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 ∈ (↑(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))

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 (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 : 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))

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 (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 ∈ (↑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))

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 (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 : 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))

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 (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 ∈
    (↑(match (motive := ULift.{w, 0} WalkingPair → Opens (↑X : Type w))
            { down := WalkingPair.left : ULift.{w, 0} WalkingPair } 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))

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 (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 ∈
    (↑(match (motive := ULift.{w, 0} WalkingPair → Opens (↑X : Type w))
            { down := WalkingPair.right : ULift.{w, 0} WalkingPair } 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))

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 (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 ∈
    (↑(match (motive := ULift.{w, 0} WalkingPair → Opens (↑X : Type w))
            { down := WalkingPair.left : ULift.{w, 0} WalkingPair } 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))

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 (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
⊢ 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 (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ι : U ⊔ V = iSup ι
create :
  (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 ⋯)))) →
    { l : s.pt ⟶ (F.interUnionPullbackCone U V).pt //
      l ≫ (F.interUnionPullbackCone U V).fst = s.fst ∧
        l ≫ (F.interUnionPullbackCone U V).snd = s.snd ∧
          ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
            m ≫ (F.interUnionPullbackCone U V).fst = s.fst → m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = l }
⊢ IsLimit (F.interUnionPullbackCone U V)

Tactic:
apply PullbackCone.isLimitAux'

Premises used: CategoryTheory.Limits.PullbackCone.isLimitAux'
-- 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_1 :
  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ι : U ⊔ V = iSup ι
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 ⋯)))
property :
  F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst ∧
    F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
        m ≫ (F.interUnionPullbackCone U V).fst = s.fst →
          m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = F.interUnionPullbackConeLift U V s
⊢ { l : s.pt ⟶ (F.interUnionPullbackCone U V).pt //
    l ≫ (F.interUnionPullbackCone U V).fst = s.fst ∧
      l ≫ (F.interUnionPullbackCone U V).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
          m ≫ (F.interUnionPullbackCone U V).fst = s.fst → m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = l }

Tactic:
use interUnionPullbackConeLift F U V s

Premises used: TopCat.Sheaf.interUnionPullbackConeLift
-- 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_1 :
  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ι : U ⊔ V = iSup ι
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 ⋯)))
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst ∧
    F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
        m ≫ (F.interUnionPullbackCone U V).fst = s.fst →
          m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = F.interUnionPullbackConeLift U V s

Tactic:
⟨?_, ?_, ?_⟩

Premises used: And.intro
-- 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_1 :
  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ι : U ⊔ V = iSup ι
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 ⋯)))
property : F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst
property₁ : F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd
property₂ :
  ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
    m ≫ (F.interUnionPullbackCone U V).fst = s.fst →
      m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = F.interUnionPullbackConeLift U V s
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst ∧
    F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
        m ≫ (F.interUnionPullbackCone U V).fst = s.fst →
          m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = F.interUnionPullbackConeLift U V s

Tactic:
refine ⟨?_, ?_, ?_⟩
-- 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_1 :
  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ι : U ⊔ V = iSup ι
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 ⋯)))
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst

Tactic:
apply interUnionPullbackConeLift_left

Premises used: TopCat.Sheaf.interUnionPullbackConeLift_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_1 :
  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ι : U ⊔ V = iSup ι
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 ⋯)))
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd

Tactic:
apply interUnionPullbackConeLift_right

Premises used: TopCat.Sheaf.interUnionPullbackConeLift_right