-- Mathlib/CategoryTheory/Sites/Sheafification.lean
theorem isIso_toSheafify {P : Cᵒᵖ ⥤ D} (hP : Presheaf.IsSheaf J P) : IsIso (toSheafify J P)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (toSheafify J P)

Tactic:
refine ⟨(sheafificationAdjunction J D |>.counit.app ⟨P, hP⟩).val, ?_, ?_⟩

Result:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ toSheafify J P ≫ ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }).val = 𝟙 P

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }).val ≫ toSheafify J P = 𝟙 (sheafify J P)

Proof state:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ toSheafify J P ≫ ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }).val = 𝟙 P

Tactic:
change _ = (𝟙 (sheafToPresheaf J D ⋙ 𝟭 (Cᵒᵖ ⥤ D)) :).app ⟨P, hP⟩

Result:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ toSheafify J P ≫ ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }).val =
    (𝟙 (sheafToPresheaf J D ⋙ 𝟭 (Cᵒᵖ ⥤ D))).app { val := P, cond := hP }

Proof state:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }) ≫
      (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj { val := P, cond := hP }) =
    𝟙 (sheafify J P)

Tactic:
rw [← (sheafificationAdjunction J D).inv_counit_map (X := ⟨P, hP⟩)]

Result:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }) ≫
      inv ((sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { val := P, cond := hP })) =
    𝟙 (sheafify J P)

Proof state:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ toSheafify J P ≫ ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }).val =
    (whiskerLeft (sheafToPresheaf J D) (sheafificationAdjunction J D).unit ≫
          whiskerRight (sheafificationAdjunction J D).counit (sheafToPresheaf J D)).app
      { val := P, cond := hP }

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ toSheafify J P ≫ ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }).val =
    (𝟙 (sheafToPresheaf J D ⋙ 𝟭 (Cᵒᵖ ⥤ D))).app { val := P, cond := hP }

Tactic:
rw [← sheafificationAdjunction J D |>.right_triangle]

Result:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ toSheafify J P ≫ ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }).val =
    (whiskerLeft (sheafToPresheaf J D) (sheafificationAdjunction J D).unit ≫
          whiskerRight (sheafificationAdjunction J D).counit (sheafToPresheaf J D)).app
      { val := P, cond := hP }

Proof state:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }) ≫
      inv ((sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { val := P, cond := hP })) =
    𝟙 (sheafify J P)

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }) ≫ toSheafify J P =
    𝟙 (sheafify J P)

Tactic:
change _ ≫ (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj ⟨P, hP⟩) = _

Result:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }) ≫
      (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj { val := P, cond := hP }) =
    𝟙 (sheafify J P)

Proof state:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }).val ≫ toSheafify J P = 𝟙 (sheafify J P)

Tactic:
change (sheafToPresheaf _ _).map _ ≫ _ = _

Result:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { val := P, cond := hP }) ≫ toSheafify J P =
    𝟙 (sheafify J P)