awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
P_1 : Functor.{v, t, u, w} Cᵒᵖ D
e_1 :
  (P_1 ⟶ sheafify J P_1) =
    (Functor.obj (𝟭 (Functor.{v, t, u, w} Cᵒᵖ D)) P_1 ⟶
      Functor.obj (sheafToPresheaf J D) (Functor.obj (presheafToSheaf J D) P_1))
e_3 : P_1 = Functor.obj (𝟭 (Functor.{v, t, u, w} Cᵒᵖ D)) P_1
e_4 : J.sheafify P_1 = Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafToPresheaf J D) P_1
P : Functor.{v, t, u, w} Cᵒᵖ D
h h₁ : Eq (α := P ⟶ J.sheafify P) (J.toPlus P ≫ J.plusMap (J.toPlus P)) (J.toPlus P ≫ J.plusMap (J.toPlus P))
⊢ J.toPlus P ≫ J.plusMap (J.toPlus P) = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ 𝟙 (J.sheafify P)

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : HasFiniteLimits.{t, w} D
inst_14 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
⊢ HasSheafify.{v, t, u, w} J D

Tactic:
HasSheafify.mk' J D (plusPlusAdjunction J D)

Premises used: CategoryTheory.plusPlusAdjunction, CategoryTheory.HasSheafify.mk'
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
⊢ HasSheafify J (Type (max u v))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : FinitaryExtensive.{w', w} D
inst_3 : HasPullbacks.{w', w} D
inst_4 : HasSheafify.{v, w', u, w} J D
⊢ FinitaryExtensive (Sheaf.{v, w', u, w} J D)

Tactic:
finitaryExtensive_of_reflective (sheafificationAdjunction _ _)

Premises used: CategoryTheory.finitaryExtensive_of_reflective, CategoryTheory.sheafificationAdjunction
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : Adhesive.{w', w} D
inst_3 : HasPullbacks.{w', w} D
inst_4 : HasPushouts.{w', w} D
inst_5 : HasSheafify.{v, w', u, w} J D
⊢ Adhesive (Sheaf.{v, w', u, w} J D)

Tactic:
adhesive_of_reflective (sheafificationAdjunction _ _)

Premises used: CategoryTheory.sheafificationAdjunction, CategoryTheory.adhesive_of_reflective
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : HasSheafify J (Type w)
⊢ FinitaryExtensive (Sheaf J (Type w))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : HasSheafify J (Type w)
⊢ Adhesive (Sheaf J (Type w))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : HasSheafify J (Type w)
⊢ Balanced (Sheaf J (Type w))

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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
simp :
  S.ι (W.shape.fst i) ≫
      (E.π.app k).app (op (W.shape.fst i).Y) ≫ (W.index ((F.obj k).obj (P := Presheaf.IsSheaf J))).fst i =
    S.ι (W.shape.snd i) ≫
      (E.π.app k).app (op (W.shape.snd i).Y) ≫ (W.index ((F.obj k).obj (P := Presheaf.IsSheaf J))).snd i
⊢ Eq (α := S.pt ⟶ (W.index ((F.obj k).obj (P := Presheaf.IsSheaf J))).right i)
    ((fun (i : W.shape.L) ↦ S.ι i ≫ (E.π.app k).app (op i.Y)) (W.shape.fst i) ≫
      (W.index ((F.obj k).obj (P := Presheaf.IsSheaf J))).fst i)
    ((fun (i : W.shape.L) ↦ S.ι i ≫ (E.π.app k).app (op i.Y)) (W.shape.snd i) ≫
      (W.index ((F.obj k).obj (P := Presheaf.IsSheaf J))).snd i)

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
erw :
  S.ι (W.shape.fst i) ≫
      (Functor.obj (Functor.obj (Functor.const K) E.pt) k).map i.r.g₁.op ≫ (E.π.app k).app (op i.r.Z) =
    S.ι (W.shape.snd i) ≫
      (Functor.obj (Functor.obj (Functor.const K) E.pt) k).map i.r.g₂.op ≫ (E.π.app k).app (op i.r.Z)
⊢ S.ι (W.shape.fst i) ≫
      (E.π.app k).app (op (W.shape.fst i).Y) ≫ (W.index ((F.obj k).obj (P := Presheaf.IsSheaf J))).fst i =
    S.ι (W.shape.snd i) ≫
      (E.π.app k).app (op (W.shape.snd i).Y) ≫ (W.index ((F.obj k).obj (P := Presheaf.IsSheaf J))).snd i

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

Premises used: 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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
dsimp :
  S.ι i.fst ≫ E.pt.map i.r.g₁.op ≫ (E.π.app k).app (op i.r.Z) =
    S.ι i.snd ≫ E.pt.map i.r.g₂.op ≫ (E.π.app k).app (op i.r.Z)
⊢ S.ι (W.shape.fst i) ≫
      (Functor.obj (Functor.obj (Functor.const K) E.pt) k).map i.r.g₁.op ≫ (E.π.app k).app (op i.r.Z) =
    S.ι (W.shape.snd i) ≫
      (Functor.obj (Functor.obj (Functor.const K) E.pt) k).map i.r.g₂.op ≫ (E.π.app k).app (op i.r.Z)

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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
simp :
  (S.ι i.fst ≫ E.pt.map i.r.g₁.op) ≫ (E.π.app k).app (op i.r.Z) =
    (S.ι i.snd ≫ E.pt.map i.r.g₂.op) ≫ (E.π.app k).app (op i.r.Z)
⊢ S.ι i.fst ≫ E.pt.map i.r.g₁.op ≫ (E.π.app k).app (op i.r.Z) =
    S.ι i.snd ≫ E.pt.map i.r.g₂.op ≫ (E.π.app k).app (op i.r.Z)

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
e_a : S.ι i.fst ≫ E.pt.map i.r.g₁.op = S.ι i.snd ≫ E.pt.map i.r.g₂.op
⊢ (S.ι i.fst ≫ E.pt.map i.r.g₁.op) ≫ (E.π.app k).app (op i.r.Z) =
    (S.ι i.snd ≫ E.pt.map i.r.g₂.op) ≫ (E.π.app k).app (op i.r.Z)

Tactic:
congr 1
-- 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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
⊢ S.ι i.fst ≫ E.pt.map i.r.g₁.op = S.ι i.snd ≫ E.pt.map i.r.g₂.op

Tactic:
apply S.condition

Premises used: CategoryTheory.Limits.Multifork.condition
-- 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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
dsimp :
  Eq.{w' + 1} (α := S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op X))
    (𝟙 S.pt ≫ ⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app j).app (op x.Y)) ⋯)
    (⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app i).app (op x.Y)) ⋯ ≫ (F.map f).hom.app (op X))
⊢ Eq.{w' + 1} (α :=
    Functor.obj.{z', w', z, w} (Functor.obj (Functor.const K) S.pt) i ⟶
      (F ⋙ sheafToPresheaf J D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X)).obj j)
    (Functor.map (Functor.obj (Functor.const K) S.pt) f ≫
      (Presheaf.isLimitOfIsSheaf J ((F.obj j).obj (P := Presheaf.IsSheaf J)) W ⋯).lift
        (Multifork.ofι (W.index ((F.obj j).obj (P := Presheaf.IsSheaf J))) S.pt
          (fun (i : W.shape.L) ↦ S.ι i ≫ (E.π.app j).app (op i.Y)) ⋯))
    ((Presheaf.isLimitOfIsSheaf J ((F.obj i).obj (P := Presheaf.IsSheaf J)) W ⋯).lift
        (Multifork.ofι (W.index ((F.obj i).obj (P := Presheaf.IsSheaf J))) S.pt
          (fun (i_1 : W.shape.L) ↦ S.ι i_1 ≫ (E.π.app i).app (op i_1.Y)) ⋯) ≫
      (F ⋙ sheafToPresheaf J D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X)).map f)

Tactic:
dsimp [Presheaf.isLimitOfIsSheaf]

Premises used: 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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
rw :
  Eq (α := S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op X))
    (⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app j).app (op x.Y)) ⋯ :
      S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op X))
    (⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app i).app (op x.Y)) ⋯ ≫ (F.map f).hom.app (op X) :
      S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op X))
