awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
hsep : Presieve.IsSeparated.{w, v, u} J (F₁ ⋙ forget D (FC := FD) (CC := CD))
⊢ (∀ (X : Cᵒᵖ),
      Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj X)) (β := CD (F₂.obj X))
        (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X))) →
    IsLocallyInjective (FD := FD) (CD := CD) J φ

Tactic:
apply isLocallyInjective_of_injective

Premises used: CategoryTheory.Presheaf.isLocallyInjective_of_injective
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
X : Cᵒᵖ
x : F.obj X
property : x ∈ G.obj X
this :
  ∀ (y : F.obj X) (property_1 : y ∈ G.obj X),
    Eq (α := F.obj X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X)
            (Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property) :
          F.obj X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X)
            (Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) y property_1) :
          F.obj X) →
      Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property =
        Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) y property_1
⊢ ∀ ⦃a₂ : G.toFunctor.obj X⦄,
    Eq (α := F.obj X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X)
            (Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property) :
          F.obj X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X) a₂ : F.obj X) →
      Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property = a₂

Tactic:
⟨y, _⟩
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
X : Cᵒᵖ
x : F.obj X
property : x ∈ G.obj X
y : F.obj X
property_1 : y ∈ G.obj X
h :
  Eq (α := F.obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X)
        (Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property) :
      F.obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X)
        (Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) y property_1) :
      F.obj X)
⊢ Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property =
    Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) y property_1

Tactic:
Subtype.ext h

Premises used: Subtype.ext
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
X : Cᵒᵖ
x : F.obj X
property : x ∈ G.obj X
y : F.obj X
property_1 : y ∈ G.obj X
h :
  Eq (α := F.obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X)
        (Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property) :
      F.obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X)
        (Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) y property_1) :
      F.obj X)
⊢ Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property =
    Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) y property_1

Tactic:
exact Subtype.ext h

Premises used: Subtype.ext
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (FC := TypeCat.Fun) (P.obj X)
h :
  Eq (α := (J.plusObj P).obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (J.toPlus P) X) : (a : P.obj X) → (J.plusObj P).obj X) x :
      (J.plusObj P).obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (J.toPlus P) X) : (a : P.obj X) → (J.plusObj P).obj X) y :
      (J.plusObj P).obj X)
⊢ ∃ (W : J.Cover (unop X)) (h1 : W ⟶ ⊤) (h2 : W ⟶ ⊤),
    Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ x) h1 =
      Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ y) h2

Tactic:
rw [toPlus_eq_mk, toPlus_eq_mk, eq_mk_iff_exists] at h

Premises used: CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk, CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (FC := TypeCat.Fun) (P.obj X)
h :
  ∃ (W : J.Cover (unop X)) (h1 : W ⟶ ⊤) (h2 : W ⟶ ⊤),
    Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ x) h1 =
      Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ y) h2
obtain :
  ∀ (W : J.Cover (unop X)) (h₁ h₂ : W ⟶ ⊤)
    (eq :
      Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ x) h₁ =
        Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ y) h₂),
    Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
      (equalizerSieve (FD := TypeCat.Fun) x y)
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := TypeCat.Fun) x y)

Tactic:
obtain ⟨W, h₁, h₂, eq⟩ := h
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (FC := TypeCat.Fun) (P.obj X)
W : J.Cover (unop X)
h₁ h₂ : W ⟶ ⊤
eq :
  Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ x) h₁ =
    Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ y) h₂
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := TypeCat.Fun) x y)

Tactic:
J.superset_covering (fun Y f hf => congr_fun (congr_arg Subtype.val eq) ⟨Y, f, hf⟩) W.2

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, congr_arg, CategoryTheory.GrothendieckTopology.Cover.Arrow.mk, congr_fun, Subtype.val, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (FC := TypeCat.Fun) (P.obj X)
W : J.Cover (unop X)
h₁ h₂ : W ⟶ ⊤
eq :
  Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ x) h₁ =
    Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ y) h₂
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := TypeCat.Fun) x y)

Tactic:
exact J.superset_covering (fun Y f hf => congr_fun (congr_arg Subtype.val eq) ⟨Y, f, hf⟩) W.2

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
rw : IsLocallyInjective (FD := TypeCat.Fun) J (F₂ := J.sheafify P) (J.toPlus P ≫ J.toPlus (J.plusObj P))
⊢ IsLocallyInjective (FD := TypeCat.Fun) J (F₂ := J.sheafify P) (J.toPlus P ≫ J.plusMap (J.toPlus P))

Tactic:
rw [GrothendieckTopology.plusMap_toPlus]

