awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
G : Functor.{vC, vD, uC, uD} C D
K : GrothendieckTopology.{vD, uD} D
inst_2 : G.IsLocallyFaithful K
U V : C
f₁ f₂ : U ⟶ V
e : G.map f₁ = G.map f₂
⊢ Membership.mem (γ := Set (Sieve.{vD, uD} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G (Sieve.equalizer f₁ f₂))

Tactic:
Functor.IsLocallyFaithful.functorPushforward_equalizer_mem _ _ e

Premises used: CategoryTheory.Functor.IsLocallyFaithful.functorPushforward_equalizer_mem
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
K : GrothendieckTopology.{vD, uD} D
G : Functor.{vC, vD, uC, uD} C D
inst_2 : G.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y),
    G.map f = G.map j ≫ i →
      Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            s :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            t :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
apply :
  ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄,
    (Sieve.functorPushforward G (G.imageSieve i)).arrows f →
      Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Y_1)))
            s :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Y_1)))
            t :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
⊢ s = t

Tactic:
apply (((isSheaf_iff_isSheaf_of_type _ _).1 ℱ.property) _
    (G.functorPushforward_imageSieve_mem K i)).isSeparatedFor.ext

Premises used: CategoryTheory.Functor.functorPushforward_imageSieve_mem, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.isSheaf_iff_isSheaf_of_type, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
K : GrothendieckTopology.{vD, uD} D
G : Functor.{vC, vD, uC, uD} C D
inst_2 : G.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y),
    G.map f = G.map j ≫ i →
      Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            s :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            t :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
Z : D
W : C
iWX : W ⟶ X
iZW : Z ⟶ G.obj W
iWY : W ⟶ Y
e : G.map iWY = G.map iWX ≫ i
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (iZW ≫ G.map iWX).op) :
          (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Z)))
        s :
      (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (iZW ≫ G.map iWX).op) :
          (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Z)))
        t :
      (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z)))

Tactic:
simp [h iWX iWY e]
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
K : GrothendieckTopology.{vD, uD} D
G : Functor.{vC, vD, uC, uD} C D
inst_2 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_2)
X Y : C
i₁ i₂ : X ⟶ Y
e : G.map i₁ = G.map i₂
s t : ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X),
    j ≫ i₁ = j ≫ i₂ →
      Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            s :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            t :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
apply :
  ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄,
    (Sieve.functorPushforward G (Sieve.equalizer i₁ i₂)).arrows f →
      Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Y_1)))
            s :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Y_1)))
            t :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y_1)))
⊢ s = t

Tactic:
apply (((isSheaf_iff_isSheaf_of_type _ _).1 ℱ.property) _
    (G.functorPushforward_equalizer_mem K i₁ i₂ e)).isSeparatedFor.ext

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.functorPushforward_equalizer_mem, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.isSheaf_iff_isSheaf_of_type, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
K : GrothendieckTopology.{vD, uD} D
G : Functor.{vC, vD, uC, uD} C D
inst_2 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_2)
X Y : C
i₁ i₂ : X ⟶ Y
e : G.map i₁ = G.map i₂
s t : ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X),
    j ≫ i₁ = j ≫ i₂ →
      Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            s :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map j).op) :
              (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) →
                (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj Z))))
            t :
          (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Z))))
Z : D
W : C
iWX : W ⟶ X
iZW : Z ⟶ G.obj W
hiWX : (Sieve.equalizer i₁ i₂).arrows iWX
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (iZW ≫ G.map iWX).op) :
          (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Z)))
        s :
      (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (iZW ≫ G.map iWX).op) :
          (a : (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op (G.obj X)))) → (fun (X : Type u_2) ↦ X) (ℱ.obj.obj (op Z)))
        t :
      (fun (X : Type u_2) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Z)))

