mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: case h
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ ∀ (j j' : J) (f : j ⟶ j'),
    (ConcreteCategory.hom (((curry.obj (swap K J ⋙ F)).obj k'').map f))
        ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j)) =
      (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j')))) (y j')

Tactic:
dsimp

Goal state after:
case h
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ ∀ (j j' : J) (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (f ×ₘ 𝟙 k'')))
        ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j)) =
      (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j')))) (y j')
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case left
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this✝ : PreservesColimitsOfSize.{?u.122, ?u.121, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
Z : C
f : Z ⟶ (colimit.cocone (pair (Gr.obj X) (Gr.obj Y))).pt
⊢ PreservesLimit (cospan f ((colimit.cocone (pair (Gr.obj X) (Gr.obj Y))).ι.app { as := WalkingPair.left })) Gl

Tactic:
dsimp

Goal state after:
case left
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this✝ : PreservesColimitsOfSize.{?u.122, ?u.121, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
Z : C
f : Z ⟶ (colimit.cocone (pair (Gr.obj X) (Gr.obj Y))).pt
⊢ PreservesLimit (cospan f (colimit.ι (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.left })) Gl
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case right
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this✝ : PreservesColimitsOfSize.{?u.122, ?u.121, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
Z : C
f : Z ⟶ (colimit.cocone (pair (Gr.obj X) (Gr.obj Y))).pt
⊢ PreservesLimit (cospan f ((colimit.cocone (pair (Gr.obj X) (Gr.obj Y))).ι.app { as := WalkingPair.right })) Gl

Tactic:
dsimp

Goal state after:
case right
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this✝ : PreservesColimitsOfSize.{?u.122, ?u.121, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
Z : C
f : Z ⟶ (colimit.cocone (pair (Gr.obj X) (Gr.obj Y))).pt
⊢ PreservesLimit (cospan f (colimit.ι (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.right })) Gl
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case left
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁶ : FinitaryExtensive D
inst✝⁵ : HasFiniteCoproducts C
inst✝⁴ : HasPullbacksOfInclusions C
inst✝³ : PreservesPullbacksOfInclusions F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
Z : C
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan f ((BinaryCofan.mk coprod.inl coprod.inr).ι.app { as := WalkingPair.left })) F

Tactic:
dsimp

Goal state after:
case left
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁶ : FinitaryExtensive D
inst✝⁵ : HasFiniteCoproducts C
inst✝⁴ : HasPullbacksOfInclusions C
inst✝³ : PreservesPullbacksOfInclusions F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
Z : C
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan f coprod.inl) F
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case right
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁶ : FinitaryExtensive D
inst✝⁵ : HasFiniteCoproducts C
inst✝⁴ : HasPullbacksOfInclusions C
inst✝³ : PreservesPullbacksOfInclusions F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
Z : C
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan f ((BinaryCofan.mk coprod.inl coprod.inr).ι.app { as := WalkingPair.right })) F

Tactic:
dsimp

Goal state after:
case right
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁶ : FinitaryExtensive D
inst✝⁵ : HasFiniteCoproducts C
inst✝⁴ : HasPullbacksOfInclusions C
inst✝³ : PreservesPullbacksOfInclusions F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
Z : C
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan f coprod.inr) F
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)} (hc : IsColimit c), IsUniversalColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ ∀ {Z : C} (i : Z ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    HasPullback (BinaryCofan.mk coprod.inl coprod.inr).inr i

Tactic:
dsimp

Goal state after:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)} (hc : IsColimit c), IsUniversalColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ ∀ {Z : C} (i : Z ⟶ f 0 ⨿ ∐ fun i ↦ f i.succ), HasPullback coprod.inr i
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ ∀ {Z : C} (i : Z ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    HasPullback (BinaryCofan.mk coprod.inl coprod.inr).inr i

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ ∀ {Z : C} (i : Z ⟶ f 0 ⨿ ∐ fun i ↦ f i.succ), HasPullback coprod.inr i
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{t, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝ : SmallCategory K
F : K ⥤ Cᵒᵖ ⥤ D
W : J.Cover X
i : W.Arrow
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj (op W))
a b : K
f : a ⟶ b
⊢ ((Functor.const K).obj E.pt).map f ≫ E.π.app b ≫ Multiequalizer.ι (W.index (F.obj b)) i =
    (E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i) ≫ (F ⋙ (evaluation Cᵒᵖ D).obj (op i.Y)).map f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{t, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝ : SmallCategory K
F : K ⥤ Cᵒᵖ ⥤ D
W : J.Cover X
i : W.Arrow
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj (op W))
a b : K
f : a ⟶ b
⊢ 𝟙 E.pt ≫ E.π.app b ≫ Multiequalizer.ι (W.index (F.obj b)) i =
    (E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i) ≫ (F.map f).app (op i.Y)
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{t, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Cᵒᵖ ⥤ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
i : (unop W).shape.R
⊢ liftToDiagramLimitObjAux F E ((unop W).shape.fst i) ≫ ((unop W).index (limit F)).fst i =
    liftToDiagramLimitObjAux F E ((unop W).shape.snd i) ≫ ((unop W).index (limit F)).snd i

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{t, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Cᵒᵖ ⥤ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
i : (unop W).shape.R
⊢ liftToDiagramLimitObjAux F E i.fst ≫ (limit F).map i.r.g₁.op =
    liftToDiagramLimitObjAux F E i.snd ≫ (limit F).map i.r.g₂.op
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{t, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Cᵒᵖ ⥤ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
m : E.pt ⟶ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).pt
hm :
  ∀ (j : K),
    m ≫ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j = E.π.app j
a : (unop W).shape.L
j : K
⊢ m ≫ Multiequalizer.ι ((unop W).index (limit F)) a ≫ (limit.π F j).app (op a.Y) =
    m ≫
      ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j ≫
        Multiequalizer.ι ((unop W).index (F.obj j)) a

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{t, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Cᵒᵖ ⥤ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
m : E.pt ⟶ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).pt
hm :
  ∀ (j : K),
    m ≫ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j = E.π.app j
a : (unop W).shape.L
j : K
⊢ m ≫ Multiequalizer.ι ((unop W).index (limit F)) a ≫ (limit.π F j).app (op a.Y) =
    m ≫
      Multiequalizer.lift ((unop W).index (F.obj j)) (multiequalizer ((unop W).index (limit F)))
          (fun x ↦ Multiequalizer.ι ((unop W).index (limit F)) x ≫ (limit.π F j).app (op x.Y)) ⋯ ≫
        Multiequalizer.ι ((unop W).index (F.obj j)) a
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{t, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Cᵒᵖ ⥤ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
m : E.pt ⟶ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).pt
hm :
  ∀ (j : K),
    m ≫ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j = E.π.app j
a : (unop W).shape.L
j : K
⊢ m ≫ Multiequalizer.ι ((unop W).index (limit F)) a ≫ (limit.π F j).app (op a.Y) =
    m ≫
      (Multifork.ofι ((unop W).index (F.obj j)) (multiequalizer ((unop W).index (limit F)))
              (fun x ↦ Multiequalizer.ι ((unop W).index (limit F)) x ≫ (limit.π F j).app (op x.Y)) ⋯).π.app
        (WalkingMulticospan.left a)

Tactic:
dsimp

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

Goal state before:
pp: case e_a
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
⊢ ((HasLimit.isoOfNatIso
            (NatIso.ofComponents (fun k ↦ colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k)
                ⋯).symm).hom ≫
        (colimitLimitIso (F ⋙ J.diagramFunctor D X)).inv ≫
          (HasColimit.isoOfNatIso
              ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
                (limit.isLimit (F ⋙ J.diagramFunctor D X)))).inv) ≫
      (J.plusMap (limit.π F k)).app (op X) =
    (limit.cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).π.app k

Tactic:
dsimp

Goal state after:
case e_a
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
⊢ ((HasLimit.isoOfNatIso
            (NatIso.ofComponents (fun k ↦ colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k)
                ⋯).symm).hom ≫
        (colimitLimitIso (F ⋙ J.diagramFunctor D X)).inv ≫
          (HasColimit.isoOfNatIso
              ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
                (limit.isLimit (F ⋙ J.diagramFunctor D X)))).inv) ≫
      (J.plusMap (limit.π F k)).app (op X) =
    limit.π (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) k
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: case e_a
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F)))
        (fun x ↦ Multiequalizer.ι ((unop j).index (limit F)) x ≫ (limit.π F k).app (op x.Y)) ⋯ ≫
      colimit.ι (J.diagram (F.obj k) X) j =
    (limit.lift (F ⋙ J.diagramFunctor D X) ((J.diagramFunctor D X).mapCone (limit.cone F))).app j ≫
      colimit.ι (limit (F ⋙ J.diagramFunctor D X)) j ≫
        (colimitLimitIso (F ⋙ J.diagramFunctor D X)).hom ≫
          ((Cone.postcompose
                      (NatIso.ofComponents
                          (fun k ↦ colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) ⋯).hom).obj
                  (limit.cone (colimit (F ⋙ J.diagramFunctor D X).flip))).π.app
            k