⊢ Eq.{w' + 1} (α := S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op X))
    (𝟙 S.pt ≫ ⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app j).app (op x.Y)) ⋯)
    (⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app i).app (op x.Y)) ⋯ ≫ (F.map f).hom.app (op X))

Tactic:
rw [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- 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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
h :
  ∀ (I : W.Arrow),
    Eq (α := S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op I.Y))
      (⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app j).app (op x.Y)) ⋯ ≫
          (F.obj j).obj (P := Presheaf.IsSheaf J).map I.f.op :
        S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op I.Y))
      ((⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app i).app (op x.Y)) ⋯ ≫ (F.map f).hom.app (op X)) ≫
          (F.obj j).obj (P := Presheaf.IsSheaf J).map I.f.op :
        S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op I.Y))
⊢ Eq (α := S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op X))
    (⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app j).app (op x.Y)) ⋯ :
      S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op X))
    (⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app i).app (op x.Y)) ⋯ ≫ (F.map f).hom.app (op X) :
      S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op X))

Tactic:
apply Presheaf.IsSheaf.hom_ext (F.obj j).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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
ii : W.Arrow
h : S.ι ii ≫ (E.π.app j).app (op ii.Y) = (S.ι ii ≫ (E.π.app i).app (op ii.Y)) ≫ (F.map f).hom.app (op ii.Y)
⊢ Eq (α := S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op ii.Y))
    (⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app j).app (op x.Y)) ⋯ ≫
        (F.obj j).obj (P := Presheaf.IsSheaf J).map ii.f.op :
      S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op ii.Y))
    ((⋯.amalgamate W (fun (x : W.Arrow) ↦ S.ι x ≫ (E.π.app i).app (op x.Y)) ⋯ ≫ (F.map f).hom.app (op X)) ≫
        (F.obj j).obj (P := Presheaf.IsSheaf J).map ii.f.op :
      S.pt ⟶ (F.obj j).obj (P := Presheaf.IsSheaf J).obj (op ii.Y))