Tactic:
simp [h iWX hiWX]
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
G_1 : Functor.{vC, vD, uC, uD} C D
J : GrothendieckTopology.{vC, uC} C
K : GrothendieckTopology.{vD, uD} D
A : Type u_1
inst_2 : Category.{v_1, u_1} A
G : Functor.{vC, vD, uC, uD} C D
inst_3 : G.Full
U V : C
f : G.obj U ⟶ G.obj V
rw :
  Membership.mem (γ := Set (Sieve.{vD, uD} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G (G.imageSieve (G.map (G.preimage f))))
⊢ Membership.mem (γ := Set (Sieve.{vD, uD} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G (G.imageSieve f))

Tactic:
rw [← G.map_preimage f]

Premises used: CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
G_1 : Functor.{vC, vD, uC, uD} C D
J : GrothendieckTopology.{vC, uC} C
K : GrothendieckTopology.{vD, uD} D
A : Type u_1
inst_2 : Category.{v_1, u_1} A
G : Functor.{vC, vD, uC, uD} C D
inst_3 : G.Full
U V : C
f : G.obj U ⟶ G.obj V
⊢ Membership.mem (γ := Set (Sieve.{vD, uD} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G (G.imageSieve (G.map (G.preimage f))))

Tactic:
simp only [Functor.imageSieve_map, Sieve.functorPushforward_top, GrothendieckTopology.top_mem]

Premises used: CategoryTheory.GrothendieckTopology.top_mem, CategoryTheory.Sieve.functorPushforward_top, CategoryTheory.Functor.imageSieve_map
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
G_1 : Functor.{vC, vD, uC, uD} C D
J : GrothendieckTopology.{vC, uC} C
K : GrothendieckTopology.{vD, uD} D
A : Type u_1
inst_2 : Category.{v_1, u_1} A
G : Functor.{vC, vD, uC, uD} C D
inst_3 : G.Faithful
U V : C
f₁ f₂ : U ⟶ V
e : G.map f₁ = G.map f₂
obtain :
  ∀ (e : G.map f₁ = G.map f₁),
    Membership.mem (γ := Set (Sieve.{vD, uD} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
      (Sieve.functorPushforward G (Sieve.equalizer f₁ f₁))
⊢ Membership.mem (γ := Set (Sieve.{vD, uD} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G (Sieve.equalizer f₁ f₂))

Tactic:
obtain rfl := G.map_injective e

Premises used: CategoryTheory.Functor.map_injective, rfl
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vD, uD} D
G_1 : Functor.{vC, vD, uC, uD} C D
J : GrothendieckTopology.{vC, uC} C
K : GrothendieckTopology.{vD, uD} D
A : Type u_1
inst_2 : Category.{v_1, u_1} A
G : Functor.{vC, vD, uC, uD} C D
inst_3 : G.Faithful
U V : C
f₁ : U ⟶ V
e : G.map f₁ = G.map f₁
⊢ Membership.mem (γ := Set (Sieve.{vD, uD} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G (Sieve.equalizer f₁ f₁))

Tactic:
simp
-- 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 : Functor.{v, v', u, u'} Cᵒᵖ D
X_1 : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F.obj X_1)
X Y : C
f : X ⟶ unop X_1
hf :
  Eq (α := CD (F.obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map f.op) : (a : CD (F.obj (op (unop X_1)))) → CD (F.obj (op X)))
        x :
      CD (F.obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map f.op) : (a : CD (F.obj (op (unop X_1)))) → CD (F.obj (op X)))
        y :
      CD (F.obj (op X)))
g : Y ⟶ X
dsimp :
  Eq (α := CD (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map (f.op ≫ g.op)) : (a : CD (F.obj X_1)) → CD (F.obj (op Y))) x :
      CD (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map (f.op ≫ g.op)) : (a : CD (F.obj X_1)) → CD (F.obj (op Y))) y :
      CD (F.obj (op Y)))
⊢ Eq (α := CD (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map (g ≫ f).op) :
          (a : CD (F.obj (op (unop X_1)))) → CD (F.obj (op Y)))
        x :
      CD (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map (g ≫ f).op) :
          (a : CD (F.obj (op (unop X_1)))) → CD (F.obj (op Y)))
        y :
      CD (F.obj (op Y)))

