Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case property.refine_3.single.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
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.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.single { down := WalkingPair.left })) =
    (F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.single { down := WalkingPair.left }))

pp: case property.refine_3.single.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
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.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.single { down := WalkingPair.right })) =
    (F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.single { down := WalkingPair.right }))

pp: case property.refine_3.pair.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
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
⊢ (m ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.pair { down := WalkingPair.left } a✝)) =
    (F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.pair { down := WalkingPair.left } a✝))

pp: case property.refine_3.pair.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
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
⊢ (m ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.pair { down := WalkingPair.right } a✝)) =
    (F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.pair { down := WalkingPair.right } a✝))

Tactic:
<;>

Goal state after:
case property.refine_3.single.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
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.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.single { down := WalkingPair.left })) =
    (F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.single { down := WalkingPair.left }))

case property.refine_3.single.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
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.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.single { down := WalkingPair.right })) =
    (F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.single { down := WalkingPair.right }))

case property.refine_3.pair.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
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
⊢ (m ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.pair { down := WalkingPair.left } a✝)) =
    (F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.pair { down := WalkingPair.left } a✝))

case property.refine_3.pair.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
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
⊢ (m ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.pair { down := WalkingPair.right } a✝)) =
    (F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op) ≫
      (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app (op (Pairwise.pair { down := WalkingPair.right } a✝))