awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
left : IsLocallyInjective (FD := FA) (CD := CA) f
right : IsLocallySurjective (FA := FA) (CA := CA) f
mp :
  IsLocallyInjective (FD := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
      (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f) ∧
    IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
      (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso f (sheafCompose J (forget A)),
      ← isLocallyBijective_iff_isIso']

Premises used: CategoryTheory.sheafCompose, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.forget, _private.0.CategoryTheory.Sheaf.isLocallyBijective_iff_isIso'
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
left : IsLocallyInjective (FD := FA) (CD := CA) f
right : IsLocallySurjective (FA := FA) (CA := CA) f
mp :
  IsLocallyInjective (FD := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
    (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)
mp₁ :
  IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
    (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)
⊢ IsLocallyInjective (FD := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
      (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f) ∧
    IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
      (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
left : IsLocallyInjective (FD := FA) (CD := CA) f
right : IsLocallySurjective (FA := FA) (CA := CA) f
⊢ IsLocallyInjective (FD := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
    (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
left : IsLocallyInjective (FD := FA) (CD := CA) f
right : IsLocallySurjective (FA := FA) (CA := CA) f
⊢ IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
    (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
h : IsIso f
mpr : IsLocallyInjective (FD := FA) (CD := CA) f
mpr₁ : IsLocallySurjective (FA := FA) (CA := CA) f
⊢ IsLocallyInjective (FD := FA) (CD := CA) f ∧ IsLocallySurjective (FA := FA) (CA := CA) f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
h : IsIso f
⊢ IsLocallyInjective (FD := FA) (CD := CA) f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
h : IsIso f
⊢ IsLocallySurjective (FA := FA) (CA := CA) f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
⊢ J.W f ↔ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f

Tactic:
apply WEqualsLocallyBijective.iff

Premises used: CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.iff
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
inst_5 : Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f
inst_6 : Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw : Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
⊢ J.W f

Tactic:
rw [W_iff_isLocallyBijective]

Premises used: CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
inst_5 : Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f
inst_6 : Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
left : Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f
right : Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
⊢ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
inst_5 : Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f
inst_6 : Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
⊢ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
inst_5 : Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f
inst_6 : Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
⊢ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
hf : J.W f
⊢ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f

Tactic:
((J.W_iff_isLocallyBijective f).1 hf).1

Premises used: And.left, Iff.mp, CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
hf : J.W f
⊢ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f

Tactic:
((J.W_iff_isLocallyBijective f).1 hf).2

Premises used: And.right, Iff.mp, CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
inst_5 : HasWeakSheafify.{v, v', u, u'} J A
P : Functor.{v, v', u, u'} Cᵒᵖ A
⊢ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J P)
    (CategoryTheory.toSheafify J P)

Tactic:
(J.W_toSheafify P).isLocallyInjective

Premises used: CategoryTheory.GrothendieckTopology.W.isLocallyInjective, CategoryTheory.GrothendieckTopology.W_toSheafify
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
D : Type w
inst_4 : Category.{w', w} D
FD : D → D → Type u_2
CD : D → Type (max u v)
inst_5 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_6 : ConcreteCategory D FD (CC := CD)
inst_7 : HasWeakSheafify.{v, w', u, w} J D
inst_8 : J.HasSheafCompose (forget D (FC := FD) (CC := CD))
inst_9 : J.PreservesSheafification (forget D (FC := FD) (CC := CD))
inst_10 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
⊢ J.WEqualsLocallyBijective D (FA := FD) (CA := CD)

Tactic:
apply WEqualsLocallyBijective.mk'

Premises used: CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.mk'
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
⊢ J.WEqualsLocallyBijective (Type (max u v)) (FA := TypeCat.Fun)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
rw :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J φ
rw₁ :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (φ ≫ toSheafify J Q)
rw₂ :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₂ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
        (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (φ ≫ toSheafify J Q)
rw₃ :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₂ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
        (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (toSheafify J P ≫ sheafifyMap J φ)
rw₄ rw₅ :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₂ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (toSheafify J P ≫ InducedCategory.Hom.hom (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (toSheafify J P ≫ sheafifyMap J φ)
⊢ Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J φ

Tactic:
rw [← Sheaf.isLocallyInjective_sheafToPresheaf_map_iff,
    ← isLocallyInjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallyInjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]

Premises used: CategoryTheory.toSheafify, CategoryTheory.ObjectProperty.ι_map, CategoryTheory.Presheaf.isLocallyInjective_comp_iff, CategoryTheory.Sheaf.isLocallyInjective_sheafToPresheaf_map_iff, CategoryTheory.Presheaf.comp_isLocallyInjective_iff, CategoryTheory.toSheafify_naturality
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
rw :
  IsLocallySurjective J (FA := FA) (CA := CA) (F :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) φ
rw₁ :
  IsLocallySurjective J (FA := FA) (CA := CA) (F :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (φ ≫ toSheafify J Q)
rw₂ :
  IsLocallySurjective J (FA := FA) (CA := CA) (G :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
        (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (φ ≫ toSheafify J Q)
rw₃ :
  IsLocallySurjective J (FA := FA) (CA := CA) (G :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
        (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (toSheafify J P ≫ sheafifyMap J φ)
rw₄ rw₅ :
  IsLocallySurjective J (FA := FA) (CA := CA) (G :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (toSheafify J P ≫ InducedCategory.Hom.hom (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) (G := sheafify J Q) (toSheafify J P ≫ sheafifyMap J φ)
⊢ Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallySurjective J (FA := FA) (CA := CA) φ

Tactic:
rw [← Sheaf.isLocallySurjective_sheafToPresheaf_map_iff,
    ← isLocallySurjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallySurjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]

Premises used: CategoryTheory.Sheaf.isLocallySurjective_sheafToPresheaf_map_iff, CategoryTheory.toSheafify, CategoryTheory.Presheaf.comp_isLocallySurjective_iff, CategoryTheory.ObjectProperty.ι_map, CategoryTheory.Presheaf.isLocallySurjective_comp_iff, CategoryTheory.toSheafify_naturality
-- 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
J : GrothendieckTopology.{vC, uC} C
K : GrothendieckTopology.{vD, uD} D
U V : C
f : G.obj U ⟶ G.obj V
Y₁ Y₂ : C
i₁ : Y₁ ⟶ U
l : Y₁ ⟶ V
hl : G.map l = G.map i₁ ≫ f
i₂ : Y₂ ⟶ Y₁
⊢ G.map (i₂ ≫ l) = G.map (i₂ ≫ i₁) ≫ f

Tactic:
simp [hl]
-- 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
J : GrothendieckTopology.{vC, uC} C
K : GrothendieckTopology.{vD, uD} D
U V : C
f : G.obj U ⟶ G.obj V
Y₁ Y₂ : C
i₁ : Y₁ ⟶ U
l : Y₁ ⟶ V
hl : G.map l = G.map i₁ ≫ f
i₂ : Y₂ ⟶ Y₁
⊢ ∃ (l : Y₂ ⟶ V), G.map l = G.map (i₂ ≫ i₁) ≫ f

Tactic:
exact ⟨i₂ ≫ l, by simp [hl]⟩
-- 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
U V : C
f : U ⟶ V
h : ∀ ⦃W : C⦄ (g : W ⟶ U), (G.imageSieve (G.map f)).arrows g ↔ Sieve.arrows ⊤ g
⊢ G.imageSieve (G.map f) = ⊤

Tactic:
ext W g
-- 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
U V : C
f : U ⟶ V
W : C
g : W ⟶ U
⊢ G.map (g ≫ f) = G.map g ≫ G.map f

Tactic:
simp
-- 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
U V : C
f : U ⟶ V
W : C
g : W ⟶ U
⊢ (G.imageSieve (G.map f)).arrows g ↔ Sieve.arrows ⊤ g

Tactic:
simpa using ⟨g ≫ f, by simp⟩
-- 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
J : GrothendieckTopology.{vC, uC} C
K : GrothendieckTopology.{vD, uD} D
U V : C
f₁ f₂ : U ⟶ V
⊢ ∀ {Y Z : C} {f : Y ⟶ U}, f ≫ f₁ = f ≫ f₂ → ∀ (g : Z ⟶ Y), (g ≫ f) ≫ f₁ = (g ≫ f) ≫ f₂

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
U V : C
f : U ⟶ V
h : ∀ ⦃Y : C⦄ (f_1 : Y ⟶ U), (equalizer f f).arrows f_1 ↔ arrows ⊤ f_1
⊢ equalizer f f = ⊤

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
U V : C
f : U ⟶ V
Y : C
f_1 : Y ⟶ U
⊢ (equalizer f f).arrows f_1 ↔ arrows ⊤ f_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
U V : C
f₁ f₂ : U ⟶ V
⊢ equalizer f₁ f₂ = Presheaf.equalizerSieve (FD := TypeCat.Fun) (F := Functor.obj yoneda V) f₁ f₂

Tactic:
rfl

Premises used: CategoryTheory.Presheaf.equalizerSieve, CategoryTheory.Sieve.equalizer, Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
Goal:
C : Type uC
inst : Category.{vC, uC} C
D : Type uD
inst_1 : Category.{vC, uD} D
G : Functor.{vC, vC, uC, uD} C D
U V : C
f : G.obj U ⟶ G.obj V
⊢ G.imageSieve f = Presheaf.imageSieve (FA := TypeCat.Fun) (yonedaMap G V) f

Tactic:
rfl

Premises used: CategoryTheory.Presheaf.imageSieve, Quiver.Hom.unop, CategoryTheory.Functor.imageSieve, 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 : Functor.{vC, vD, uC, uD} C D
K : GrothendieckTopology.{vD, uD} D
inst_2 : G.IsLocallyFull K
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 f))

Tactic:
Functor.IsLocallyFull.functorPushforward_imageSieve_mem _

Premises used: CategoryTheory.Functor.IsLocallyFull.functorPushforward_imageSieve_mem