Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e_a.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', 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

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

Goal state after:
case e'_2
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', 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 ⟶ ⊤ := ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := ⋯
II : (unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).shape.L
e_1✝ :
  ((J.diagram P (unop X)).obj 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
        { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } })
⊢ ((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.ι ((unop S).index P)
        ((unop S).shape.fst
          { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } }) ≫
      ((unop S).index P).fst
        { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } }

case e'_3
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', 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 ⟶ ⊤ := ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := ⋯
II : (unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).shape.L
e_1✝ :
  ((J.diagram P (unop X)).obj 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
        { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } })
⊢ 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 =
    Multiequalizer.ι ((unop S).index P)
        ((unop S).shape.snd
          { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } }) ≫
      ((unop S).index P).snd
        { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } }