-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem isIso_toPlus_of_isSheaf (hP : Presheaf.IsSheaf J P) : IsIso (J.toPlus P)

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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
⊢ ∀ (X : Cᵒᵖ), IsIso ((J.toPlus P).app X)

Tactic:
intro X

Result:
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
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
X : Cᵒᵖ
⊢ IsIso ((J.toPlus P).app 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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (J.toPlus P)

Tactic:
rw [Presheaf.isSheaf_iff_multiequalizer] at hP

Result:
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
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
⊢ IsIso (J.toPlus P)

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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
X : Cᵒᵖ
S T : (J.Cover (unop X))ᵒᵖ
e : S ⟶ T
II : (unop T).shape.L
⊢ ((unop S).toMultiequalizer P ≫ (J.diagram P (unop X)).map e) ≫ Multiequalizer.ι ((unop T).index P) II =
    (unop T).toMultiequalizer P ≫ Multiequalizer.ι ((unop T).index P) II

Tactic:
dsimp

Result:
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
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
X : Cᵒᵖ
S T : (J.Cover (unop X))ᵒᵖ
e : S ⟶ T
II : (unop T).shape.L
⊢ ((unop S).toMultiequalizer P ≫
        Multiequalizer.lift ((unop T).index P) (multiequalizer ((unop S).index P))
          (fun I => Multiequalizer.ι ((unop S).index P) (I.map e.unop)) ⋯) ≫
      Multiequalizer.ι ((unop T).index P) II =
    (unop T).toMultiequalizer P ≫ Multiequalizer.ι ((unop T).index P) II

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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
X : Cᵒᵖ
⊢ ∀ (S T : (J.Cover (unop X))ᵒᵖ) (f : S ⟶ T), IsIso ((J.diagram P (unop X)).map f)

Tactic:
intro S T e

Result:
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
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
X : Cᵒᵖ
S T : (J.Cover (unop X))ᵒᵖ
e : S ⟶ T
⊢ IsIso ((J.diagram P (unop X)).map e)

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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
X : Cᵒᵖ
S T : (J.Cover (unop X))ᵒᵖ
e : S ⟶ T
this : (unop S).toMultiequalizer P ≫ (J.diagram P (unop X)).map e = (unop T).toMultiequalizer P
⊢ (J.diagram P (unop X)).map e = inv ((unop S).toMultiequalizer P) ≫ (unop T).toMultiequalizer P

Tactic:
simp [← this]

Result:
no goals