-- 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
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 : (fromPUnit (op (G.obj U))).obj { as := PUnit.unit } ⟶ G.op.obj (op W)
⊢ 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 } =
    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 }

Tactic:
obtain ⟨g, rfl⟩ : ∃ g' : G.obj W ⟶ G.obj U, g = g'.op := ⟨g.unop, rfl⟩

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
⊢ 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 }

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
⊢ Function.Bijective ((yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X))

Tactic:
constructor

Result:
case left
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
⊢ Function.Injective ((yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X))

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
⊢ Function.Surjective ((yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X))

Proof state:
case refine_2.mk.mk.unit.op.mk.mk.unit.op.mk.up.up.refl.refl.intro.intro.h
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
W₁ W₂ : C
g : G.obj W₁ ⟶ G.obj U
i : W₂ ⟶ W₁
hi : 𝟙 (op (G.obj U)) ≫ g.op ≫ (G.map i.op.unop).op = g.op ≫ (G.map i.op.unop).op
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (G.map i ≫ g), ⋯⟩
I' : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g, ⋯⟩ := { Y := I.Y, f := I.f ≫ i, hf := ⋯ }
⊢ f ≫ Y.val.map (l I.Y W₂ U I.f (G.map i ≫ g) ⋯).op = f ≫ Y.val.map (l I'.Y W₁ U I'.f g ⋯).op

Tactic:
apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (l _ _ _ _ _ I.hf)
  (l _ _ _ _ _ I'.hf) (by simp [I', hl]))).isSeparatedFor.ext
    fun V iUV (hiUV : _ = _) ↦ ?_

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
W₁ W₂ : C
g : G.obj W₁ ⟶ G.obj U
i : W₂ ⟶ W₁
hi : 𝟙 (op (G.obj U)) ≫ g.op ≫ (G.map i.op.unop).op = g.op ≫ (G.map i.op.unop).op
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (G.map i ≫ g), ⋯⟩
I' : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g, ⋯⟩ := { Y := I.Y, f := I.f ≫ i, hf := ⋯ }
V : C
iUV : V ⟶ I.Y
hiUV : iUV ≫ l I.Y W₂ U I.f (G.map i ≫ g) ⋯ = iUV ≫ l I.Y W₁ U I'.f g ⋯
⊢ (Y.val ⋙ coyoneda.obj (op X)).map iUV.op (f ≫ Y.val.map (l I.Y W₂ U I.f (G.map i ≫ g) ⋯).op) =
    (Y.val ⋙ coyoneda.obj (op X)).map iUV.op (f ≫ Y.val.map (l I'.Y W₁ U I'.f g ⋯).op)