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 : ∀ (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
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)

Tactic:
colimit.hom_ext (fun j => ?_)

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.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
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
x : Cᵒᵖ
h :
  ∀ (j : (J.Cover (unop x))ᵒᵖ),
    Eq (α :=
      Functor.obj (J.diagram (J.plusObj F) (unop x)) j ⟶
        (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) G).obj (P := Presheaf.IsSheaf J).obj x)
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (J.plusObj F) (unop x)))
        (colimit.ι (J.diagram (J.plusObj F) (unop x)) j)
        (NatTrans.app (InducedCategory.Hom.hom (Functor.map (plusPlusSheaf J D (FD := FD) (CD := CD)) 0)) x))
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (J.plusObj F) (unop x)))
        (colimit.ι (J.diagram (J.plusObj F) (unop x)) j) (NatTrans.app (InducedCategory.Hom.hom 0) x))
⊢ 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)

Tactic:
refine colimit.hom_ext (fun j => ?_)

Premises used: CategoryTheory.Limits.colimit.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
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
x : Cᵒᵖ
j : (J.Cover (unop x))ᵒᵖ
h :
  Eq (α :=
    Functor.obj (J.diagram (J.plusObj F) (unop x)) j ⟶
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) G).obj (P := Presheaf.IsSheaf J).obj x)
    (NatTrans.app (J.diagramNatTrans (J.plusMap 0) (unop x)) j ≫ colimit.ι (J.diagram (J.plusObj G) (unop x)) j) 0
⊢ Eq (α :=
    Functor.obj (J.diagram (J.plusObj F) (unop x)) j ⟶
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) G).obj (P := Presheaf.IsSheaf J).obj x)
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (J.plusObj F) (unop x)))
      (colimit.ι (J.diagram (J.plusObj F) (unop x)) j)
      (NatTrans.app (InducedCategory.Hom.hom (Functor.map (plusPlusSheaf J D (FD := FD) (CD := CD)) 0)) x))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (J.plusObj F) (unop x)))
      (colimit.ι (J.diagram (J.plusObj F) (unop x)) j) (NatTrans.app (InducedCategory.Hom.hom 0) x))

Tactic:
erw [colimit.ι_map, comp_zero]

Premises used: CategoryTheory.Limits.colimit.ι_map, CategoryTheory.Limits.comp_zero
-- 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
x : Cᵒᵖ
j : (J.Cover (unop x))ᵒᵖ
⊢ Eq (α :=
    Functor.obj (J.diagram (J.plusObj F) (unop x)) j ⟶
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) G).obj (P := Presheaf.IsSheaf J).obj x)
    (NatTrans.app (J.diagramNatTrans (J.plusMap 0) (unop x)) j ≫ colimit.ι (J.diagram (J.plusObj G) (unop x)) j) 0

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
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 Q : Functor.{v, w', u, w} Cᵒᵖ D
R : Sheaf.{v, w', u, w} J D
η : P ⟶ Q
γ : Q ⟶ Functor.obj (sheafToPresheaf J D) R
h :
  Eq (α := J.sheafify P ⟶ R.obj (P := Presheaf.IsSheaf J)) (J.sheafifyLift (η ≫ γ) ⋯)
    (J.sheafifyMap η ≫ J.sheafifyLift γ ⋯)
⊢ Eq (α :=
    (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P).obj (P := Presheaf.IsSheaf J) ⟶
      R.obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom
        ((Equiv.symm
              { toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P ⟶ R) ↦ J.toSheafify P ≫ e.hom,
                invFun := fun (e : P ⟶ Functor.obj (sheafToPresheaf J D) R) ↦ { hom := J.sheafifyLift e ⋯ },
                left_inv := ⋯, right_inv := ⋯ } :
            (a : P ⟶ (sheafToPresheaf J D).obj R) → (plusPlusSheaf J D).obj P ⟶ R)
          (η ≫ γ)) :
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P).obj (P := Presheaf.IsSheaf J) ⟶
        R.obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom
        (Functor.map (plusPlusSheaf J D (FD := FD) (CD := CD)) η ≫
          (Equiv.symm
                {
                  toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) Q ⟶ R) ↦
                    J.toSheafify Q ≫ e.hom,
                  invFun := fun (e : Q ⟶ Functor.obj (sheafToPresheaf J D) R) ↦ { hom := J.sheafifyLift e ⋯ },
                  left_inv := ⋯, right_inv := ⋯ } :
              (a : Q ⟶ (sheafToPresheaf J D).obj R) → (plusPlusSheaf J D).obj Q ⟶ R)
            γ) :
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P).obj (P := Presheaf.IsSheaf J) ⟶
        R.obj (P := Presheaf.IsSheaf J))

