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₂
hφ :
  ∀ (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))
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Eq (α := CD (F₂.obj X))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x : CD (F₂.obj X))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y : CD (F₂.obj X))
Y : C
f : Y ⟶ unop X
h₁ :
  Eq (α := CD (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) x :
          CD (F₁.obj (op Y))) :
      CD (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) y :
          CD (F₁.obj (op Y))) :
      CD (F₂.obj (op Y)))
⊢ Eq (α := CD (F₁.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) x :
      CD (F₁.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) y :
      CD (F₁.obj (op Y)))

Tactic:
apply 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₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
hφ :
  ∀ (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))
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Eq (α := CD (F₂.obj X))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x : CD (F₂.obj X))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y : CD (F₂.obj X))
Y : C
f : Y ⟶ unop X
⊢ Eq (α := CD (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) x :
          CD (F₁.obj (op Y))) :
      CD (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj X)) → CD (F₁.obj (op Y))) y :
          CD (F₁.obj (op Y))) :
      CD (F₂.obj (op Y)))

Tactic:
simp [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₃
inst_4 : IsIso φ
X : Cᵒᵖ
rw :
  IsIso.{w, w + 1} (X := CD (F₁.obj X)) (Y := CD (F₂.obj X))
    (↾(⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X)))
⊢ Function.Bijective.{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))

Tactic:
rw [bijective_iff_isIso_ofHom]

Premises used: CategoryTheory.bijective_iff_isIso_ofHom
-- 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₃
inst_4 : IsIso φ
X : Cᵒᵖ
⊢ IsIso.{w, w + 1} (X := CD (F₁.obj X)) (Y := CD (F₂.obj X))
    (↾(⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X)) : (a : CD (F₁.obj X)) → CD (F₂.obj X)))

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₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
mp :
  IsLocallyInjective (FD := TypeCat.Fun) J (Functor.whiskerRight φ (forget D (FC := FD) (CC := CD))) →
    IsLocallyInjective (FD := FD) (CD := CD) J φ
mpr :
  IsLocallyInjective (FD := FD) (CD := CD) J φ →
    IsLocallyInjective (FD := TypeCat.Fun) J (Functor.whiskerRight φ (forget D (FC := FD) (CC := CD)))
⊢ IsLocallyInjective (FD := TypeCat.Fun) J (Functor.whiskerRight φ (forget D (FC := FD) (CC := CD))) ↔
    IsLocallyInjective (FD := FD) (CD := CD) J φ

Tactic:
constructor
-- 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₂
h : IsLocallyInjective (FD := TypeCat.Fun) J (Functor.whiskerRight φ (forget D (FC := FD) (CC := CD)))
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ

Tactic:
⟨fun x y h => equalizerSieve_mem J (Functor.whiskerRight φ (forget D)) x y h⟩

Premises used: CategoryTheory.Presheaf.IsLocallyInjective.mk
-- 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₂
h : IsLocallyInjective (FD := TypeCat.Fun) J (Functor.whiskerRight φ (forget D (FC := FD) (CC := CD)))
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ

Tactic:
exact ⟨fun x y h => equalizerSieve_mem J (Functor.whiskerRight φ (forget D)) x y 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₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
h : IsLocallyInjective (FD := FD) (CD := CD) J φ
⊢ IsLocallyInjective (FD := TypeCat.Fun) J (Functor.whiskerRight φ (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₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
mp :
  IsLocallyInjective (FD := FD) (CD := CD) J φ →
    ∀ ⦃X : Cᵒᵖ⦄ (x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)),
      Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)) →
        Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve (FD := FD) (CD := CD) x y)
mpr :
  (∀ ⦃X : Cᵒᵖ⦄ (x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)),
      Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)) →
        Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve (FD := FD) (CD := CD) x y)) →
    IsLocallyInjective (FD := FD) (CD := CD) J φ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ ↔
    ∀ ⦃X : Cᵒᵖ⦄ (x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)),
      Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
            ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)) →
        Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
          (equalizerSieve (FD := FD) (CD := CD) x y)

Tactic:
constructor
-- 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₂
h_1 : IsLocallyInjective (FD := FD) (CD := CD) J φ
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
S : Sieve.{v, u} (unop X) :=
  equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (x_1 : S.arrows f) ↦
    equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₁)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        y)
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := FD) (CD := CD) x y)

Tactic:
J.superset_covering ?_ (J.transitive h (Sieve.bind S.1 T) ?_)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.transitive, CategoryTheory.Sieve.bind, CategoryTheory.Sieve.arrows
-- 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₂
h_1 : IsLocallyInjective (FD := FD) (CD := CD) J φ
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
S : Sieve.{v, u} (unop X) :=
  equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (x_1 : S.arrows f) ↦
    equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₁)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        y)
mp : Sieve.bind S.arrows T ≤ equalizerSieve (FD := FD) (CD := CD) x y
mp₁ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop X⦄,
    Sieve.arrows
        (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
        f →
      Sieve.pullback f (Sieve.bind S.arrows T) ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := FD) (CD := CD) x y)

Tactic:
refine J.superset_covering ?_ (J.transitive h (Sieve.bind S.1 T) ?_)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.transitive, CategoryTheory.Sieve.bind, CategoryTheory.Sieve.arrows
-- 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₂
h_1 : IsLocallyInjective (FD := FD) (CD := CD) J φ
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
S : Sieve.{v, u} (unop X) :=
  equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (x_1 : S.arrows f) ↦
    equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₁)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        y)
Y Z : C
a : Y ⟶ Z
g : Z ⟶ unop X
hg : S.arrows g
ha : (T hg).arrows a
⊢ (equalizerSieve (FD := FD) (CD := CD) x y).arrows (a ≫ g)

Tactic:
simpa using ha
-- 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₂
h_1 : IsLocallyInjective (FD := FD) (CD := CD) J φ
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
S : Sieve.{v, u} (unop X) :=
  equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (x_1 : S.arrows f) ↦
    equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₁)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        y)
Y : C
f : Y ⟶ unop X
hf :
  Sieve.arrows
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
    f
⊢ Sieve.pullback f (Sieve.bind S.arrows T) ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
J.superset_covering (Sieve.le_pullback_bind S.1 T _ hf)
        (equalizerSieve_mem J φ _ _ ?_)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Sieve.le_pullback_bind, CategoryTheory.Sieve.arrows, CategoryTheory.Presheaf.equalizerSieve_mem
-- 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₂
h_1 : IsLocallyInjective (FD := FD) (CD := CD) J φ
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
S : Sieve.{v, u} (unop X) :=
  equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (x_1 : S.arrows f) ↦
    equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₁)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        y)
Y : C
f : Y ⟶ unop X
hf :
  Sieve.arrows
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
    f
mp :
  Eq (α := CD (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) :
              (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
            x :
          CD (F₁.obj (op Y))) :
      CD (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) :
              (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
            y :
          CD (F₁.obj (op Y))) :
      CD (F₂.obj (op Y)))
⊢ Sieve.pullback f (Sieve.bind S.arrows T) ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
refine J.superset_covering (Sieve.le_pullback_bind S.1 T _ hf)
        (equalizerSieve_mem J φ _ _ ?_)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Sieve.le_pullback_bind, CategoryTheory.Sieve.arrows, CategoryTheory.Presheaf.equalizerSieve_mem