-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem plusMap_id (P : Cᵒᵖ ⥤ D) : J.plusMap (𝟙 P) = 𝟙 _

Proof state:
case w.h.w
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j✝ : (J.Cover (unop x✝))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop x✝)) j✝ ≫ colimMap (𝟙 (J.diagram P (unop x✝))) =
    colimit.ι (J.diagram P (unop x✝)) j✝ ≫ 𝟙 (colimit (J.diagram P (unop x✝)))

Tactic:
simp

Result:
no goals

Proof state:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ colimMap (𝟙 (J.diagram P (unop x✝))) =
    𝟙
      ({ obj := fun X => colimit (J.diagram P (unop X)),
            map := fun {X Y} f =>
              colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op,
            map_id := ⋯, map_comp := ⋯ }.obj
        x✝)

Tactic:
ext

Result:
case w.h.w
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j✝ : (J.Cover (unop x✝))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop x✝)) j✝ ≫ colimMap (𝟙 (J.diagram P (unop x✝))) =
    colimit.ι (J.diagram P (unop x✝)) j✝ ≫
      𝟙
        ({ obj := fun X => colimit (J.diagram P (unop X)),
              map := fun {X Y} f =>
                colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op,
              map_id := ⋯, map_comp := ⋯ }.obj
          x✝)

Proof state:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ colimMap (J.diagramNatTrans (𝟙 P) (unop x✝)) =
    (𝟙
          { obj := fun X => colimit (J.diagram P (unop X)),
            map := fun {X Y} f =>
              colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op,
            map_id := ⋯, map_comp := ⋯ }).app
      x✝

Tactic:
rw [J.diagramNatTrans_id, NatTrans.id_app]

Result:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ colimMap (𝟙 (J.diagram P (unop x✝))) =
    𝟙
      ({ obj := fun X => colimit (J.diagram P (unop X)),
            map := fun {X Y} f =>
              colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op,
            map_id := ⋯, map_comp := ⋯ }.obj
        x✝)

Proof state:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ (J.plusMap (𝟙 P)).app x✝ = (𝟙 (J.plusObj P)).app x✝

Tactic:
dsimp only [plusMap, plusObj]

Result:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ colimMap (J.diagramNatTrans (𝟙 P) (unop x✝)) =
    (𝟙
          { obj := fun X => colimit (J.diagram P (unop X)),
            map := fun {X Y} f =>
              colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op,
            map_id := ⋯, map_comp := ⋯ }).app
      x✝

Proof state:
case w.h.w
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j✝ : (J.Cover (unop x✝))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop x✝)) j✝ ≫ colimMap (𝟙 (J.diagram P (unop x✝))) =
    colimit.ι (J.diagram P (unop x✝)) j✝ ≫
      𝟙
        ({ obj := fun X => colimit (J.diagram P (unop X)),
              map := fun {X Y} f =>
                colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op,
              map_id := ⋯, map_comp := ⋯ }.obj
          x✝)

Tactic:
dsimp

Result:
case w.h.w
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j✝ : (J.Cover (unop x✝))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop x✝)) j✝ ≫ colimMap (𝟙 (J.diagram P (unop x✝))) =
    colimit.ι (J.diagram P (unop x✝)) j✝ ≫ 𝟙 (colimit (J.diagram P (unop x✝)))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
⊢ J.plusMap (𝟙 P) = 𝟙 (J.plusObj P)

Tactic:
ext : 2

Result:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ (J.plusMap (𝟙 P)).app x✝ = (𝟙 (J.plusObj P)).app x✝