-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (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
h :
  (Functor.obj (J.diagram P (unop X)) S ⟶
        ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II) =
      (multiequalizer ((unop S).index P) ⟶
        ((unop S).index P).right
          (Cover.Relation.mk (snd := Cover.Arrow.base II) { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ })) →
    Eq (α :=
      Functor.obj (J.diagram P (unop X)) S ⟶
        ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II)
      (CategoryStruct.comp (Y :=
        multiequalizer ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P))
        (CategoryStruct.comp (Y :=
          multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
          (Multiequalizer.ι ((unop S).index P) I ≫ Cover.toMultiequalizer ⊤ P) (Functor.map (J.diagram P I.Y) ee.op))
        (Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II))
      (Multiequalizer.ι ((unop S).index P)
          ((unop S).shape.fst
            (Cover.Relation.mk (snd := Cover.Arrow.base II) { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ })) ≫
        ((unop S).index P).fst
          (Cover.Relation.mk (snd := Cover.Arrow.base II)
            { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ : Cover.Arrow.Relation I (Cover.Arrow.base II) }))
h₁ :
  (Functor.obj (J.diagram P (unop X)) S ⟶
        ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II) =
      (multiequalizer ((unop S).index P) ⟶
        ((unop S).index P).right
          (Cover.Relation.mk (snd := Cover.Arrow.base II) { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ })) →
    Eq (α :=
      Functor.obj (J.diagram P (unop X)) S ⟶
        ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II)
      (CategoryStruct.comp (Y :=
        multiequalizer ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P))
        (Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
          (Functor.obj (J.diagram P (unop X)) S)
          (fun (I_1 : (unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).shape.L) ↦
            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))
      (Multiequalizer.ι ((unop S).index P)
          ((unop S).shape.snd
            (Cover.Relation.mk (snd := Cover.Arrow.base II) { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ })) ≫
        ((unop S).index P).snd
          (Cover.Relation.mk (snd := Cover.Arrow.base II)
            { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ : Cover.Arrow.Relation I (Cover.Arrow.base II) }))
⊢ Eq (α :=
    Functor.obj (J.diagram P (unop X)) S ⟶
      ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II)
    (CategoryStruct.comp (Y := multiequalizer ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.ι ((unop S).index P) I ≫ Cover.toMultiequalizer ⊤ P) (Functor.map (J.diagram P I.Y) ee.op))
      (Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II))
    (CategoryStruct.comp (Y := multiequalizer ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P))
      (Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
        (Functor.obj (J.diagram P (unop X)) S)
        (fun (I_1 : (unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).shape.L) ↦
          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))

Tactic:
convert!
    Multiequalizer.condition (S.unop.index P)
      { fst := I, snd := II.base, r.Z := II.Y, r.g₁ := II.f, r.g₂ := 𝟙 II.Y } using 1

Premises used: CategoryTheory.Limits.Multiequalizer.condition, CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk, CategoryTheory.CategoryStruct.id, CategoryTheory.GrothendieckTopology.Cover.index, CategoryTheory.GrothendieckTopology.Cover.Relation.mk, CategoryTheory.GrothendieckTopology.Cover.Arrow.f, CategoryTheory.GrothendieckTopology.Cover.Arrow.Y, Opposite.unop