-- Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean
theorem interUnionPullbackConeLift_right :
    interUnionPullbackConeLift F U V s ≫ F.1.map (homOfLE le_sup_right).op = s.snd

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.val.map (homOfLE ⋯).op) (F.val.map (homOfLE ⋯).op)
⊢ F.interUnionPullbackConeLift U V s ≫ F.val.map (homOfLE ⋯).op = s.snd

Tactic:
erw [Category.assoc]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.val.map (homOfLE ⋯).op) (F.val.map (homOfLE ⋯).op)
⊢ ⋯.some.lift
        { pt := s.pt,
          π :=
            {
              app := fun X_1 =>
                Opposite.casesOn X_1 fun unop =>
                  Pairwise.casesOn unop (fun a => ULift.casesOn a fun down => WalkingPair.casesOn down s.fst s.snd)
                    fun a a_1 =>
                    ULift.casesOn a fun down =>
                      WalkingPair.casesOn down (s.fst ≫ F.val.map (homOfLE ⋯).op) (s.snd ≫ F.val.map (homOfLE ⋯).op),
              naturality := ⋯ } } ≫
      F.val.map (eqToHom ⋯).op ≫ F.val.map (homOfLE ⋯).op =
    s.snd

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.val.map (homOfLE ⋯).op) (F.val.map (homOfLE ⋯).op)
⊢ ⋯.some.lift
        { pt := s.pt,
          π :=
            {
              app := fun X_1 =>
                Opposite.casesOn X_1 fun unop =>
                  Pairwise.casesOn unop (fun a => ULift.casesOn a fun down => WalkingPair.casesOn down s.fst s.snd)
                    fun a a_1 =>
                    ULift.casesOn a fun down =>
                      WalkingPair.casesOn down (s.fst ≫ F.val.map (homOfLE ⋯).op) (s.snd ≫ F.val.map (homOfLE ⋯).op),
              naturality := ⋯ } } ≫
      F.val.map (eqToHom ⋯).op ≫ F.val.map (homOfLE ⋯).op =
    s.snd

Tactic:
simp_rw [← F.1.map_comp]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.val.map (homOfLE ⋯).op) (F.val.map (homOfLE ⋯).op)
⊢ ⋯.some.lift
        { pt := s.pt,
          π :=
            {
              app := fun X_1 =>
                Pairwise.rec (fun a => WalkingPair.rec s.fst s.snd a.down)
                  (fun a a_1 =>
                    WalkingPair.rec (s.fst ≫ F.val.map (homOfLE ⋯).op) (s.snd ≫ F.val.map (homOfLE ⋯).op) a.down)
                  (unop X_1),
              naturality := ⋯ } } ≫
      F.val.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    s.snd

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.val.map (homOfLE ⋯).op) (F.val.map (homOfLE ⋯).op)
⊢ ⋯.some.lift
        { pt := s.pt,
          π :=
            {
              app := fun X_1 =>
                Pairwise.rec (fun a => WalkingPair.rec s.fst s.snd a.down)
                  (fun a a_1 =>
                    WalkingPair.rec (s.fst ≫ F.val.map (homOfLE ⋯).op) (s.snd ≫ F.val.map (homOfLE ⋯).op) a.down)
                  (unop X_1),
              naturality := ⋯ } } ≫
      F.val.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    s.snd

Tactic:
exact
  (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
    op <| Pairwise.single <| ULift.up WalkingPair.right

Result:
no goals