awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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)) ↔
    ∃ (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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (hypothesis)
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
⊢ s.pt ⟶ F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V))
have hι : 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]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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 ⟶ F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V))
have refine_1 : (X_1 : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) →
  Functor.obj.{w, v_1, w, u_1} (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
      X_1 ⟶
    (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj X_1
Tactic: refine
    (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.lift
        ⟨s.pt,
          { app := ?_
            naturality := ?_ }⟩ ≫
      F.1.map (eqToHom hι).op
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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.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 ⋯)))
have 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 sorry)))
  (s.fst ≫ F.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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 (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 ⋯)))
have 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 sorry) ≫ Quiver.Hom.op (eqToHom sorry)))
  (s.fst ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (eqToHom sorry)))
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]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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 ι
have h : ∀ (x : (↑X : Type w)), x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) ↔ x ∈ (↑(iSup ι) : Set (↑X : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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)
⊢ x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) ↔ x ∈ (↑(iSup ι) : Set (↑X : Type w))
have 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))
Tactic: rw [Opens.coe_iSup, Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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)
⊢ 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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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)) ↔
    ∃ (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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (hypothesis)
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
⊢ IsLimit (F.interUnionPullbackCone U V)
have hι : 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]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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 ι
⊢ IsLimit (F.interUnionPullbackCone U V)
have 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 sorry)))
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE sorry)))) →
  { 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: apply PullbackCone.isLimitAux'
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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 ⋯)))
⊢ { 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 }
have 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
Tactic: use interUnionPullbackConeLift F U V s
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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
have property : F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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).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
have property₁ : F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd
Tactic: refine ⟨?_, ?_, ?_⟩