-- Mathlib/CategoryTheory/Sites/DenseSubsite/SheafEquiv.lean
lemma isIso_ranCounit_app_of_isDenseSubsite (Y : Sheaf J A) (U X) :
    IsIso ((yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X))

Proof state:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.val).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
⊢ ∀ ⦃X_1 Y_1 : StructuredArrow (op (G.obj U)) G.op⦄ (f_1 : X_1 ⟶ Y_1),
    ((const (StructuredArrow (op (G.obj U)) G.op)).obj X).map f_1 ≫
        (fun g =>
            ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I => f ≫ Y.val.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op)
              ⋯)
          Y_1 =
      (fun g =>
            ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I => f ≫ Y.val.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op)
              ⋯)
          X_1 ≫
        (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.val).map f_1

Tactic:
dsimp

Result:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.val).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
⊢ ∀ ⦃X_1 Y_1 : StructuredArrow (op (G.obj U)) G.op⦄ (f_1 : X_1 ⟶ Y_1),
    𝟙 X ≫
        ⋯.amalgamate ⟨G.imageSieve Y_1.hom.unop, ⋯⟩
          (fun I => f ≫ Y.val.map (l I.Y (unop Y_1.2) U I.f Y_1.hom.unop ⋯).op) ⋯ =
      ⋯.amalgamate ⟨G.imageSieve X_1.hom.unop, ⋯⟩ (fun I => f ≫ Y.val.map (l I.Y (unop X_1.2) U I.f X_1.hom.unop ⋯).op)
          ⋯ ≫
        Y.val.map f_1.right

Proof state:
case right
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.val).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
c : Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.val) :=
  { pt := X,
    π :=
      {
        app := fun g =>
          ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I => f ≫ Y.val.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op) ⋯,
        naturality := ⋯ } }
this :
  (G.op.isPointwiseRightKanExtensionRanCounit Y.val (op (G.obj U))).lift c ≫
      ((RightExtension.mk (G.op.ran.obj Y.val) (G.op.ranCounit.app Y.val)).coneAt (op (G.obj U))).π.app
        (StructuredArrow.mk (𝟙 (op (G.obj U)))) =
    c.π.app (StructuredArrow.mk (𝟙 (op (G.obj U))))
⊢ (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X)
      ((G.op.isPointwiseRightKanExtensionRanCounit Y.val (op (G.obj U))).lift c) =
    f

Tactic:
simp only [id_obj, comp_obj, StructuredArrow.proj_obj, StructuredArrow.mk_right,
  RightExtension.coneAt_pt, RightExtension.mk_left, RightExtension.coneAt_π_app,
  const_obj_obj, op_obj, StructuredArrow.mk_hom_eq_self, map_id, whiskeringLeft_obj_obj,
  RightExtension.mk_hom, Category.id_comp, StructuredArrow.mk_left, unop_id] at this

Result:
case right
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.val).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
c : Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.val) :=
  { pt := X,
    π :=
      {
        app := fun g =>
          ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I => f ≫ Y.val.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op) ⋯,
        naturality := ⋯ } }
this :
  (G.op.isPointwiseRightKanExtensionRanCounit Y.val (op (G.obj U))).lift c ≫ (G.op.ranCounit.app Y.val).app (op U) =
    c.π.app (StructuredArrow.mk (𝟙 (op (G.obj U))))
⊢ (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X)
      ((G.op.isPointwiseRightKanExtensionRanCounit Y.val (op (G.obj U))).lift c) =
    f