Tactic:
dsimp

Goal state after:
case e_a
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F)))
        (fun x ↦ Multiequalizer.ι ((unop j).index (limit F)) x ≫ (limit.π F k).app (op x.Y)) ⋯ ≫
      colimit.ι (J.diagram (F.obj k) X) j =
    (limit.lift (F ⋙ J.diagramFunctor D X) ((J.diagramFunctor D X).mapCone (limit.cone F))).app j ≫
      colimit.ι (limit (F ⋙ J.diagramFunctor D X)) j ≫
        (colimitLimitIso (F ⋙ J.diagramFunctor D X)).hom ≫
          limit.π (colimit (F ⋙ J.diagramFunctor D X).flip) k ≫
            (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).hom
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : Cᵒᵖ
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X)
m : S.pt ⟶ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).pt
hm : ∀ (j : K), m ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j = S.π.app j
k✝ : K
k : (J.Cover (unop X))ᵒᵖ
| ((Cocone.precompose
                ((isLimitOfPreserves (J.diagramFunctor D (unop X)) (limit.isLimit F)).conePointUniqueUpToIso
                    (limit.isLimit (F ⋙ J.diagramFunctor D (unop X)))).hom).obj
            (colimit.cocone (limit (F ⋙ J.diagramFunctor D (unop X))))).ι.app
      k ≫
    (colimitLimitIso (F ⋙ J.diagramFunctor D (unop X))).hom ≫
      ((Cone.postcompose
                  (NatIso.ofComponents
                        (fun k ↦ colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D (unop X)).flip k)
                        ⋯).symm.inv).obj
              (limit.cone (colimit (F ⋙ J.diagramFunctor D (unop X)).flip))).π.app
        k✝

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : Cᵒᵖ
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X)
m : S.pt ⟶ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).pt
hm : ∀ (j : K), m ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j = S.π.app j
k✝ : K
k : (J.Cover (unop X))ᵒᵖ
| (((isLimitOfPreserves (J.diagramFunctor D (unop X)) (limit.isLimit F)).conePointUniqueUpToIso
              (limit.isLimit (F ⋙ J.diagramFunctor D (unop X)))).hom.app
        k ≫
      colimit.ι (limit (F ⋙ J.diagramFunctor D (unop X))) k) ≫
    (colimitLimitIso (F ⋙ J.diagramFunctor D (unop X))).hom ≫
      limit.π (colimit (F ⋙ J.diagramFunctor D (unop X)).flip) k✝ ≫
        (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D (unop X)).flip k✝).hom