Premises used: CategoryTheory.GrothendieckTopology.plusMap_toPlus
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
⊢ IsLocallyInjective (FD := TypeCat.Fun) J (F₂ := J.sheafify P) (J.toPlus P ≫ J.toPlus (J.plusObj P))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD_1 : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD_1 X) (CD_1 Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD_1)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
CD : D → Type (max u v)
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
P : Functor.{v, v', u, u'} Cᵒᵖ D
inst_6 : HasWeakSheafify.{v, v', u, u'} J D
inst_7 : J.HasSheafCompose (forget D (FC := FD) (CC := CD))
inst_8 : J.PreservesSheafification (forget D (FC := FD) (CC := CD))
rw :
  IsLocallyInjective (FD := TypeCat.Fun) J (F₂ := sheafify J P ⋙ forget D (FC := FD) (CC := CD))
    (CategoryStruct.comp (Y := sheafify J (P ⋙ forget D (FC := FD) (CC := CD)))
      (CategoryStruct.comp (Y := J.sheafify (P ⋙ forget D (FC := FD) (CC := CD)))
          (J.toSheafify (P ⋙ forget D (FC := FD) (CC := CD)))
          (Iso.hom (plusPlusIsoSheafify J (Type (max u v)) (FD := TypeCat.Fun) (P ⋙ forget D (FC := FD) (CC := CD)))) :
        P ⋙ forget D (FC := FD) (CC := CD) ⟶ sheafify J (P ⋙ forget D (FC := FD) (CC := CD)))
      (Iso.hom (sheafifyComposeIso J (forget D (FC := FD) (CC := CD)) P) :
        sheafify J (P ⋙ forget D (FC := FD) (CC := CD)) ⟶ sheafify J P ⋙ forget D (FC := FD) (CC := CD)))
⊢ IsLocallyInjective (FD := FD) (CD := CD) J (F₂ := sheafify J P) (toSheafify J P)

Tactic:
rw [← isLocallyInjective_forget_iff, ← sheafComposeIso_hom_fac,
    ← toSheafify_plusPlusIsoSheafify_hom]

Premises used: CategoryTheory.sheafComposeIso_hom_fac, CategoryTheory.Presheaf.isLocallyInjective_forget_iff, CategoryTheory.toSheafify_plusPlusIsoSheafify_hom
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD_1 : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD_1 X) (CD_1 Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD_1)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
CD : D → Type (max u v)
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
P : Functor.{v, v', u, u'} Cᵒᵖ D
inst_6 : HasWeakSheafify.{v, v', u, u'} J D
inst_7 : J.HasSheafCompose (forget D (FC := FD) (CC := CD))
inst_8 : J.PreservesSheafification (forget D (FC := FD) (CC := CD))
⊢ IsLocallyInjective (FD := TypeCat.Fun) J (F₂ := sheafify J P ⋙ forget D (FC := FD) (CC := CD))
    (CategoryStruct.comp (Y := sheafify J (P ⋙ forget D (FC := FD) (CC := CD)))
      (CategoryStruct.comp (Y := J.sheafify (P ⋙ forget D (FC := FD) (CC := CD)))
          (J.toSheafify (P ⋙ forget D (FC := FD) (CC := CD)))
          (Iso.hom (plusPlusIsoSheafify J (Type (max u v)) (FD := TypeCat.Fun) (P ⋙ forget D (FC := FD) (CC := CD)))) :
        P ⋙ forget D (FC := FD) (CC := CD) ⟶ sheafify J (P ⋙ forget D (FC := FD) (CC := CD)))
      (Iso.hom (sheafifyComposeIso J (forget D (FC := FD) (CC := CD)) P) :
        sheafify J (P ⋙ forget D (FC := FD) (CC := CD)) ⟶ sheafify J P ⋙ forget D (FC := FD) (CC := CD)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
⊢ Presheaf.IsLocallyInjective (FD := FD) (CD := CD) J (F₁ := Functor.obj (sheafToPresheaf J D) F₁)
      (Functor.map (sheafToPresheaf J D) φ) ↔
    IsLocallyInjective (FD := FD) (CD := CD) φ

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : IsIso φ
change :
  Presheaf.IsLocallyInjective (FD := FD) (CD := CD) J (F₁ := Functor.obj (sheafToPresheaf J D) F₁)
    (Functor.map (sheafToPresheaf J D) φ)
⊢ IsLocallyInjective (FD := FD) (CD := CD) φ

Tactic:
change Presheaf.IsLocallyInjective J ((sheafToPresheaf _ _).map φ)

Premises used: CategoryTheory.Functor.map, CategoryTheory.sheafToPresheaf, CategoryTheory.Presheaf.IsLocallyInjective
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : IsIso φ
⊢ Presheaf.IsLocallyInjective (FD := FD) (CD := CD) J (F₁ := Functor.obj (sheafToPresheaf J D) F₁)
    (Functor.map (sheafToPresheaf J D) φ)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
hφ :
  ∀ (X : Cᵒᵖ),
    Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj (P := Presheaf.IsSheaf J).obj X)) (β :=
      CD (F₂.obj (P := Presheaf.IsSheaf J).obj X))
      (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.hom.app X)) : (a : CD (F₁.obj.obj X)) → CD (F₂.obj.obj X))
