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 ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.single { down := WalkingPair.left }))) =
    F.interUnionPullbackConeLift U V s ≫
      F.obj.map ((eqToHom ⋯).op ≫ (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 ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.single { down := WalkingPair.right }))) =
    F.interUnionPullbackConeLift U V s ≫
      F.obj.map ((eqToHom ⋯).op ≫ (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 ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.pair { down := WalkingPair.left } a✝))) =
    F.interUnionPullbackConeLift U V s ≫
      F.obj.map ((eqToHom ⋯).op ≫ (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 ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.pair { down := WalkingPair.right } a✝))) =
    F.interUnionPullbackConeLift U V s ≫
      F.obj.map ((eqToHom ⋯).op ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.pair { down := WalkingPair.right } a✝)))

Tactic:
· convert! h₁
      apply interUnionPullbackConeLift_left

Goal state after:
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 ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.single { down := WalkingPair.right }))) =
    F.interUnionPullbackConeLift U V s ≫
      F.obj.map ((eqToHom ⋯).op ≫ (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 ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.pair { down := WalkingPair.left } a✝))) =
    F.interUnionPullbackConeLift U V s ≫
      F.obj.map ((eqToHom ⋯).op ≫ (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 ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.pair { down := WalkingPair.right } a✝))) =
    F.interUnionPullbackConeLift U V s ≫
      F.obj.map ((eqToHom ⋯).op ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.pair { down := WalkingPair.right } a✝)))