-- Mathlib/CategoryTheory/Sites/Sheafification.lean
theorem toSheafify_sheafifyLift {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) :
    toSheafify J P ≫ sheafifyLift J η hQ = η

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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ (sheafificationAdjunction J D).unit.app P ≫
      ((presheafToSheaf J D).map η ≫ (sheafificationAdjunction J D).counit.app { val := Q, cond := hQ }).val =
    η

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

Result:
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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ (sheafificationAdjunction J D).unit.app P ≫
      (sheafToPresheaf J D).map ((presheafToSheaf J D).map η) ≫
        ((sheafificationAdjunction J D).counit.app { val := Q, cond := hQ }).val =
    η

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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ (sheafificationAdjunction J D).unit.app P ≫
      (sheafToPresheaf J D).map ((presheafToSheaf J D).map η) ≫
        ((sheafificationAdjunction J D).counit.app { val := Q, cond := hQ }).val =
    η

Tactic:
simp only [Adjunction.unit_naturality_assoc]

Result:
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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ η ≫
      (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj { val := Q, cond := hQ }) ≫
        ((sheafificationAdjunction J D).counit.app { val := Q, cond := hQ }).val =
    η

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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ toSheafify J P ≫ sheafifyLift J η hQ = η

Tactic:
rw [toSheafify, sheafifyLift, Adjunction.homEquiv_counit]

Result:
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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ (sheafificationAdjunction J D).unit.app P ≫
      ((presheafToSheaf J D).map η ≫ (sheafificationAdjunction J D).counit.app { val := Q, cond := hQ }).val =
    η

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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ η ≫ 𝟙 ((sheafToPresheaf J D).obj { val := Q, cond := hQ }) = η

Tactic:
simp

Result:
no goals

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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ η ≫
      (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj { val := Q, cond := hQ }) ≫
        ((sheafificationAdjunction J D).counit.app { val := Q, cond := hQ }).val =
    η

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

Result:
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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ η ≫
      (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj { val := Q, cond := hQ }) ≫
        (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { val := Q, cond := hQ }) =
    η

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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ η ≫
      (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj { val := Q, cond := hQ }) ≫
        (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { val := Q, cond := hQ }) =
    η

Tactic:
rw [sheafificationAdjunction J D |>.right_triangle_components (Y := ⟨Q, hQ⟩)]

Result:
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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ η ≫ 𝟙 ((sheafToPresheaf J D).obj { val := Q, cond := hQ }) = η