awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
f : obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U))) (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (hf : (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₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi :
  StructuredArrow.hom (StructuredArrow.mk (op g₁)) ≫ G.op.map (op i) =
    StructuredArrow.hom (StructuredArrow.mk (op (G.map i ≫ g₁)))
I :
  GrothendieckTopology.Cover.Arrow
    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₂) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₂)
      (G.imageSieve (G.map i ≫ g₁)) ⋯)
I' : GrothendieckTopology.Cover.Arrow
  (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁) (G.imageSieve g₁) ⋯) :=
  { Y := I.Y, f := I.f ≫ i, hf := ⋯ }
⊢ f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op =
    ⋯.amalgamate
        (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁) (G.imageSieve g₁) ⋯)
        (fun
            (I :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁)
                  (G.imageSieve g₁) ⋯)) ↦
          f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₁ U I.f g₁ ⋯).op)
        ⋯ ≫
      Y.obj (P := Presheaf.IsSheaf J).map (op i ≫ I.f.op)

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

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map, CategoryTheory.ObjectProperty.FullSubcategory.property, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
f : obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U))) (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (hf : (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₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi :
  StructuredArrow.hom (StructuredArrow.mk (op g₁)) ≫ G.op.map (op i) =
    StructuredArrow.hom (StructuredArrow.mk (op (G.map i ≫ g₁)))
I :
  GrothendieckTopology.Cover.Arrow
    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₂) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₂)
      (G.imageSieve (G.map i ≫ g₁)) ⋯)
I' : GrothendieckTopology.Cover.Arrow
  (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁) (G.imageSieve g₁) ⋯) :=
  { Y := I.Y, f := I.f ≫ i, hf := ⋯ }
refine_2 :
  f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op =
    f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I'.Y W₁ U I'.f g₁ ⋯).op
⊢ f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op =
    ⋯.amalgamate
        (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁) (G.imageSieve g₁) ⋯)
        (fun
            (I :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁)
                  (G.imageSieve g₁) ⋯)) ↦
          f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₁ U I.f g₁ ⋯).op)
        ⋯ ≫
      Y.obj (P := Presheaf.IsSheaf J).map (op i ≫ I.f.op)

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

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map, CategoryTheory.ObjectProperty.FullSubcategory.property, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
f : obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U))) (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (hf : (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₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi :
  StructuredArrow.hom (StructuredArrow.mk (op g₁)) ≫ G.op.map (op i) =
    StructuredArrow.hom (StructuredArrow.mk (op (G.map i ≫ g₁)))
I :
  GrothendieckTopology.Cover.Arrow
    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₂) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₂)
      (G.imageSieve (G.map i ≫ g₁)) ⋯)
I' : GrothendieckTopology.Cover.Arrow
  (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁) (G.imageSieve g₁) ⋯) :=
  { Y := I.Y, f := I.f ≫ i, hf := ⋯ }
⊢ G.map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯) = G.map (l I.Y W₁ U I'.f g₁ ⋯)

Tactic:
simp [I', hl]
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
f : obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U))) (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (hf : (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₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi :
  StructuredArrow.hom (StructuredArrow.mk (op g₁)) ≫ G.op.map (op i) =
    StructuredArrow.hom (StructuredArrow.mk (op (G.map i ≫ g₁)))
I :
  GrothendieckTopology.Cover.Arrow
    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₂) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₂)
      (G.imageSieve (G.map i ≫ g₁)) ⋯)
I' : GrothendieckTopology.Cover.Arrow
  (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁) (G.imageSieve g₁) ⋯) :=
  { Y := I.Y, f := I.f ≫ i, hf := ⋯ }
apply :
  ∀ (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₁ ⋯),
    Eq (α := (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).map iUV.op) :
            (a : (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op I.Y))) →
              (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op V)))
          (f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op) :
        (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).map iUV.op) :
            (a : (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op I.Y))) →
              (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op V)))
          (f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I'.Y W₁ U I'.f g₁ ⋯).op) :
        (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
⊢ f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op =
    f ≫ Y.obj (P := Presheaf.IsSheaf J).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 : _ = _) ↦ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.IsDenseSubsite.equalizer_mem, CategoryTheory.GrothendieckTopology.Cover.Arrow.hf, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
f : obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U))) (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (hf : (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₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi :
  StructuredArrow.hom (StructuredArrow.mk (op g₁)) ≫ G.op.map (op i) =
    StructuredArrow.hom (StructuredArrow.mk (op (G.map i ≫ g₁)))
I :
  GrothendieckTopology.Cover.Arrow
    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₂) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₂)
      (G.imageSieve (G.map i ≫ g₁)) ⋯)
I' : GrothendieckTopology.Cover.Arrow
  (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁) (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₁ ⋯
⊢ Eq (α := (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).map iUV.op) :
          (a : (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op I.Y))) →
            (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op V)))
        (f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op) :
      (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).map iUV.op) :
          (a : (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op I.Y))) →
            (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op V)))
        (f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I'.Y W₁ U I'.f g₁ ⋯).op) :
      (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))

Tactic:
simp [I', ← Functor.map_comp, ← op_comp, hiUV]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
f : obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U))) (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (hf : (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 (P := Presheaf.IsSheaf J)) :=
  { pt := X,
    π :=
      {
        app := fun (g : StructuredArrow (op (G.obj U)) G.op) ↦
          ⋯.amalgamate
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (C := C) (unop g.2)) ↦
              Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (unop g.2)))
                ((J : (a : C) → Set (Sieve a)) (unop g.2)) S)
              (G.imageSieve g.hom.unop) ⋯)
            (fun
                (I :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (C := C) (unop g.2)) ↦
                      Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (unop g.2)))
                        ((J : (a : C) → Set (Sieve a)) (unop g.2)) S)
                      (G.imageSieve g.hom.unop) ⋯)) ↦
              f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op)
            ⋯,
        naturality := ⋯ } }
⊢ ∃ (a :
    (fun (X : Type w') ↦ X)
      (obj
        (obj yoneda
          ((obj (G.op.ran ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U)))
        (op X))),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (map yoneda (NatTrans.app (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J))) (op U)))
              (op X)) :
          (a :
              (fun (X : Type w') ↦ X)
                ((yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X))) →
            (fun (X : Type w') ↦ X) ((yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)))
        a =
      f

Tactic:
⟨(isPointwiseRightKanExtensionRanCounit G.op Y.1 (.op (G.obj U))).lift c, ?_⟩

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.isPointwiseRightKanExtensionRanCounit, CategoryTheory.ObjectProperty.FullSubcategory.obj, Opposite.op, Exists.intro, CategoryTheory.Functor.obj, CategoryTheory.Limits.IsLimit.lift
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
f : obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U))) (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (hf : (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 (P := Presheaf.IsSheaf J)) :=
  { pt := X,
    π :=
      {
        app := fun (g : StructuredArrow (op (G.obj U)) G.op) ↦
          ⋯.amalgamate
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (C := C) (unop g.2)) ↦
              Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (unop g.2)))
                ((J : (a : C) → Set (Sieve a)) (unop g.2)) S)
              (G.imageSieve g.hom.unop) ⋯)
            (fun
                (I :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (C := C) (unop g.2)) ↦
                      Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (unop g.2)))
                        ((J : (a : C) → Set (Sieve a)) (unop g.2)) S)
                      (G.imageSieve g.hom.unop) ⋯)) ↦
              f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op)
            ⋯,
        naturality := ⋯ } }
⊢ Eq (α :=
    c.pt ⟶
      (StructuredArrow.proj (op (G.obj U)) G.op ⋙
            obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj
        (StructuredArrow.mk (𝟙 (op (G.obj U)))))
    (CategoryStruct.comp (Y :=
      Limits.Cone.pt (J := StructuredArrow (op (G.obj U)) G.op)
        ((RightExtension.mk (obj G.op.ran (Y.obj (P := Presheaf.IsSheaf J)))
              (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J)))).coneAt
          (op (G.obj U))))
      (Limits.IsLimit.lift (G.op.isPointwiseRightKanExtensionRanCounit (Y.obj (P := Presheaf.IsSheaf J)) (op (G.obj U)))
        c)
      (NatTrans.app
        (Limits.Cone.π
          ((RightExtension.mk (obj G.op.ran (Y.obj (P := Presheaf.IsSheaf J)))
                (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J)))).coneAt
            (op (G.obj U))))
        (StructuredArrow.mk (𝟙 (op (G.obj U))))))
    (c.π.app (StructuredArrow.mk (𝟙 (op (G.obj U)))))

