Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case single.single.id_single
C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.id_single i))))
      (objPairwiseOfFamily sf (op (Pairwise.single i))) =
    objPairwiseOfFamily sf (op (Pairwise.single i))

pp: case single.pair.left
C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i j' : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.left i j'))))
      (objPairwiseOfFamily sf (op (Pairwise.single i))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i j'))

pp: case single.pair.right
C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i i' : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.right i' i))))
      (objPairwiseOfFamily sf (op (Pairwise.single i))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i' i))

pp: case pair.pair.id_pair
C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i j : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.id_pair i j))))
      (objPairwiseOfFamily sf (op (Pairwise.pair i j))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))

Tactic:
· exact ConcreteCategory.congr_hom (G.map_id <| op <| Pairwise.single i) _

Goal state after:
case single.pair.left
C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i j' : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.left i j'))))
      (objPairwiseOfFamily sf (op (Pairwise.single i))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i j'))

case single.pair.right
C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i i' : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.right i' i))))
      (objPairwiseOfFamily sf (op (Pairwise.single i))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i' i))

case pair.pair.id_pair
C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i j : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.id_pair i j))))
      (objPairwiseOfFamily sf (op (Pairwise.pair i j))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))