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_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
⊢ 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₂ : ∀ {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 ⟨?_, ?_, ?_⟩
-- 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 ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
⊢ m = F.interUnionPullbackConeLift U V s
have property : m ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry)) =
  F.interUnionPullbackConeLift U V s ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry))
Tactic: rw [← cancel_mono (F.1.map (eqToHom hι.symm).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_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 ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
⊢ m ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom ⋯)) =
    F.interUnionPullbackConeLift U V s ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom ⋯))
have property : ∀ (j : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ),
  (m ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom sorry))) ≫
      (Functor.mapCone F.presheaf (Cocone.op (Pairwise.cocone ι))).π.app j =
    (F.interUnionPullbackConeLift U V s ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom sorry))) ≫
      (Functor.mapCone F.presheaf (Cocone.op (Pairwise.cocone ι))).π.app j
Tactic: apply (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.hom_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_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 ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
⊢ Eq (α :=
    s.pt ⟶ (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.left })))
    ((m ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯))) ≫
      (Functor.mapCone F.presheaf (Cocone.op (Pairwise.cocone ι))).π.app
        (op (Pairwise.single { down := WalkingPair.left })))
    ((F.interUnionPullbackConeLift U V s ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯))) ≫
      (Functor.mapCone F.presheaf (Cocone.op (Pairwise.cocone ι))).π.app
        (op (Pairwise.single { down := WalkingPair.left })))
have property : Eq (α := s.pt ⟶ (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.left })))
  (m ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry) ≫
        NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.single { down := WalkingPair.left }))))
  (F.interUnionPullbackConeLift U V s ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry) ≫
        NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.single { down := WalkingPair.left }))))
Tactic: rw [Category.assoc, Category.assoc, Functor.mapCone_π_app, ← 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_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 ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
⊢ Eq (α :=
    s.pt ⟶ (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.right })))
    ((m ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯))) ≫
      (Functor.mapCone F.presheaf (Cocone.op (Pairwise.cocone ι))).π.app
        (op (Pairwise.single { down := WalkingPair.right })))
    ((F.interUnionPullbackConeLift U V s ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯))) ≫
      (Functor.mapCone F.presheaf (Cocone.op (Pairwise.cocone ι))).π.app
        (op (Pairwise.single { down := WalkingPair.right })))
have property : Eq (α := s.pt ⟶ (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.right })))
  (m ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry) ≫
        NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.single { down := WalkingPair.right }))))
  (F.interUnionPullbackConeLift U V s ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry) ≫
        NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.single { down := WalkingPair.right }))))
Tactic: rw [Category.assoc, Category.assoc, Functor.mapCone_π_app, ← 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_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 ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a : ULift.{w, 0} WalkingPair
⊢ Eq (α :=
    s.pt ⟶ (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := WalkingPair.left } a)))
    ((m ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯))) ≫
      (Functor.mapCone F.presheaf (Cocone.op (Pairwise.cocone ι))).π.app
        (op (Pairwise.pair { down := WalkingPair.left } a)))
    ((F.interUnionPullbackConeLift U V s ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯))) ≫
      (Functor.mapCone F.presheaf (Cocone.op (Pairwise.cocone ι))).π.app
        (op (Pairwise.pair { down := WalkingPair.left } a)))
have property : Eq (α := s.pt ⟶ (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := WalkingPair.left } a)))
  (m ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry) ≫
        NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.pair { down := WalkingPair.left } a))))
  (F.interUnionPullbackConeLift U V s ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry) ≫
        NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.pair { down := WalkingPair.left } a))))
Tactic: rw [Category.assoc, Category.assoc, Functor.mapCone_π_app, ← 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_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 ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a : ULift.{w, 0} WalkingPair
⊢ Eq (α :=
    s.pt ⟶ (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := WalkingPair.right } a)))
    ((m ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯))) ≫
      (Functor.mapCone F.presheaf (Cocone.op (Pairwise.cocone ι))).π.app
        (op (Pairwise.pair { down := WalkingPair.right } a)))
    ((F.interUnionPullbackConeLift U V s ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯))) ≫
      (Functor.mapCone F.presheaf (Cocone.op (Pairwise.cocone ι))).π.app
        (op (Pairwise.pair { down := WalkingPair.right } a)))
have property : Eq (α := s.pt ⟶ (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := WalkingPair.right } a)))
  (m ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry) ≫
        NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.pair { down := WalkingPair.right } a))))
  (F.interUnionPullbackConeLift U V s ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry) ≫
        NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.pair { down := WalkingPair.right } a))))
Tactic: rw [Category.assoc, Category.assoc, Functor.mapCone_π_app, ← 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_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 ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
⊢ Eq (α :=
    s.pt ⟶ (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.left })))
    (m ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom ⋯) ≫
          NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.single { down := WalkingPair.left }))))
    (F.interUnionPullbackConeLift U V s ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom ⋯) ≫
          NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.single { down := WalkingPair.left }))))
have h : (s.pt ⟶
      (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj
        (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair }))) =
    (s.pt ⟶ F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U)) →
  F.interUnionPullbackConeLift U V s ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom sorry) ≫
          NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.single { down := WalkingPair.left }))) =
    s.fst
Tactic: convert! h₁