Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, 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.obj).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.obj) :=
  { pt := X,
    π :=
      {
        app := fun g ↦
          ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op) ⋯,
        naturality := ⋯ } }
this :
  (G.op.isPointwiseRightKanExtensionRanCounit Y.obj (op (G.obj U))).lift c ≫ (G.op.ranCounit.app Y.obj).app (op U) =
    c.π.app (StructuredArrow.mk (𝟙 (op (G.obj U))))
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (𝟙 (G.obj U)), ⋯⟩
⊢ ⋯.amalgamate ⟨G.imageSieve (StructuredArrow.mk (𝟙 (op (G.obj U)))).hom.unop, ⋯⟩
        (fun I ↦
          f ≫
            Y.obj.map
              (l I.Y (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2) U I.f
                  (StructuredArrow.mk (𝟙 (op (G.obj U)))).hom.unop ⋯).op)
        ⋯ ≫
      Y.obj.map I.f.op =
    f ≫ Y.obj.map I.f.op

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

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, 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.obj).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.obj) :=
  { pt := X,
    π :=
      {
        app := fun g ↦
          ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op) ⋯,
        naturality := ⋯ } }
this :
  (G.op.isPointwiseRightKanExtensionRanCounit Y.obj (op (G.obj U))).lift c ≫ (G.op.ranCounit.app Y.obj).app (op U) =
    c.π.app (StructuredArrow.mk (𝟙 (op (G.obj U))))
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (𝟙 (G.obj U)), ⋯⟩
V : C
iUV : V ⟶ I.Y
hiUV : iUV ≫ l I.Y U U I.f (𝟙 (G.obj U)) ⋯ = iUV ≫ I.f
⊢ (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      (⋯.amalgamate ⟨G.imageSieve (StructuredArrow.mk (𝟙 (op (G.obj U)))).hom.unop, ⋯⟩
          (fun I ↦
            f ≫
              Y.obj.map
                (l I.Y (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2) U I.f
                    (StructuredArrow.mk (𝟙 (op (G.obj U)))).hom.unop ⋯).op)
          ⋯ ≫
        Y.obj.map I.f.op) =
    (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op)) (f ≫ Y.obj.map I.f.op)