Tactic:
have := (isPointwiseRightKanExtensionRanCounit G.op Y.1 (.op (G.obj U))).fac c (.mk (𝟙 _))
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
f : obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U))) (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (hf : (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 (P := Presheaf.IsSheaf J)) :=
  { pt := X,
    π :=
      {
        app := fun (g : StructuredArrow (op (G.obj U)) G.op) ↦
          ⋯.amalgamate
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (C := C) (unop g.2)) ↦
              Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (unop g.2)))
                ((J : (a : C) → Set (Sieve a)) (unop g.2)) S)
              (G.imageSieve g.hom.unop) ⋯)
            (fun
                (I :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (C := C) (unop g.2)) ↦
                      Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (unop g.2)))
                        ((J : (a : C) → Set (Sieve a)) (unop g.2)) S)
                      (G.imageSieve g.hom.unop) ⋯)) ↦
              f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op)
            ⋯,
        naturality := ⋯ } }
this :
  CategoryStruct.comp (Y := (obj G.op.ran (Y.obj (P := Presheaf.IsSheaf J))).obj (op (G.obj U)))
      (Limits.IsLimit.lift (G.op.isPointwiseRightKanExtensionRanCounit (Y.obj (P := Presheaf.IsSheaf J)) (op (G.obj U)))
          c :
        c.pt ⟶
          Limits.Cone.pt (J := StructuredArrow (op (G.obj U)) G.op)
            ((RightExtension.mk (obj G.op.ran (Y.obj (P := Presheaf.IsSheaf J)))
                  (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J)))).coneAt
              (op (G.obj U))))
      (NatTrans.app (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J))) (op U)) =
    c.π.app (StructuredArrow.mk (𝟙 (op (G.obj U))))
I :
  GrothendieckTopology.Cover.Arrow
    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} U) ↦ S ∈ (J : (a : C) → Set (Sieve a)) U) (G.imageSieve (𝟙 (G.obj U)))
      ⋯)
⊢ G.map (l I.Y U U I.f (𝟙 (G.obj U)) ⋯) = G.map I.f

Tactic:
simp [hl]
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst_1 : Category.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_3 : Category.{w', w} A
inst_4 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_5 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
inst :
  IsIso (X :=
    obj (sheafToPresheaf J A) (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y))
    (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y))
⊢ IsIso (X := obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)
    (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y)

Tactic:
apply +allowSynthFailures ReflectsIsomorphisms.reflects (sheafToPresheaf J A)

Premises used: CategoryTheory.Functor.ReflectsIsomorphisms.reflects, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst_1 : Category.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_3 : Category.{w', w} A
inst_4 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_5 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
inst :
  ∀ (X : Cᵒᵖ),
    IsIso (X :=
      (obj (sheafToPresheaf J A)
            (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)).obj
        X)
      (NatTrans.app
        (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y)) X)
⊢ IsIso (X :=
    obj (sheafToPresheaf J A) (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y))
    (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y))

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst_1 : Category.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_3 : Category.{w', w} A
inst_4 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_5 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
inst :
  IsIso (X :=
    obj yoneda
      ((obj (sheafToPresheaf J A)
            (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)).obj
        (op U)))
    (map yoneda
      (NatTrans.app
        (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y)) (op U)))
⊢ IsIso (X :=
    (obj (sheafToPresheaf J A) (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)).obj
      (op U))
    (NatTrans.app (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y))
      (op U))

Tactic:
apply +allowSynthFailures ReflectsIsomorphisms.reflects yoneda

Premises used: CategoryTheory.Functor.ReflectsIsomorphisms.reflects, CategoryTheory.yoneda