-- Mathlib/CategoryTheory/Sites/CoverLifting.lean
lemma sheafAdjunctionCocontinuous_unit_app_val (F : Sheaf K A) :
    ((G.sheafAdjunctionCocontinuous A J K).unit.app F).val =
      (G.op.ranAdjunction A).unit.app F.val

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app F.val ≫ 𝟙 (G.op.ran.obj (G.op ⋙ F.val)) ≫ 𝟙 (G.op.ran.obj (G.op ⋙ F.val)) =
    (G.op.ranAdjunction A).unit.app F.val

Tactic:
simp only [Category.comp_id]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app ((sheafToPresheaf K A).obj F) ≫
      G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm.hom.app F) ≫
        (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm.hom.app
          ((G.sheafPushforwardContinuous A J K).obj F) =
    (G.op.ranAdjunction A).unit.app F.val

Tactic:
dsimp

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app F.val ≫
      G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app F) ≫
        𝟙 ((G.sheafPushforwardCocontinuous A J K).obj ((G.sheafPushforwardContinuous A J K).obj F)).val =
    (G.op.ranAdjunction A).unit.app F.val

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app F.val ≫
      G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app F) ≫
        𝟙 ((G.sheafPushforwardCocontinuous A J K).obj ((G.sheafPushforwardContinuous A J K).obj F)).val =
    (G.op.ranAdjunction A).unit.app F.val

Tactic:
erw [Functor.map_id]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app F.val ≫
      𝟙 (G.op.ran.obj (G.op ⋙ F.val)) ≫
        𝟙 ((G.sheafPushforwardCocontinuous A J K).obj ((G.sheafPushforwardContinuous A J K).obj F)).val =
    (G.op.ranAdjunction A).unit.app F.val

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app F.val ≫
      𝟙 (G.op.ran.obj (G.op ⋙ F.val)) ≫
        𝟙 ((G.sheafPushforwardCocontinuous A J K).obj ((G.sheafPushforwardContinuous A J K).obj F)).val =
    (G.op.ranAdjunction A).unit.app F.val

Tactic:
change _ ≫ 𝟙 _ ≫ 𝟙 _ = _

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app F.val ≫ 𝟙 (G.op.ran.obj (G.op ⋙ F.val)) ≫ 𝟙 (G.op.ran.obj (G.op ⋙ F.val)) =
    (G.op.ranAdjunction A).unit.app F.val

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ ((G.sheafAdjunctionCocontinuous A J K).unit.app F).val = (G.op.ranAdjunction A).unit.app F.val

Tactic:
apply ((G.op.ranAdjunction A).map_restrictFullyFaithful_unit_app
  (fullyFaithfulSheafToPresheaf K A) (fullyFaithfulSheafToPresheaf J A)
  (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm
  (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm F).trans

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app ((sheafToPresheaf K A).obj F) ≫
      G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm.hom.app F) ≫
        (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm.hom.app
          ((G.sheafPushforwardContinuous A J K).obj F) =
    (G.op.ranAdjunction A).unit.app F.val