mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
this : x''.Compatible
t : F.obj (op U)
ht : x''.IsAmalgamation t
ht' : ∀ (y : F.obj (op U)), (fun t ↦ x''.IsAmalgamation t) y → y = t
V : C
i : V ⟶ unop (op U)
hi : (Sieve.bind S.arrows fun V i hi ↦ G.sieveOfSection ↑(x i hi)).arrows i
⊢ (G.sieveOfSection t).arrows i

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
this : x''.Compatible
t : F.obj (op U)
ht : x''.IsAmalgamation t
ht' : ∀ (y : F.obj (op U)), (fun t ↦ x''.IsAmalgamation t) y → y = t
V : C
i : V ⟶ unop (op U)
hi : (Sieve.bind S.arrows fun V i hi ↦ G.sieveOfSection ↑(x i hi)).arrows i
⊢ (ConcreteCategory.hom (F.map i.op)) t ∈ G.obj (op V)
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj : (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows j
⊢ (G.familyOfElementsOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).map f j hj =
    (ConcreteCategory.hom (F'.map j.op))
      ((ConcreteCategory.hom ((↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map i)).toFun s)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj : (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows j
⊢ (ConcreteCategory.hom (f.app (op W)))
      (G.familyOfElementsOfSection (↑({ toFun := fun x ↦ ⟨(ConcreteCategory.hom (F.map i)) ↑x, ⋯⟩ } s)) j hj) =
    (ConcreteCategory.hom (F'.map j.op))
      ((ConcreteCategory.hom (F'.map i)) (⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯))
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection ↑s).arrows i
⊢ (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom (l₁.app U)).toFun s) =
    (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom (l₂.app U)).toFun s)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection ↑s).arrows i
⊢ (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom (l₁.app U)) s) =
    (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom (l₂.app U)) s)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
M : C
m : M ⟶ Y
hm : (Sieve.pullback (l ≫ h) (B hf)).arrows m
this : (Sieve.bind U.arrows B).arrows (m ≫ l ≫ h ≫ f)
⊢ s (m ≫ l ≫ h ≫ f) this =
    (ConcreteCategory.hom (P.map m.op))
      ((ConcreteCategory.hom (P.map l.op)) ((ConcreteCategory.hom (P.map h.op)) (t f hf)))

Tactic:
have h : s _ _ = _ := (ht hf _ hm).symm
      -- Porting note: this was done by `simp only [assoc] at`
      conv_lhs at h => congr; rw [assoc, assoc]
      simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
E : Type u_2
inst✝³ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
X : C
A B : (J.Cover X)ᵒᵖ
f : A ⟶ B
⊢ (J.diagram P X ⋙ F).map f ≫
      ((isLimitOfPreserves F (limit.isLimit ((unop B).index P).multicospan)).conePointUniqueUpToIso
            (limit.isLimit (((unop B).index P).multicospan ⋙ F)) ≪≫
          HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop B)).symm).hom =
    ((isLimitOfPreserves F (limit.isLimit ((unop A).index P).multicospan)).conePointUniqueUpToIso
            (limit.isLimit (((unop A).index P).multicospan ⋙ F)) ≪≫
          HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop A)).symm).hom ≫
      (J.diagram (P ⋙ F) X).map f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
