-- 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 left.mk.mk.unit.op.intro.intro
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₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.val).obj (op U))).obj (op X)
e :
  (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) f₁ =
    (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) f₂
W : C
g : G.obj W ⟶ G.obj U
V : C
iVW : V ⟶ W
iVU : V ⟶ U
e' : G.map iVU = G.map iVW ≫ g
this :
  (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) f₁ ≫ Y.val.map iVU.op =
    (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) f₂ ≫ Y.val.map iVU.op
⊢ (f₁ ≫ (G.op.ran.obj Y.val).map g.op ≫ (G.op.ranCounit.app Y.val).app (op W)) ≫ Y.val.map iVW.op =
    (f₂ ≫ (G.op.ran.obj Y.val).map g.op ≫ (G.op.ranCounit.app Y.val).app (op W)) ≫ Y.val.map iVW.op

Tactic:
simp only [comp_obj, yoneda_map_app, Category.assoc, coyoneda_obj_obj, comp_map,
  coyoneda_obj_map, ← NatTrans.naturality, op_obj, op_map, Quiver.Hom.unop_op, ← map_comp_assoc,
  ← op_comp, ← e'] at this ⊢

Result:
case left.mk.mk.unit.op.intro.intro
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₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.val).obj (op U))).obj (op X)
e :
  (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) f₁ =
    (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) f₂
W : C
g : G.obj W ⟶ G.obj U
V : C
iVW : V ⟶ W
iVU : V ⟶ U
e' : G.map iVU = G.map iVW ≫ g
this :
  f₁ ≫ (G.op.ranCounit.app Y.val).app (op U) ≫ Y.val.map iVU.op =
    f₂ ≫ (G.op.ranCounit.app Y.val).app (op U) ≫ Y.val.map iVU.op
⊢ f₁ ≫ (G.op.ran.obj Y.val).map (G.map iVU).op ≫ (G.op.ranCounit.app Y.val).app (op V) =
    f₂ ≫ (G.op.ran.obj Y.val).map (G.map iVU).op ≫ (G.op.ranCounit.app Y.val).app (op V)

Proof state:
case left.mk.mk.unit.op.intro
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₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.val).obj (op U))).obj (op X)
e :
  (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) f₁ =
    (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) f₂
W : C
g : G.obj W ⟶ G.obj U
⊢ f₁ ≫
      ((RightExtension.mk (G.op.ran.obj Y.val) (G.op.ranCounit.app Y.val)).coneAt (op (G.obj U))).π.app
        { left := { as := PUnit.unit }, right := op W, hom := g.op } =
    f₂ ≫
      ((RightExtension.mk (G.op.ran.obj Y.val) (G.op.ranCounit.app Y.val)).coneAt (op (G.obj U))).π.app
        { left := { as := PUnit.unit }, right := op W, hom := g.op }

Tactic:
apply (Y.2 X _ (IsDenseSubsite.imageSieve_mem J K G g)).isSeparatedFor.ext

Result:
case left.mk.mk.unit.op.intro
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₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.val).obj (op U))).obj (op X)
e :
  (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) f₁ =
    (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) f₂
W : C
g : G.obj W ⟶ G.obj U
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ W⦄,
    (G.imageSieve g).arrows f →
      (Y.val ⋙ coyoneda.obj (op X)).map f.op
          (f₁ ≫
            ((RightExtension.mk (G.op.ran.obj Y.val) (G.op.ranCounit.app Y.val)).coneAt (op (G.obj U))).π.app
              { left := { as := PUnit.unit }, right := op W, hom := g.op }) =
        (Y.val ⋙ coyoneda.obj (op X)).map f.op
          (f₂ ≫
            ((RightExtension.mk (G.op.ran.obj Y.val) (G.op.ranCounit.app Y.val)).coneAt (op (G.obj U))).π.app
              { left := { as := PUnit.unit }, right := op W, hom := g.op })

Proof state:
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
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
⊢ G.map (r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯) = G.map (r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯)

Tactic:
simp only [const_obj_obj, op_obj, map_comp, hl]

Result:
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
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
⊢ G.map r.g₁ ≫ G.map I₁.f ≫ g.hom.unop = G.map r.g₂ ≫ G.map I₂.f ≫ g.hom.unop