Tactic:
dsimp
-- 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 Q : Functor.{v, w', u, w} Cᵒᵖ D
R : Sheaf.{v, w', u, w} J D
η : P ⟶ Q
γ : Q ⟶ Functor.obj (sheafToPresheaf J D) R
h :
  Eq (α := J.sheafify P ⟶ R.obj (P := Presheaf.IsSheaf J)) (J.sheafifyMap η ≫ J.sheafifyLift γ ⋯)
    (J.sheafifyLift (η ≫ γ) ⋯)
⊢ Eq (α := J.sheafify P ⟶ R.obj (P := Presheaf.IsSheaf J)) (J.sheafifyLift (η ≫ γ) ⋯)
    (J.sheafifyMap η ≫ J.sheafifyLift γ ⋯)

Tactic:
symm
-- 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 Q : Functor.{v, w', u, w} Cᵒᵖ D
R : Sheaf.{v, w', u, w} J D
η : P ⟶ Q
γ : Q ⟶ Functor.obj (sheafToPresheaf J D) R
⊢ Eq (α := J.sheafify P ⟶ R.obj (P := Presheaf.IsSheaf J)) (J.sheafifyMap η ≫ J.sheafifyLift γ ⋯)
    (J.sheafifyLift (η ≫ γ) ⋯)

Tactic:
apply J.sheafifyMap_sheafifyLift

Premises used: CategoryTheory.GrothendieckTopology.sheafifyMap_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))
X : Functor.{v, w', u, w} Cᵒᵖ D
Y Y' : Sheaf.{v, w', u, w} J D
η : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) X ⟶ Y
γ : Y ⟶ Y'
dsimp : J.toSheafify X ≫ η.hom ≫ γ.hom = (J.toSheafify X ≫ η.hom) ≫ γ.hom
⊢ Eq (α := X ⟶ Functor.obj (sheafToPresheaf J D) Y')
    (({ toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) X ⟶ Y') ↦ J.toSheafify X ≫ e.hom,
            invFun := fun (e : X ⟶ Functor.obj (sheafToPresheaf J D) Y') ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
            right_inv := ⋯ } :
          (a : (plusPlusSheaf J D).obj X ⟶ Y') → X ⟶ (sheafToPresheaf J D).obj Y')
        (η ≫ γ) :
      X ⟶ Functor.obj (sheafToPresheaf J D) Y')
    (({ toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) X ⟶ Y) ↦ J.toSheafify X ≫ e.hom,
              invFun := fun (e : X ⟶ Functor.obj (sheafToPresheaf J D) Y) ↦ { hom := J.sheafifyLift e ⋯ },
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (plusPlusSheaf J D).obj X ⟶ Y) → X ⟶ (sheafToPresheaf J D).obj Y)
          η ≫
        Functor.map (sheafToPresheaf J D) γ :
      X ⟶ Functor.obj (sheafToPresheaf J D) Y')

Tactic:
dsimp
-- 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))
X : Functor.{v, w', u, w} Cᵒᵖ D
Y Y' : Sheaf.{v, w', u, w} J D
η : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) X ⟶ Y
γ : Y ⟶ Y'
rw rw₁ : J.toSheafify X ≫ η.hom ≫ γ.hom = J.toSheafify X ≫ η.hom ≫ γ.hom
⊢ J.toSheafify X ≫ η.hom ≫ γ.hom = (J.toSheafify X ≫ η.hom) ≫ γ.hom

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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))
⊢ Functor.IsRightAdjoint (C := Functor.{v, w', u, w} Cᵒᵖ D) (sheafToPresheaf J D)

Tactic:
(plusPlusAdjunction J D).isRightAdjoint

Premises used: CategoryTheory.plusPlusAdjunction, CategoryTheory.Adjunction.isRightAdjoint
-- 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))
F G : Sheaf.{v, w', u, w} J D
f : F ⟶ G
inst_8 : Mono f
⊢ Mono f.hom

Tactic:
(sheafToPresheaf J D).map_mono _

Premises used: CategoryTheory.Functor.map_mono, CategoryTheory.sheafToPresheaf
-- 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))
F G : Sheaf.{v, w', u, w} J D
f : F ⟶ G
m : Mono f
⊢ Mono f.hom

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
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))
F G : Sheaf.{v, w', u, w} J D
f : F ⟶ G
m : Mono f.hom
⊢ Mono f

Tactic:
Sheaf.Hom.mono_of_presheaf_mono J D f

Premises used: CategoryTheory.Sheaf.Hom.mono_of_presheaf_mono
-- 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))
F G : Sheaf.{v, w', u, w} J D
f : F ⟶ G
m : Mono f.hom
⊢ Mono f

Tactic:
exact Sheaf.Hom.mono_of_presheaf_mono J D f

Premises used: CategoryTheory.Sheaf.Hom.mono_of_presheaf_mono
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
T : C
hT : IsTerminal.{v_1, u_1} T
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
x x_1 : Cᵒᵖ
x_2 : x ⟶ x_1
simp : F.map (Quiver.Hom.op (hT.from (Opposite.unop x_1))) = F.map (Quiver.Hom.op (hT.from (Opposite.unop x)) ≫ x_2)
⊢ Eq (α :=
    obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) F) x ⟶
      (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) F).obj x_1)
    (map (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) F) x_2 ≫
      match (motive :=
        (x : Cᵒᵖ) →
          obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) F) x ⟶
            (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) F).obj x)
        x_1 with
      | Opposite.op X => F.map (hT.from X).op)
    ((match (motive :=
        (x : Cᵒᵖ) →
          obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) F) x ⟶
            (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) F).obj x)
        x with
      | Opposite.op X => F.map (hT.from X).op) ≫
      (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) F).map x_2)

