-- 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),
    𝟙 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

Tactic:
rintro ⟨⟨⟨⟩⟩, ⟨W₁⟩, g₁⟩ ⟨⟨⟨⟩⟩, ⟨W₂⟩, g₂⟩ ⟨⟨⟨⟨⟩⟩⟩, i, hi⟩

Result:
case refine_2.mk.mk.unit.op.mk.mk.unit.op.mk.up.up.refl
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₁ : C
g₁ : (fromPUnit (op (G.obj U))).obj { as := PUnit.unit } ⟶ G.op.obj (op W₁)
W₂ : C
g₂ : (fromPUnit (op (G.obj U))).obj { as := PUnit.unit } ⟶ G.op.obj (op W₂)
i :
  { left := { as := PUnit.unit }, right := op W₁, hom := g₁ }.right ⟶
    { left := { as := PUnit.unit }, right := op W₂, hom := g₂ }.right
hi :
  (fromPUnit (op (G.obj U))).map { down := { down := ⋯ } } ≫
      { left := { as := PUnit.unit }, right := op W₂, hom := g₂ }.hom =
    { left := { as := PUnit.unit }, right := op W₁, hom := g₁ }.hom ≫ G.op.map i
⊢ 𝟙 X ≫
      ⋯.amalgamate ⟨G.imageSieve { left := { as := PUnit.unit }, right := op W₂, hom := g₂ }.hom.unop, ⋯⟩
        (fun I =>
          f ≫
            Y.val.map
              (l I.Y (unop { left := { as := PUnit.unit }, right := op W₂, hom := g₂ }.2) U I.f
                  { left := { as := PUnit.unit }, right := op W₂, hom := g₂ }.hom.unop ⋯).op)
        ⋯ =
    ⋯.amalgamate ⟨G.imageSieve { left := { as := PUnit.unit }, right := op W₁, hom := g₁ }.hom.unop, ⋯⟩
        (fun I =>
          f ≫
            Y.val.map
              (l I.Y (unop { left := { as := PUnit.unit }, right := op W₁, hom := g₁ }.2) U I.f
                  { left := { as := PUnit.unit }, right := op W₁, hom := g₁ }.hom.unop ⋯).op)
        ⋯ ≫
      Y.val.map { left := { down := { down := ⋯ } }, right := i, w := hi }.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)
this : ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z), (G.imageSieve g).arrows f → ∃ l, G.map l = G.map f ≫ g
⊢ ∃ a, (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) a = f

Tactic:
choose l hl using 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
⊢ ∃ a, (yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X) a = f

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
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), ⋯⟩
⊢ G.map (l I.Y W₂ U I.f (G.map i ≫ g) ⋯) = G.map (I.f ≫ i) ≫ g

Tactic:
simp [hl]

Result:
no goals

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 =
    ⋯.amalgamate ⟨G.imageSieve g, ⋯⟩ (fun I => f ≫ Y.val.map (l I.Y W₁ U I.f g ⋯).op) ⋯ ≫ Y.val.map (I.f ≫ i).op

Tactic:
refine Eq.trans ?_ (Y.2.amalgamate_map _ _ _ I').symm

Result:
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