C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
⊢ IsIso (toPlus J P)
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (toPlus J P)
rw [Presheaf.isSheaf_iff_multiequalizer] at hP
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
this : ∀ (X : Cᵒᵖ), IsIso ((toPlus J P).app X)
⊢ IsIso (toPlus J P)

case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
⊢ ∀ (X : Cᵒᵖ), IsIso ((toPlus J P).app X)
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
⊢ IsIso (toPlus J P)
suffices : ∀ X, IsIso ((J.toPlus P).app X)
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
⊢ IsIso ((toPlus J P).app X)
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
⊢ ∀ (X : Cᵒᵖ), IsIso ((toPlus J P).app X)
intro X
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
⊢ IsIso ((toPlus J P).app X)
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
⊢ IsIso ((toPlus J P).app X)
dsimp
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
this : IsIso (colimit.ι (diagram J P X.unop) ⊤.op)
⊢ IsIso ((toPlus J P).app X)

case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
⊢ IsIso (colimit.ι (diagram J P X.unop) ⊤.op)
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
⊢ IsIso ((toPlus J P).app X)
suffices : IsIso (colimit.ι (J.diagram P X.unop) (op ⊤))
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
this : ∀ (S T : (Cover J X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((diagram J P X.unop).map f)
⊢ IsIso (colimit.ι (diagram J P X.unop) ⊤.op)

case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
⊢ ∀ (S T : (Cover J X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((diagram J P X.unop).map f)
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
⊢ IsIso (colimit.ι (diagram J P X.unop) ⊤.op)
suffices : ∀ (S T : (J.Cover X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((J.diagram P X.unop).map f)
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
⊢ IsIso ((diagram J P X.unop).map e)
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
⊢ ∀ (S T : (Cover J X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((diagram J P X.unop).map f)
intro S T e
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
this : Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e = Cover.toMultiequalizer T.unop P
⊢ IsIso ((diagram J P X.unop).map e)
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
⊢ IsIso ((diagram J P X.unop).map e)
have : S.unop.toMultiequalizer P ≫ (J.diagram P X.unop).map e = T.unop.toMultiequalizer P :=
  Multiequalizer.hom_ext _ _ _ (fun II => by dsimp ; simp)
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
this✝ : Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e = Cover.toMultiequalizer T.unop P
this : (diagram J P X.unop).map e = inv (Cover.toMultiequalizer S.unop P) ≫ Cover.toMultiequalizer T.unop P
⊢ IsIso ((diagram J P X.unop).map e)
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
this : Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e = Cover.toMultiequalizer T.unop P
⊢ IsIso ((diagram J P X.unop).map e)
have :
  (J.diagram P X.unop).map e = inv (S.unop.toMultiequalizer P) ≫ T.unop.toMultiequalizer P := by
  simp [← this]
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
this✝ : Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e = Cover.toMultiequalizer T.unop P
this : (diagram J P X.unop).map e = inv (Cover.toMultiequalizer S.unop P) ≫ Cover.toMultiequalizer T.unop P
⊢ IsIso (inv (Cover.toMultiequalizer S.unop P) ≫ Cover.toMultiequalizer T.unop P)
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
this✝ : Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e = Cover.toMultiequalizer T.unop P
this : (diagram J P X.unop).map e = inv (Cover.toMultiequalizer S.unop P) ≫ Cover.toMultiequalizer T.unop P
⊢ IsIso ((diagram J P X.unop).map e)
rw [this]
no goals
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
this✝ : Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e = Cover.toMultiequalizer T.unop P
this : (diagram J P X.unop).map e = inv (Cover.toMultiequalizer S.unop P) ≫ Cover.toMultiequalizer T.unop P
⊢ IsIso (inv (Cover.toMultiequalizer S.unop P) ≫ Cover.toMultiequalizer T.unop P)
infer_instance
no goals
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
this : ∀ (X : Cᵒᵖ), IsIso ((toPlus J P).app X)
⊢ IsIso (toPlus J P)
apply NatIso.isIso_of_isIso_app
no goals
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
this : IsIso (colimit.ι (diagram J P X.unop) ⊤.op)
⊢ IsIso ((toPlus J P).app X)
apply IsIso.comp_isIso
no goals
case this
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
this : ∀ (S T : (Cover J X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((diagram J P X.unop).map f)
⊢ IsIso (colimit.ι (diagram J P X.unop) ⊤.op)
apply isIso_ι_of_isInitial (initialOpOfTerminal isTerminalTop)
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
II : (Cover.index T.unop P).L
⊢ (Cover.toMultiequalizer S.unop P ≫
        Multiequalizer.lift (Cover.index T.unop P) (multiequalizer (Cover.index S.unop P))
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.map I e.unop))
          (_ :
            ∀ (I : (Cover.index T.unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.map I e.unop)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.map I e.unop) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.map I e.unop)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.map I e.unop))) ≫
      Multiequalizer.ι (Cover.index T.unop P) II =
    Cover.toMultiequalizer T.unop P ≫ Multiequalizer.ι (Cover.index T.unop P) II
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
II : (Cover.index T.unop P).L
⊢ (Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e) ≫ Multiequalizer.ι (Cover.index T.unop P) II =
    Cover.toMultiequalizer T.unop P ≫ Multiequalizer.ι (Cover.index T.unop P) II
dsimp
no goals
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
II : (Cover.index T.unop P).L
⊢ (Cover.toMultiequalizer S.unop P ≫
        Multiequalizer.lift (Cover.index T.unop P) (multiequalizer (Cover.index S.unop P))
          (fun I => Multiequalizer.ι (Cover.index S.unop P) (Cover.Arrow.map I e.unop))
          (_ :
            ∀ (I : (Cover.index T.unop P).R),
              Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.fstTo (Cover.index S.unop P) (Cover.Relation.map I e.unop)) ≫
                  MulticospanIndex.fst (Cover.index S.unop P) (Cover.Relation.map I e.unop) =
                Multiequalizer.ι (Cover.index S.unop P)
                    (MulticospanIndex.sndTo (Cover.index S.unop P) (Cover.Relation.map I e.unop)) ≫
                  MulticospanIndex.snd (Cover.index S.unop P) (Cover.Relation.map I e.unop))) ≫
      Multiequalizer.ι (Cover.index T.unop P) II =
    Cover.toMultiequalizer T.unop P ≫ Multiequalizer.ι (Cover.index T.unop P) II
simp
no goals
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
hP : ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S P)
X : Cᵒᵖ
S T : (Cover J X.unop)ᵒᵖ
e : S ⟶ T
this : Cover.toMultiequalizer S.unop P ≫ (diagram J P X.unop).map e = Cover.toMultiequalizer T.unop P
⊢ (diagram J P X.unop).map e = inv (Cover.toMultiequalizer S.unop P) ≫ Cover.toMultiequalizer T.unop P
simp [← this]