Tactic:
rw [Presheaf.IsSheaf.amalgamate_map, Category.assoc, ← (F.map f).hom.naturality, ←
          Category.assoc, Presheaf.IsSheaf.amalgamate_map]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Presheaf.IsSheaf.amalgamate_map, CategoryTheory.Functor.map, CategoryTheory.NatTrans.naturality, CategoryTheory.InducedCategory.Hom.hom
-- 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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
ii : W.Arrow
h :
  S.ι ii ≫ (E.π.app i ≫ (F ⋙ sheafToPresheaf J D).map f).app (op ii.Y) =
    S.ι ii ≫ (E.π.app i).app (op ii.Y) ≫ (F.map f).hom.app (op ii.Y)
⊢ S.ι ii ≫ (E.π.app j).app (op ii.Y) = (S.ι ii ≫ (E.π.app i).app (op ii.Y)) ≫ (F.map f).hom.app (op ii.Y)

Tactic:
erw [Category.assoc, ← E.w f]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cone.w
-- 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
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
ii : W.Arrow
h h₁ h₂ h₃ :
  S.ι ii ≫ (E.π.app i ≫ (F ⋙ sheafToPresheaf J D).map f).app (op ii.Y) =
    S.ι ii ≫ (E.π.app i).app (op ii.Y) ≫ (F.map f).hom.app (op ii.Y)
⊢ S.ι ii ≫ (E.π.app i ≫ (F ⋙ sheafToPresheaf J D).map f).app (op ii.Y) =
    S.ι ii ≫ (E.π.app i).app (op ii.Y) ≫ (F.map f).hom.app (op ii.Y)

Tactic:
cat_disch
-- 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
apply :
  ∀ (j : K),
    Eq (α := S.pt ⟶ ((F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op i.Y)).obj j)
      (((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 ≫
          (W.multifork E.pt).ι i) ≫
        NatTrans.app (Cone.π (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op i.Y)) E)) j)
      (S.ι i ≫ NatTrans.app (Cone.π (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op i.Y)) E)) j)
⊢ (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 ≫
      (W.multifork E.pt).ι i =
    S.ι i

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

Premises used: Opposite, CategoryTheory.Limits.IsLimit.hom_ext, Opposite.op, CategoryTheory.evaluation, CategoryTheory.GrothendieckTopology.Cover.Arrow.Y, 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)
i : W.shape.L
k : K
dsimp :
  (IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
        E.pt.map i.f.op) ≫
      (E.π.app k).app (op i.Y) =
    S.ι i ≫ (E.π.app k).app (op i.Y)
⊢ Eq (α := S.pt ⟶ ((F ⋙ sheafToPresheaf J D) ⋙ Functor.obj (evaluation Cᵒᵖ D) (op i.Y)).obj k)
    (((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 ≫
        (W.multifork E.pt).ι i) ≫
      NatTrans.app (Cone.π (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op i.Y)) E)) k)
    (S.ι i ≫ NatTrans.app (Cone.π (Functor.mapCone (Functor.obj (evaluation Cᵒᵖ D) (op i.Y)) E)) k)

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)
i : W.shape.L
k : K
erw :
  IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
      (E.π.app k).app (op X) ≫ ((F ⋙ sheafToPresheaf J D).obj k).map i.f.op =
    S.ι i ≫ (E.π.app k).app (op i.Y)
⊢ (IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
        E.pt.map i.f.op) ≫
      (E.π.app k).app (op i.Y) =
    S.ι i ≫ (E.π.app k).app (op i.Y)

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

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)
i : W.shape.L
k : K
dsimp :
  IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
      (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)
⊢ IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
      (E.π.app k).app (op X) ≫ ((F ⋙ sheafToPresheaf J D).obj k).map i.f.op =
    S.ι i ≫ (E.π.app k).app (op i.Y)

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)
i : W.shape.L
k : K
rw :
  (IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
        (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)
⊢ IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
      (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:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
erw :
  (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)
⊢ (IsLimit.lift (isLimitOfPreserves (Functor.obj (evaluation Cᵒᵖ D) (op X)) hE) (multiforkEvaluationCone F E X W S) ≫
        (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 [(isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).fac
        (multiforkEvaluationCone F E X W S)]

Premises used: Opposite, CategoryTheory.Sheaf.multiforkEvaluationCone, Opposite.op, CategoryTheory.evaluation, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Functor.obj, CategoryTheory.Limits.IsLimit.fac