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_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
⊢ Eq (α := 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)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op (unop X))) :
              (a : CD (F₁.obj (op (unop X)))) → CD (F₂.obj (op (unop X))))
            x :
          CD (F₂.obj (op (unop X)))) :
      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)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op (unop X))) :
              (a : CD (F₁.obj (op (unop X)))) → CD (F₂.obj (op (unop X))))
            y :
          CD (F₂.obj (op (unop X)))) :
      CD (F₂.obj (op Y)))

Tactic:
hf
-- 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
⊢ Eq (α := 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)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op (unop X))) :
              (a : CD (F₁.obj (op (unop X)))) → CD (F₂.obj (op (unop X))))
            x :
          CD (F₂.obj (op (unop X)))) :
      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)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op (unop X))) :
              (a : CD (F₁.obj (op (unop X)))) → CD (F₂.obj (op (unop X))))
            y :
          CD (F₂.obj (op (unop X)))) :
      CD (F₂.obj (op Y)))

Tactic:
exact hf
-- 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ᵒᵖ⦄ (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)
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))
⊢ 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))

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₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
hφ :
  ∀ ⦃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 φ

Tactic:
exact ⟨fun {X} x y h => hφ x y (by 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₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
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))
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J φ
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := FD) (CD := CD) x y)

Tactic:
(isLocallyInjective_iff_equalizerSieve_mem_imp J φ).1 inferInstance x y h

Premises used: CategoryTheory.Presheaf.isLocallyInjective_iff_equalizerSieve_mem_imp, inferInstance, Iff.mp
-- 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 : IsLocallyInjective (FD := FD) (CD := CD) J φ
inst_5 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
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))
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))
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := FD) (CD := CD) x y)

Tactic:
apply equalizerSieve_mem_of_equalizerSieve_app_mem J φ

Premises used: CategoryTheory.Presheaf.equalizerSieve_mem_of_equalizerSieve_app_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₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J φ
inst_5 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
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))
⊢ Eq (α := CD (F₃.obj X))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (ψ.app X) : (a : 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 :
          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))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y :
          CD (F₂.obj X)) :
      CD (F₃.obj X))

Tactic:
simpa using 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 : IsLocallyInjective (FD := FD) (CD := CD) J φ
inst_5 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
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))
⊢ 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))

Tactic:
exact equalizerSieve_mem J ψ _ _ (by simpa using h)

Premises used: 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₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J (φ ≫ ψ)
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))
⊢ 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))

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₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J φψ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J (φ ≫ ψ)

Tactic:
subst fac
-- 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 : IsLocallyInjective (FD := FD) (CD := CD) J (φ ≫ ψ)
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ

Tactic:
isLocallyInjective_of_isLocallyInjective J φ ψ

Premises used: CategoryTheory.Presheaf.isLocallyInjective_of_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₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J (φ ≫ ψ)
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ

Tactic:
exact isLocallyInjective_of_isLocallyInjective J φ ψ

Premises used: CategoryTheory.Presheaf.isLocallyInjective_of_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₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
mp : IsLocallyInjective (FD := FD) (CD := CD) J φψ → IsLocallyInjective (FD := FD) (CD := CD) J φ
mpr : IsLocallyInjective (FD := FD) (CD := CD) J φ → IsLocallyInjective (FD := FD) (CD := CD) J φψ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φψ ↔ 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₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
h : IsLocallyInjective (FD := FD) (CD := CD) J φψ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ

Tactic:
isLocallyInjective_of_isLocallyInjective_fac J fac

Premises used: CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_fac
-- 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₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
h : IsLocallyInjective (FD := FD) (CD := CD) J φψ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ

Tactic:
exact isLocallyInjective_of_isLocallyInjective_fac J fac

Premises used: CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_fac
-- 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₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
h : IsLocallyInjective (FD := FD) (CD := CD) J φ
mpr : IsLocallyInjective (FD := FD) (CD := CD) J (φ ≫ ψ)
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φψ

Tactic:
rw [← fac]
-- 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₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
h : IsLocallyInjective (FD := FD) (CD := CD) J φ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J (φ ≫ ψ)

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₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FD) (CD := CD) J ψ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J (φ ≫ ψ) ↔ IsLocallyInjective (FD := FD) (CD := CD) J φ

Tactic:
isLocallyInjective_iff_of_fac J rfl

Premises used: CategoryTheory.Presheaf.isLocallyInjective_iff_of_fac, 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₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
hsep : Presieve.IsSeparated.{w, v, u} J (F₁ ⋙ forget D (FC := FD) (CC := CD))
mp :
  IsLocallyInjective (FD := FD) (CD := CD) J φ →
    ∀ (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))
mpr :
  (∀ (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 φ
⊢ IsLocallyInjective (FD := FD) (CD := CD) J φ ↔
    ∀ (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))

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₂
hsep : Presieve.IsSeparated.{w, v, u} J (F₁ ⋙ forget D (FC := FD) (CC := CD))
h_1 : IsLocallyInjective (FD := FD) (CD := CD) J φ
X : Cᵒᵖ
x y : 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))
⊢ x = y

Tactic:
(hsep _ (equalizerSieve_mem J φ x y h)).ext (fun _ _ hf => hf)

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, 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₂
hsep : Presieve.IsSeparated.{w, v, u} J (F₁ ⋙ forget D (FC := FD) (CC := CD))
h_1 : IsLocallyInjective (FD := FD) (CD := CD) J φ
X : Cᵒᵖ
x y : 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))
⊢ x = y

Tactic:
exact (hsep _ (equalizerSieve_mem J φ x y h)).ext (fun _ _ hf => hf)

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presheaf.equalizerSieve_mem