awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i : W.shape.L
k : K
dsimp :
  ⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app k).app (op x.Y)) ⋯ ≫
      (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op =
    S.ι i ≫ (E.π.app k).app (op i.Y)
⊢ (multiforkEvaluationCone F E X W S).π.app k ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op =
    S.ι i ≫ (E.π.app k).app (op i.Y)

Tactic:
dsimp [multiforkEvaluationCone, Presheaf.isLimitOfIsSheaf]

Premises used: CategoryTheory.Sheaf.multiforkEvaluationCone, CategoryTheory.Presheaf.isLimitOfIsSheaf
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i : W.shape.L
k : K
rw rw₁ : S.ι i ≫ (E.π.app k).app (op i.Y) = S.ι i ≫ (E.π.app k).app (op i.Y)
⊢ ⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app k).app (op x.Y)) ⋯ ≫
      (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op =
    S.ι i ≫ (E.π.app k).app (op i.Y)

Tactic:
rw [Presheaf.IsSheaf.amalgamate_map]

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
apply :
  ∀ (j : K),
    Eq (α := S.pt ⟶ ((F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X)).obj j)
      (m ≫ NatTrans.app (Cone.π (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E)) j)
      (CategoryStruct.comp (Y :=
        Cone.pt (F := (F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
          (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E))
        ((fun (S : Multifork (W.index E.pt)) ↦
              (IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE)
                  (multiforkEvaluationCone F E X W S) :
                (multiforkEvaluationCone F E X W S).pt ⟶
                  Cone.pt (F := (F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
                    (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E)))
            S :
          (multiforkEvaluationCone F E X W S).pt ⟶
            Cone.pt (F := (F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
              (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E))
        (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E)) j :
          Functor.obj.{z', w', z, w}
              (Functor.obj (Functor.const K)
                (Cone.pt (F := (F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
                  (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E)))
              j ⟶
            ((F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X)).obj j))
⊢ m =
    (fun (S : Multifork (W.index E.pt)) ↦
        (IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE)
            (multiforkEvaluationCone F E X W S) :
          (multiforkEvaluationCone F E X W S).pt ⟶
            Cone.pt (F := (F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
              (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E)))
      S

Tactic:
apply (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).hom_ext

Premises used: Opposite, CategoryTheory.Limits.IsLimit.hom_ext, Opposite.op, CategoryTheory.evaluation, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
dsimp :
  m ≫ (E.π.app k).app (op X) =
    IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
      (E.π.app k).app (op X)
⊢ Eq (α := S.pt ⟶ ((F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X)).obj k)
    (m ≫ NatTrans.app (Cone.π (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E)) k)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := (F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
        (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E))
      ((fun (S : Multifork (W.index E.pt)) ↦
            (IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE)
                (multiforkEvaluationCone F E X W S) :
              (multiforkEvaluationCone F E X W S).pt ⟶
                Cone.pt (F := (F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
                  (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E)))
          S :
        (multiforkEvaluationCone F E X W S).pt ⟶
          Cone.pt (F := (F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
            (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E))
      (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E)) k :
        Functor.obj.{z', w', z, w}
            (Functor.obj (Functor.const K)
              (Cone.pt (F := (F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
                (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op X)) E)))
            k ⟶
          ((F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X)).obj k))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
erw : m ≫ (E.π.app k).app (op X) = (multiforkEvaluationCone F E X W S).π.app k
⊢ m ≫ (E.π.app k).app (op X) =
    IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
      (E.π.app k).app (op X)

Tactic:
erw [(isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).fac]

Premises used: Opposite, Opposite.op, CategoryTheory.evaluation, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Functor.obj, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
h :
  ∀ (I : W.Arrow),
    (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map I.f.op =
      (multiforkEvaluationCone F E X W S).π.app k ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map I.f.op
⊢ m ≫ (E.π.app k).app (op X) = (multiforkEvaluationCone F E X W S).π.app k

Tactic:
apply Presheaf.IsSheaf.hom_ext (F.obj k).2 W

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
h :
  (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op =
    ⋯.amalgamate W
        (fun (x : W.Arrow) ↦
          (Multifork.ofι (W.index ((F.obj k).obj (P := Presheaf.IsSheaf J))) S.pt
                (fun (i : W.shape.L) ↦ S.ι i ≫ (E.π.app k).app (op i.Y)) ⋯).ι
            x)
        ⋯ ≫
      (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op
⊢ (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op =
    (multiforkEvaluationCone F E X W S).π.app k ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op

Tactic:
dsimp only [multiforkEvaluationCone, Presheaf.isLimitOfIsSheaf]

Premises used: CategoryTheory.Sheaf.multiforkEvaluationCone, CategoryTheory.Presheaf.isLimitOfIsSheaf
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
h :
  (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op =
    (Multifork.ofι (W.index ((F.obj k).obj (P := Presheaf.IsSheaf J))) S.pt
          (fun (i : W.shape.L) ↦ S.ι i ≫ (E.π.app k).app (op i.Y)) ⋯).ι
      i
⊢ (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op =
    ⋯.amalgamate W
        (fun (x : W.Arrow) ↦
          (Multifork.ofι (W.index ((F.obj k).obj (P := Presheaf.IsSheaf J))) S.pt
                (fun (i : W.shape.L) ↦ S.ι i ≫ (E.π.app k).app (op i.Y)) ⋯).ι
            x)
        ⋯ ≫
      (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op

Tactic:
rw [(F.obj k).property.amalgamate_map]

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
h :
  (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op =
    Multifork.ι
      { pt := S.pt,
        π :=
          {
            app := fun (x : WalkingMulticospan W.shape) ↦
              match (motive :=
                (x : WalkingMulticospan W.shape) →
                  S.pt ⟶
                    match (motive := WalkingMulticospan W.shape → D) x with
                    | WalkingMulticospan.left a => (F.obj k).obj (P := Presheaf.IsSheaf J).obj (op a.Y)
                    | WalkingMulticospan.right b => (F.obj k).obj (P := Presheaf.IsSheaf J).obj (op b.r.Z))
                x with
              | WalkingMulticospan.left a => S.ι a ≫ (E.π.app k).app (op a.Y)
              | WalkingMulticospan.right b =>
                (S.ι b.fst ≫ (E.π.app k).app (op b.fst.Y)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map b.r.g₁.op,
            naturality := ⋯ } }
      i
⊢ (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op =
    (Multifork.ofι (W.index ((F.obj k).obj (P := Presheaf.IsSheaf J))) S.pt
          (fun (i : W.shape.L) ↦ S.ι i ≫ (E.π.app k).app (op i.Y)) ⋯).ι
      i

Tactic:
dsimp [Multifork.ofι]

Premises used: CategoryTheory.Limits.Multifork.ofι
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
h : (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op = S.ι i ≫ (E.π.app k).app (op i.Y)
⊢ (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op =
    Multifork.ι
      { pt := S.pt,
        π :=
          {
            app := fun (x : WalkingMulticospan W.shape) ↦
              match (motive :=
                (x : WalkingMulticospan W.shape) →
                  S.pt ⟶
                    match (motive := WalkingMulticospan W.shape → D) x with
                    | WalkingMulticospan.left a => (F.obj k).obj (P := Presheaf.IsSheaf J).obj (op a.Y)
                    | WalkingMulticospan.right b => (F.obj k).obj (P := Presheaf.IsSheaf J).obj (op b.r.Z))
                x with
              | WalkingMulticospan.left a => S.ι a ≫ (E.π.app k).app (op a.Y)
              | WalkingMulticospan.right b =>
                (S.ι b.fst ≫ (E.π.app k).app (op b.fst.Y)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map b.r.g₁.op,
            naturality := ⋯ } }
      i

Tactic:
change _ = S.ι i ≫ _

Premises used: CategoryTheory.Limits.Multifork.ι
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
h :
  m ≫ (Functor.obj (Functor.obj (Functor.const K) E.pt) k).map i.f.op ≫ (E.π.app k).app (op i.Y) =
    m ≫ (W.multifork E.pt).ι i ≫ (E.π.app k).app (op i.Y)
⊢ (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj (P := Presheaf.IsSheaf J).map i.f.op = S.ι i ≫ (E.π.app k).app (op i.Y)

Tactic:
erw [← hm, Category.assoc, ← (E.π.app k).naturality, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
⊢ m ≫ (Functor.obj (Functor.obj (Functor.const K) E.pt) k).map i.f.op ≫ (E.π.app k).app (op i.Y) =
    m ≫ (W.multifork E.pt).ι i ≫ (E.π.app k).app (op i.Y)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
rw : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork E.pt))
⊢ Presheaf.IsSheaf J E.pt

Tactic:
rw [Presheaf.isSheaf_iff_multifork]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_multifork
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
S : J.Cover X
⊢ Nonempty (IsLimit (S.multifork E.pt))

Tactic:
⟨isLimitMultiforkOfIsLimit _ _ hE _ _⟩

Premises used: CategoryTheory.Sheaf.isLimitMultiforkOfIsLimit, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
S : J.Cover X
⊢ Nonempty (IsLimit (S.multifork E.pt))

Tactic:
exact ⟨isLimitMultiforkOfIsLimit _ _ hE _ _⟩
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
P : Functor.{v, w', u, w} Cᵒᵖ D
h : ObjectProperty.LimitOfShape (Presheaf.IsSheaf J) K P
F : K ⥤ Sheaf.{v, w', u, w} J D :=
  ObjectProperty.lift (Presheaf.IsSheaf J) h.toLimitPresentation (P := Presheaf.IsSheaf J).diag ⋯
⊢ Presheaf.IsSheaf J P

Tactic:
isSheaf_of_isLimit F _ h.isLimit

Premises used: CategoryTheory.Sheaf.isSheaf_of_isLimit, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.LimitPresentation.isLimit
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
P : Functor.{v, w', u, w} Cᵒᵖ D
h : ObjectProperty.LimitOfShape (Presheaf.IsSheaf J) K P
F : K ⥤ Sheaf.{v, w', u, w} J D :=
  ObjectProperty.lift (Presheaf.IsSheaf J) h.toLimitPresentation (P := Presheaf.IsSheaf J).diag ⋯
⊢ Presheaf.IsSheaf J P

Tactic:
exact isSheaf_of_isLimit F _ h.isLimit

Premises used: CategoryTheory.Sheaf.isSheaf_of_isLimit, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.LimitPresentation.isLimit
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
⊢ HasLimitsOfShape K (Sheaf.{v, w', u, w} J D)

Tactic:
hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (sheafToPresheaf J D)

Premises used: CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
inst_4 : HasFiniteProducts.{w', w} D
⊢ HasFiniteProducts (Sheaf.{v, w', u, w} J D)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteProducts.mk
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfShape.{z', z, w', w} K D
inst_4 : HasFiniteLimits.{w', w} D
⊢ HasFiniteLimits (Sheaf.{v, w', u, w} J D)

Tactic:
⟨fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteLimits.mk
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasLimitsOfSize.{u₁, u₂, w', w} D
⊢ HasLimitsOfSize.{u₁, u₂, max u w', max (max (max w u) w') v} (Sheaf.{v, w', u, w} J D)

Tactic:
hasLimits_of_hasLimits_createsLimits (sheafToPresheaf J D)

Premises used: CategoryTheory.hasLimits_of_hasLimits_createsLimits, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D_1 : Type w
inst_1 : Category.{w', w} D_1
K : Type z
inst_2 : Category.{z', z} K
D : Type w
inst_3 : Category.{max v u, w} D
inst_4 : HasLimits D
⊢ HasLimits (Sheaf J D)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
rw :
  Eq (α :=
    Functor.obj (sheafToPresheaf J D) (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) (F.obj k)) ⟶
      (Functor.obj (Functor.obj (Functor.const K) (sheafifyCocone E).pt) k).obj (P := Presheaf.IsSheaf J))
    (Functor.map (sheafToPresheaf J D) (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      ((sheafifyCocone E).ι.app k).hom)
    (Functor.map (sheafToPresheaf J D) (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      E.ι.app k ≫ toSheafify J E.pt)
⊢ ((sheafifyCocone E).ι.app k).hom = E.ι.app k ≫ toSheafify J E.pt

Tactic:
rw [← cancel_epi ((sheafToPresheaf _ _).map
    ((sheafificationAdjunction J D).counit.app (F.obj k)))]

Premises used: CategoryTheory.sheafificationAdjunction, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.cancel_epi, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
dsimp :
  Eq (α :=
    (Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J) ⟶
      (Functor.obj (presheafToSheaf J D) E.pt).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      InducedCategory.Hom.hom (NatTrans.app (inv (Adjunction.counit (sheafificationAdjunction J D))) (F.obj k)) ≫
        InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      E.ι.app k ≫ toSheafify J E.pt)
⊢ Eq (α :=
    Functor.obj (sheafToPresheaf J D) (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) (F.obj k)) ⟶
      (Functor.obj (Functor.obj (Functor.const K) (sheafifyCocone E).pt) k).obj (P := Presheaf.IsSheaf J))
    (Functor.map (sheafToPresheaf J D) (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      ((sheafifyCocone E).ι.app k).hom)
    (Functor.map (sheafToPresheaf J D) (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      E.ι.app k ≫ toSheafify J E.pt)

Tactic:
dsimp [sheafifyCocone]

Premises used: CategoryTheory.Sheaf.sheafifyCocone