awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              x :
            CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              y :
            CD (P.obj (op I.Y)))) →
      x = y
X : C
S : J.Cover X
x :
  ToType.{t, w', w, u_1} (FC := FD) (CC := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)))
    (multiequalizer (S.index (J.plusObj P)))
t : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
ht :
  Meq.mk (FD := FD) (CD := CD) S t =
    (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      x
i : S.Arrow
⊢ (ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map i.f.op) :
        (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op i.Y)))
      t =
    (↑(Meq.mk (FD := FD) (CD := CD) S t) : (I : S.Arrow) → ToType ((J.plusObj P).obj (op I.Y))) i

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD ((J.plusObj P).obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
                (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
              x :
            CD ((J.plusObj P).obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
                (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
              y :
            CD ((J.plusObj P).obj (op I.Y)))) →
      x = y
⊢ Presheaf.IsSheaf J (J.plusObj (J.plusObj P))

Tactic:
apply isSheaf_of_sep

Premises used: CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
X : C
S : J.Cover X
x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
⊢ (∀ (I : S.Arrow),
      Eq (α := CD ((J.plusObj P).obj (op I.Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
              (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
            x :
          CD ((J.plusObj P).obj (op I.Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
              (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
            y :
          CD ((J.plusObj P).obj (op I.Y)))) →
    x = y

Tactic:
apply sep

Premises used: CategoryTheory.GrothendieckTopology.Plus.sep
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
⊢ J.plusMap (J.plusMap (𝟙 P)) = 𝟙 (J.plusObj (J.plusObj P))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
⊢ Eq (α := J.plusObj (J.plusObj P) ⟶ J.plusObj (J.plusObj R)) (J.plusMap (J.plusMap (η ≫ γ)))
    (J.plusMap (J.plusMap η) ≫ J.plusMap (J.plusMap γ))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
⊢ Eq (α := P ⟶ J.plusObj (J.plusObj Q)) (η ≫ J.toPlus Q ≫ J.plusMap (J.toPlus Q))
    ((J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ J.plusMap (J.plusMap η))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
⊢ Functor.obj (J.sheafification D) P = J.sheafify P

Tactic:
rfl

Premises used: CategoryTheory.GrothendieckTopology.sheafify, CategoryTheory.GrothendieckTopology.plusObj, rfl
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
⊢ Eq (α := Functor.obj (J.sheafification D) P ⟶ Functor.obj (J.sheafification D) Q) (Functor.map (J.sheafification D) η)
    (J.sheafifyMap η)

Tactic:
rfl

Premises used: CategoryTheory.GrothendieckTopology.plusMap, CategoryTheory.GrothendieckTopology.sheafifyMap, CategoryTheory.GrothendieckTopology.plusObj, rfl
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
⊢ Eq (α := Functor.obj (𝟭 (Functor.{v, w', u, w} Cᵒᵖ D)) P ⟶ Functor.obj (J.sheafification D) P)
    (NatTrans.app (J.toSheafification D) P) (J.toSheafify P)

Tactic:
rfl

Premises used: CategoryTheory.GrothendieckTopology.plusMap, CategoryTheory.GrothendieckTopology.toSheafify, CategoryTheory.GrothendieckTopology.sheafify, CategoryTheory.GrothendieckTopology.toPlus, CategoryTheory.GrothendieckTopology.plusObj, rfl
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (Y := J.plusObj P) (J.toPlus P)

Tactic:
haveI := isIso_toPlus_of_isSheaf J P hP
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
this : IsIso (Y := J.plusObj P) (J.toPlus P)
⊢ IsIso (Y := Functor.obj (J.plusFunctor D) (J.plusObj P))
    (CategoryStruct.comp (Y := J.plusObj P) (J.toPlus P) (Functor.map (J.plusFunctor D) (J.toPlus P)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ Eq (α := P ⟶ J.sheafify P) (Iso.hom (J.isoSheafify hP)) (J.toSheafify P)

Tactic:
rfl

Premises used: CategoryTheory.GrothendieckTopology.toSheafify, rfl
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ CategoryStruct.comp (Y := J.sheafify P) (J.toPlus P ≫ J.plusMap (J.toPlus P)) (J.plusLift (J.plusLift η hQ) hQ) = η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
hγ : J.toPlus (J.plusObj P) ≫ γ = J.plusLift η hQ
⊢ γ = J.sheafifyLift η hQ

Tactic:
apply plusLift_unique

Premises used: CategoryTheory.GrothendieckTopology.plusLift_unique
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
hγ : J.toPlus P ≫ J.toPlus (J.plusObj P) ≫ γ = η
⊢ J.toPlus (J.plusObj P) ≫ γ = J.plusLift η hQ

Tactic:
apply plusLift_unique

Premises used: CategoryTheory.GrothendieckTopology.plusLift_unique
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
hγ : (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ = η
⊢ J.toPlus P ≫ J.toPlus (J.plusObj P) ≫ γ = η

Tactic:
rw [← Category.assoc, ← plusMap_toPlus]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GrothendieckTopology.plusMap_toPlus
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ = η

Tactic:
h

Premises used: CategoryTheory.GrothendieckTopology.toSheafify, CategoryTheory.GrothendieckTopology.sheafify
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ = η

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
a : CategoryStruct.comp (Y := J.sheafify P) (J.toSheafify P) (Iso.inv (J.isoSheafify hP)) = 𝟙 P
⊢ Eq (α := J.sheafify P ⟶ P) (Iso.inv (J.isoSheafify hP)) (J.sheafifyLift (𝟙 P) hP)

Tactic:
apply J.sheafifyLift_unique

Premises used: CategoryTheory.GrothendieckTopology.sheafifyLift_unique
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ CategoryStruct.comp (Y := J.sheafify P) (J.toSheafify P) (Iso.inv (J.isoSheafify hP)) = 𝟙 P

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.sheafify P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ
apply : J.toPlus (J.plusObj P) ≫ η = J.toPlus (J.plusObj P) ≫ γ
⊢ η = γ

Tactic:
apply J.plus_hom_ext _ _ hQ

Premises used: CategoryTheory.GrothendieckTopology.plus_hom_ext
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.sheafify P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ
apply : J.toPlus P ≫ J.toPlus (J.plusObj P) ≫ η = J.toPlus P ≫ J.toPlus (J.plusObj P) ≫ γ
⊢ J.toPlus (J.plusObj P) ≫ η = J.toPlus (J.plusObj P) ≫ γ

Tactic:
apply J.plus_hom_ext _ _ hQ

Premises used: CategoryTheory.GrothendieckTopology.plus_hom_ext
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.sheafify P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ
rw : (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ η = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ
⊢ J.toPlus P ≫ J.toPlus (J.plusObj P) ≫ η = J.toPlus P ≫ J.toPlus (J.plusObj P) ≫ γ

Tactic:
rw [← Category.assoc, ← Category.assoc, ← plusMap_toPlus]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GrothendieckTopology.plusMap_toPlus
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.sheafify P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ η = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ

Tactic:
h

Premises used: CategoryTheory.GrothendieckTopology.toSheafify, CategoryTheory.GrothendieckTopology.sheafify
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.sheafify P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ η = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
a : CategoryStruct.comp (Y := J.sheafify P) (J.toSheafify P) (J.sheafifyMap η ≫ J.sheafifyLift γ hR) = η ≫ γ
⊢ Eq (α := J.sheafify P ⟶ R) (J.sheafifyMap η ≫ J.sheafifyLift γ hR) (J.sheafifyLift (η ≫ γ) hR)

Tactic:
apply J.sheafifyLift_unique

Premises used: CategoryTheory.GrothendieckTopology.sheafifyLift_unique
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
a : CategoryStruct.comp (Y := J.sheafify Q) (J.toSheafify P ≫ J.sheafifyMap η) (J.sheafifyLift γ hR) = η ≫ γ
a₁ : CategoryStruct.comp (Y := J.sheafify Q) (η ≫ J.toSheafify Q) (J.sheafifyLift γ hR) = η ≫ γ
a₂ : η ≫ CategoryStruct.comp (Y := J.sheafify Q) (J.toSheafify Q) (J.sheafifyLift γ hR) = η ≫ γ
a₃ a₄ : η ≫ γ = η ≫ γ
⊢ CategoryStruct.comp (Y := J.sheafify P) (J.toSheafify P) (J.sheafifyMap η ≫ J.sheafifyLift γ hR) = η ≫ γ

Tactic:
rw [← Category.assoc, ← J.toSheafify_naturality, Category.assoc, toSheafify_sheafifyLift]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GrothendieckTopology.toSheafify_naturality, CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
⊢ Presheaf.IsSheaf J (J.sheafify P)

Tactic:
GrothendieckTopology.Plus.isSheaf_plus_plus _ _

Premises used: CategoryTheory.GrothendieckTopology.sheafify, CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
inst_8 : Preadditive.{w', w} D
F G : Functor.{v, w', u, w} Cᵒᵖ D
h :
  ∀ (x : Cᵒᵖ),
    Eq.{w' + 1} (α :=
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) F).obj (P := Presheaf.IsSheaf J).obj x ⟶
        (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) G).obj (P := Presheaf.IsSheaf J).obj x)
      (NatTrans.app (InducedCategory.Hom.hom (Functor.map (plusPlusSheaf J D (FD := FD) (CD := CD)) 0)) x)
      (NatTrans.app (InducedCategory.Hom.hom 0) x)
⊢ Eq (α :=
    Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) F ⟶ Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) G)
    (Functor.map (plusPlusSheaf J D (FD := FD) (CD := CD)) 0) 0

Tactic:
ext : 3