E : Type u_2
inst✝³ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
X : C
A B : (J.Cover X)ᵒᵖ
f : A ⟶ B
⊢ F.map
        (Multiequalizer.lift ((unop B).index P) (multiequalizer ((unop A).index P))
          (fun I ↦ Multiequalizer.ι ((unop A).index P) (I.map f.unop)) ⋯) ≫
      ((isLimitOfPreserves F (limit.isLimit ((unop B).index P).multicospan)).conePointUniqueUpToIso
            (limit.isLimit (((unop B).index P).multicospan ⋙ F))).hom ≫
        (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop B)).symm).hom =
    (((isLimitOfPreserves F (limit.isLimit ((unop A).index P).multicospan)).conePointUniqueUpToIso
            (limit.isLimit (((unop A).index P).multicospan ⋙ F))).hom ≫
        (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop A)).symm).hom) ≫
      Multiequalizer.lift ((unop B).index (P ⋙ F)) (multiequalizer ((unop A).index (P ⋙ F)))
        (fun I ↦ Multiequalizer.ι ((unop A).index (P ⋙ F)) (I.map f.unop)) ⋯
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Mono ((sheafToPresheaf J (Type w)).map (Sheaf.imageι f))

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Mono (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case trans
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ IsSeparatedFor P (Sieve.pullback f (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S)).arrows

Tactic:
have : Sieve.pullback f (Sieve.bind R fun T (k : T ⟶ X) (_ : R k) => Sieve.pullback k S) =
        R.pullback f := by
      ext Z g
      constructor
      · rintro ⟨W, k, l, hl, _, comm⟩
        rw [pullback_apply, ← comm]
        simp [hl]
      · intro a
        refine ⟨Z, 𝟙 Z, _, a, ?_⟩
        simp [hf]

Goal state after:
case trans
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this✝ : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this : Sieve.pullback f (Sieve.bind R.arrows fun T k x ↦ Sieve.pullback k S) = Sieve.pullback f R
⊢ IsSeparatedFor P (Sieve.pullback f (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S)).arrows
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map
        (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
          (fun I ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) ≫
      (colimit.cocone (J.diagram P (unop Y) ⋙ F)).ι.app (op ((unop W).pullback f.unop)) ≫
        (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
    (colimit.cocone (J.diagram P (unop X) ⋙ F)).ι.app W ≫
      (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom ≫
        colimMap (J.diagramPullback (P ⋙ F) f.unop) ≫ colimit.pre (J.diagram (P ⋙ F) (unop Y)) (J.pullback f.unop).op

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map
        (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
          (fun I ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) ≫
      colimit.ι (J.diagram P (unop Y) ⋙ F) (op ((unop W).pullback f.unop)) ≫
        (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
    colimit.ι (J.diagram P (unop X) ⋙ F) W ≫
      (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom ≫
        colimMap (J.diagramPullback (P ⋙ F) f.unop) ≫ colimit.pre (J.diagram (P ⋙ F) (unop Y)) (J.pullback f.unop).op
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
⊢ (F.map
          (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
            (fun I ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) ≫
        (J.diagramCompIso F P (unop Y)).hom.app (op ((unop W).pullback f.unop))) ≫
      colimit.ι (J.diagram (P ⋙ F) (unop Y)) (op ((unop W).pullback f.unop)) =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj W)).index (P ⋙ F)) ((J.diagram (P ⋙ F) (unop X)).obj W)
          (fun I ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) (Cover.Arrow.base I)) ⋯) ≫
      colimit.ι (J.diagram (P ⋙ F) (unop Y)) ((J.pullback f.unop).op.obj W)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
⊢ (F.map
          (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
            (fun I ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) ≫
        (J.diagramCompIso F P (unop Y)).hom.app (op ((unop W).pullback f.unop))) ≫
      colimit.ι (J.diagram (P ⋙ F) (unop Y)) (op ((unop W).pullback f.unop)) =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift (((unop W).pullback f.unop).index (P ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun I ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) I.base) ⋯) ≫
      colimit.ι (J.diagram (P ⋙ F) (unop Y)) (op ((unop W).pullback f.unop))
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: case e_a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a✝ : ((unop W).pullback f.unop).shape.L
⊢ (F.map
          (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
            (fun I ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) ≫
        (J.diagramCompIso F P (unop Y)).hom.app (op ((unop W).pullback f.unop))) ≫
      Multiequalizer.ι (((unop W).pullback f.unop).index (P ⋙ F)) a✝ =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift (((unop W).pullback f.unop).index (P ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun I ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) I.base) ⋯) ≫
      Multiequalizer.ι (((unop W).pullback f.unop).index (P ⋙ F)) a✝

Tactic:
dsimp

Goal state after:
case e_a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a✝ : ((unop W).pullback f.unop).shape.L
⊢ (F.map
          (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
            (fun I ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) ≫
        (J.diagramCompIso F P (unop Y)).hom.app (op ((unop W).pullback f.unop))) ≫
      Multiequalizer.ι (((unop W).pullback f.unop).index (P ⋙ F)) a✝ =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift (((unop W).pullback f.unop).index (P ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun I ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) I.base) ⋯) ≫
      Multiequalizer.ι (((unop W).pullback f.unop).index (P ⋙ F)) a✝
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
K : Type z
inst✝ : Category.{z', z} K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
⊢ S.ι (W.shape.fst i) ≫ (((Functor.const K).obj E.pt).obj k).map i.r.g₁.op ≫ (E.π.app k).app (op i.r.Z) =
    S.ι (W.shape.snd i) ≫ (((Functor.const K).obj E.pt).obj k).map i.r.g₂.op ≫ (E.π.app k).app (op i.r.Z)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
K : Type z
inst✝ : Category.{z', z} K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
⊢ S.ι i.fst ≫ E.pt.map i.r.g₁.op ≫ (E.π.app k).app (op i.r.Z) =
    S.ι i.snd ≫ E.pt.map i.r.g₂.op ≫ (E.π.app k).app (op i.r.Z)
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
f : j ⟶ j'
⊢ ((const J).obj (colimit.cocone (curry.obj (swap K J ⋙ F) ⋙ lim)).1).map f ≫
      colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
        { pt := (colimit.cocone ((curry.obj F).obj j')).1,
          ι :=
            { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((curry.obj F).obj j') k,
              naturality := ⋯ } } =
    colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
        { pt := (colimit.cocone ((curry.obj F).obj j)).1,
          ι :=
            { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
              naturality := ⋯ } } ≫
      (curry.obj F ⋙ colim).map f

Tactic:
dsimp

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
f : j ⟶ j'
⊢ 𝟙 (colimit (curry.obj (swap K J ⋙ F) ⋙ lim)) ≫
      colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
        { pt := colimit ((curry.obj F).obj j'),
          ι :=
            { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((curry.obj F).obj j') k,
              naturality := ⋯ } } =
    colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
        { pt := colimit ((curry.obj F).obj j),
          ι :=
            { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
              naturality := ⋯ } } ≫
      colimMap ((curry.obj F).map f)
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁵ : Category.{v₁, u₁} J
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
⊢ (colim.map (limitIsoSwapCompLim G).hom ≫
        colimitLimitToLimitColimit (uncurry.obj G) ≫ lim.map (whiskerRight (currying.unitIso.app G).inv colim)) ≫
      (limit.cone (G ⋙ colim)).π.app j =
    (colim.mapCone (limit.cone G)).π.app j

Tactic:
dsimp

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁵ : Category.{v₁, u₁} J
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
⊢ (colimMap (limitIsoSwapCompLim G).hom ≫
        colimitLimitToLimitColimit (uncurry.obj G) ≫ limMap (whiskerRight (currying.unitIso.inv.app G) colim)) ≫
      limit.π (G ⋙ colim) j =
    colimMap (limit.π G j)
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i : W.shape.L
k : K
⊢ (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S) ≫
      (E.π.app k).app (op X) ≫ ((F ⋙ sheafToPresheaf J D).obj k).map i.f.op =
    S.ι i ≫ (E.π.app k).app (op i.Y)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i : W.shape.L
k : K
⊢ (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S) ≫
      (E.π.app k).app (op X) ≫ (F.obj k).obj.map i.f.op =
    S.ι i ≫ (E.π.app k).app (op i.Y)