-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem plusMap_toPlus : J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P)

Proof state:
case w.h.e_a.e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
⊢ (Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P) ≫ (J.diagram P I.Y).map ee.op =
    Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
      ((J.diagram P (unop X)).obj S) (fun I_1 => Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1)) ⋯

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun II => ?_)

Result:
case w.h.e_a.e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
II : (unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).shape.L
⊢ ((Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P) ≫ (J.diagram P I.Y).map ee.op) ≫
      Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II =
    Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
        ((J.diagram P (unop X)).obj S) (fun I_1 => Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1)) ⋯ ≫
      Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II

Proof state:
case w.h.e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
⊢ (J.diagramNatTrans { app := fun X => ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }
          (unop X)).app
      S =
    (colimit.ι (J.diagram P (unop X)) S ≫ ⊤.toMultiequalizer (J.plusObj P)) ≫
      (J.diagram (J.plusObj P) (unop X)).map e.op

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun I => ?_)

Result:
case w.h.e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
⊢ (J.diagramNatTrans { app := fun X => ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }
            (unop X)).app
        S ≫
      Multiequalizer.ι ((unop S).index (J.plusObj P)) I =
    ((colimit.ι (J.diagram P (unop X)) S ≫ ⊤.toMultiequalizer (J.plusObj P)) ≫
        (J.diagram (J.plusObj P) (unop X)).map e.op) ≫
      Multiequalizer.ι ((unop S).index (J.plusObj P)) I

Proof state:
case w.h.e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
⊢ Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P I.Y) (op ⊤) =
    colimit.ι (J.diagram P (unop X)) S ≫ (J.plusObj P).map (Cover.Arrow.map I e.op.unop).f.op

Tactic:
erw [← colimit.w _ ee.op, ι_colimMap_assoc, colimit.ι_pre, diagramPullback_app,
  ← Category.assoc, ← Category.assoc]

Result:
case w.h.e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
⊢ ((Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P) ≫ (J.diagram P I.Y).map ee.op) ≫
      colimit.ι (J.diagram P I.Y) (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S))) =
    Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
        ((J.diagram P (unop X)).obj S) (fun I_1 => Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1)) ⋯ ≫
      colimit.ι (J.diagram P (unop (op (Cover.Arrow.map I e.op.unop).Y)))
        ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)

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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
⊢ (J.diagramNatTrans { app := fun X => ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }
            (unop X)).app
        S ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) S =
    ((colimit.ι (J.diagram P (unop X)) S ≫ ⊤.toMultiequalizer (J.plusObj P)) ≫
        (J.diagram (J.plusObj P) (unop X)).map e.op) ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) (op (unop S))

Tactic:
congr 1

Result:
case w.h.e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
⊢ (J.diagramNatTrans { app := fun X => ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }
          (unop X)).app
      S =
    (colimit.ι (J.diagram P (unop X)) S ≫ ⊤.toMultiequalizer (J.plusObj P)) ≫
      (J.diagram (J.plusObj P) (unop X)).map e.op

Proof state:
case w.h.e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
⊢ Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P I.Y) (op ⊤) =
    colimit.ι (J.diagram P (unop X)) S ≫ (J.plusObj P).map (Cover.Arrow.map I e.op.unop).f.op

Tactic:
let ee : (J.pullback (I.map e).f).obj S.unop ⟶ ⊤ := homOfLE (OrderTop.le_top _)

Result:
case w.h.e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
⊢ Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P I.Y) (op ⊤) =
    colimit.ι (J.diagram P (unop X)) S ≫ (J.plusObj P).map (Cover.Arrow.map I e.op.unop).f.op