Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_2.single.left.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 j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
g : Pairwise.pair { down := WalkingPair.left } { down := down✝ } ⟶ Pairwise.single { down := WalkingPair.left }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn (op (Pairwise.pair { down := WalkingPair.left } { down := down✝ })) 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.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) =
    (Opposite.casesOn (op (Pairwise.single { down := WalkingPair.left })) 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.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) ≫
      ((Pairwise.diagram ι).op ⋙ F.presheaf).map g.op

Tactic:
rcases g with ⟨⟩

Goal state after:
case refine_2.single.left.pair.left.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 j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).map
        (Quiver.Hom.op (Pairwise.Hom.left { down := WalkingPair.left } { down := down✝ })) ≫
      Opposite.casesOn (op (Pairwise.pair { down := WalkingPair.left } { down := down✝ })) 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.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) =
    (Opposite.casesOn (op (Pairwise.single { down := WalkingPair.left })) 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.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) ≫
      ((Pairwise.diagram ι).op ⋙ F.presheaf).map
        (Quiver.Hom.op (Pairwise.Hom.left { down := WalkingPair.left } { down := down✝ }))

case refine_2.single.left.pair.left.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 j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).map
        (Quiver.Hom.op (Pairwise.Hom.right { down := WalkingPair.left } { down := WalkingPair.left })) ≫
      Opposite.casesOn (op (Pairwise.pair { down := WalkingPair.left } { down := WalkingPair.left })) 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.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) =
    (Opposite.casesOn (op (Pairwise.single { down := WalkingPair.left })) 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.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) ≫
      ((Pairwise.diagram ι).op ⋙ F.presheaf).map
        (Quiver.Hom.op (Pairwise.Hom.right { down := WalkingPair.left } { down := WalkingPair.left }))