Tactic:
simp only [Functor.comp_obj, Functor.const_obj_obj, Functor.id_obj, Functor.const_obj_map,
          Category.id_comp, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
T : C
hT : IsTerminal.{v_1, u_1} T
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
x x_1 : Cᵒᵖ
x_2 : x ⟶ x_1
e_a : hT.from (Opposite.unop x_1) = x_2.unop ≫ Quiver.Hom.unop (Quiver.Hom.op (hT.from (Opposite.unop x)))
⊢ F.map (Quiver.Hom.op (hT.from (Opposite.unop x_1))) = F.map (Quiver.Hom.op (hT.from (Opposite.unop x)) ≫ x_2)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
T : C
hT : IsTerminal.{v_1, u_1} T
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
x x_1 : Cᵒᵖ
x_2 : x ⟶ x_1
⊢ hT.from (Opposite.unop x_1) = x_2.unop ≫ Quiver.Hom.unop (Quiver.Hom.op (hT.from (Opposite.unop x)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
T : C
hT : IsTerminal.{v_1, u_1} T
X Y : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : X ⟶ Y
w :
  ∀ (x : Cᵒᵖ),
    Eq (α :=
      obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) X) x ⟶
        (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) Y).obj x)
      (NatTrans.app
        (map (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) f ≫
          {
            app := fun (x : Cᵒᵖ) ↦
              match (motive :=
                (x : Cᵒᵖ) →
                  obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) Y) x ⟶
                    (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) Y).obj x)
                x with
              | Opposite.op X => Y.map (hT.from X).op,
            naturality := ⋯ })
        x)
      (NatTrans.app
        ({
            app := fun (x : Cᵒᵖ) ↦
              match (motive :=
                (x : Cᵒᵖ) →
                  obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) X) x ⟶
                    (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) X).obj x)
                x with
              | Opposite.op X_1 => X.map (hT.from X_1).op,
            naturality := ⋯ } ≫
          map (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) f)
        x)
⊢ Eq (α := obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) X ⟶ obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) Y)
    (map (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) f ≫
      {
        app := fun (x : Cᵒᵖ) ↦
          match (motive :=
            (x : Cᵒᵖ) →
              obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) Y) x ⟶
                (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) Y).obj x)
            x with
          | Opposite.op X => Y.map (hT.from X).op,
        naturality := ⋯ })
    ({
        app := fun (x : Cᵒᵖ) ↦
          match (motive :=
            (x : Cᵒᵖ) →
              obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) X) x ⟶
                (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) X).obj x)
            x with
          | Opposite.op X_1 => X.map (hT.from X_1).op,
        naturality := ⋯ } ≫
      map (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) f)

Tactic:
ext