Tactic:
dsimp at 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 : Functor.{v, v', u, u'} Cᵒᵖ D
X_1 : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F.obj X_1)
X Y : C
f : X ⟶ unop X_1
hf :
  Eq (α := CD (F.obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map f.op) : (a : CD (F.obj X_1)) → CD (F.obj (op X))) x :
      CD (F.obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map f.op) : (a : CD (F.obj X_1)) → CD (F.obj (op X))) y :
      CD (F.obj (op X)))
g : Y ⟶ X
⊢ Eq (α := CD (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map (f.op ≫ g.op)) : (a : CD (F.obj X_1)) → CD (F.obj (op Y))) x :
      CD (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map (f.op ≫ g.op)) : (a : CD (F.obj X_1)) → CD (F.obj (op Y))) y :
      CD (F.obj (op Y)))

Tactic:
simp [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)
F : Functor.{v, v', u, u'} Cᵒᵖ D
X : Cᵒᵖ
x : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F.obj X)
⊢ equalizerSieve (FD := FD) (CD := CD) x x = ⊤

Tactic:
aesop
-- 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)
F : Functor.{v, v', u, u'} Cᵒᵖ D
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F.obj X)
mp : equalizerSieve (FD := FD) (CD := CD) x y = ⊤ → x = y
mpr : x = y → equalizerSieve (FD := FD) (CD := CD) x y = ⊤
⊢ equalizerSieve (FD := FD) (CD := CD) x y = ⊤ ↔ 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)
F : Functor.{v, v', u, u'} Cᵒᵖ D
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F.obj X)
h : equalizerSieve (FD := FD) (CD := CD) x y = ⊤
⊢ (equalizerSieve (FD := FD) (CD := CD) x y).arrows (𝟙 (unop 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)
F : Functor.{v, v', u, u'} Cᵒᵖ D
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F.obj X)
h : equalizerSieve (FD := FD) (CD := CD) x y = ⊤
⊢ x = y

Tactic:
simpa using (show equalizerSieve 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)
F : Functor.{v, v', u, u'} Cᵒᵖ D
X : Cᵒᵖ
x : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F.obj X)
⊢ equalizerSieve (FD := FD) (CD := CD) x x = ⊤

Tactic:
apply equalizerSieve_self_eq_top

Premises used: CategoryTheory.Presheaf.equalizerSieve_self_eq_top
-- 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₂
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))
⊢ 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.equalizerSieve_mem x y h

Premises used: CategoryTheory.Presheaf.IsLocallyInjective.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φ :
  ∀ (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))
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) ⊤

Tactic:
J.top_mem X.unop

Premises used: CategoryTheory.GrothendieckTopology.top_mem, Opposite.unop
-- 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))
h₁ : equalizerSieve (FD := FD) (CD := CD) 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:
convert! J.top_mem X.unop

Premises used: CategoryTheory.GrothendieckTopology.top_mem, Opposite.unop
-- 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))
h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ unop X), (equalizerSieve (FD := FD) (CD := CD) x y).arrows f ↔ Sieve.arrows ⊤ f
⊢ equalizerSieve (FD := FD) (CD := CD) x y = ⊤

Tactic:
ext Y f
-- 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) (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)))
⊢ (equalizerSieve (FD := FD) (CD := CD) x y).arrows f ↔ Sieve.arrows ⊤ f

Tactic:
simp only [equalizerSieve_apply, op_unop, Sieve.top_apply, iff_true]

Premises used: CategoryTheory.Sieve.top_apply, Opposite.op_unop, iff_true, CategoryTheory.Presheaf.equalizerSieve_apply