⊢ Mono φ

Tactic:
have : ∀ X, Mono (φ.hom.app X) := fun X ↦ ConcreteCategory.mono_of_injective _ (hφ X)
  (sheafToPresheaf _ _).mono_of_mono_map (NatTrans.mono_of_mono_app φ.1)

Premises used: CategoryTheory.Functor.mono_of_mono_map, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.NatTrans.mono_of_mono_app, CategoryTheory.ConcreteCategory.mono_of_injective, CategoryTheory.NatTrans.app, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
inst_5 : IsLocallyInjective (FD := FD) (CD := CD) φ
⊢ IsLocallyInjective (FD := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget D (FC := FD) (CC := CD))) F₁)
    (Functor.map (sheafCompose J (forget D (FC := FD) (CC := CD))) φ)

Tactic:
Presheaf.isLocallyInjective_forget J φ.1

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerRight, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Presheaf.isLocallyInjective_forget
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
h : Presieve.IsSheaf.{w, v, u} J (F₁.obj (P := Presheaf.IsSheaf J) ⋙ forget D (FC := FD) (CC := CD))
⊢ Presieve.IsSeparated.{w, v, u} J (F₁.obj (P := Presheaf.IsSheaf J) ⋙ forget D (FC := FD) (CC := CD))

Tactic:
apply Presieve.IsSheaf.isSeparated

Premises used: CategoryTheory.Presieve.IsSheaf.isSeparated
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
h : Presheaf.IsSheaf J (F₁.obj (P := Presheaf.IsSheaf J) ⋙ forget D (FC := FD) (CC := CD))
⊢ Presieve.IsSheaf.{w, v, u} J (F₁.obj (P := Presheaf.IsSheaf J) ⋙ forget D (FC := FD) (CC := CD))

Tactic:
rw [← isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
⊢ Presheaf.IsSheaf J (F₁.obj (P := Presheaf.IsSheaf J) ⋙ forget D (FC := FD) (CC := CD))

Tactic:
((sheafCompose J (forget D)).obj F₁).2

Premises used: CategoryTheory.sheafCompose, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, CategoryTheory.forget, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
⊢ Presheaf.IsSheaf J (F₁.obj (P := Presheaf.IsSheaf J) ⋙ forget D (FC := FD) (CC := CD))

Tactic:
exact ((sheafCompose J (forget D)).obj F₁).2

Premises used: CategoryTheory.sheafCompose, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.forget, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
inst_5 : IsLocallyInjective (FD := FD) (CD := CD) φ
hφ :
  ∀ (X : Cᵒᵖ),
    Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj (P := Presheaf.IsSheaf J).obj X)) (β :=
      CD (F₂.obj (P := Presheaf.IsSheaf J).obj X))
      (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.hom.app X)) : (a : CD (F₁.obj.obj X)) → CD (F₂.obj.obj X))
⊢ Mono φ

Tactic:
apply mono_of_injective

Premises used: CategoryTheory.Sheaf.mono_of_injective
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
inst_5 hφ : IsLocallyInjective (FD := FD) (CD := CD) φ
⊢ ∀ (X : Cᵒᵖ),
    Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj (P := Presheaf.IsSheaf J).obj X)) (β :=
      CD (F₂.obj (P := Presheaf.IsSheaf J).obj X))
      (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.hom.app X)) : (a : CD (F₁.obj.obj X)) → CD (F₂.obj.obj X))

Tactic:
rw [← isLocallyInjective_iff_injective]

Premises used: CategoryTheory.Sheaf.isLocallyInjective_iff_injective
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
inst_5 : IsLocallyInjective (FD := FD) (CD := CD) φ
⊢ IsLocallyInjective (FD := FD) (CD := CD) φ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallyInjective
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsLocallyInjective.{w, w, v, w + 1, u, w} (C := C) (FD := TypeCat.Fun) (J := J) (F₁ := image f) (F₂ := G)
    { hom := (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι }

Tactic:
infer_instance