awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
inst_5 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op X))
S : Sieve.{v, u} X :=
  imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦
    equalizerSieve.{w', v', v, u', u, u_1} (FD := FA) (CD := CA) (F := F₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
            x)
          f hf))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y))) x)
refine_1 : Sieve.bind S.arrows T ≤ imageSieve (FA := FA) (CA := CA) f₁ x
refine_2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop (op X)⦄,
    Sieve.arrows
        (imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
            x))
        f →
      Sieve.pullback f (Sieve.bind S.arrows T) ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ imageSieve (FA := FA) (CA := CA) f₁ x ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
refine J.superset_covering ?_ (J.transitive (imageSieve_mem J (f₁ ≫ f₂) (f₂.app _ x))
      (Sieve.bind S.1 T) ?_)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.transitive, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Sieve.bind, CategoryTheory.Sieve.arrows, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.NatTrans.app, CategoryTheory.Presheaf.imageSieve_mem
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
inst_5 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op X))
S : Sieve.{v, u} X :=
  imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦
    equalizerSieve.{w', v', v, u', u, u_1} (FD := FA) (CD := CA) (F := F₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
            x)
          f hf))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y))) x)
Y Z : C
a : Y ⟶ Z
g : Z ⟶ unop (op X)
hg : S.arrows g
ha : (T g hg).arrows a
⊢ Eq (α := CA (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₁.map a.op) : (a : CA (F₁.obj (op Z))) → CA (F₁.obj (op Y)))
            (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
              ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) :
                  (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
                x)
              g hg) :
          CA (F₁.obj (op Y))) :
      CA (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map (a ≫ g).op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y)))
        x :
      CA (F₂.obj (op Y)))

Tactic:
simpa using ha
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
inst_5 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op X))
S : Sieve.{v, u} X :=
  imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦
    equalizerSieve.{w', v', v, u', u, u_1} (FD := FA) (CD := CA) (F := F₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
            x)
          f hf))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y))) x)
Y Z : C
a : Y ⟶ Z
g : Z ⟶ unop (op X)
hg : S.arrows g
ha : (T g hg).arrows a
⊢ (imageSieve (FA := FA) (CA := CA) f₁ x).arrows (a ≫ g)

Tactic:
exact ⟨F₁.map a.op (localPreimage (f₁ ≫ f₂) _ _ hg), by simpa using ha⟩
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
inst_5 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op X))
S : Sieve.{v, u} X :=
  imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦
    equalizerSieve.{w', v', v, u', u, u_1} (FD := FA) (CD := CA) (F := F₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
            x)
          f hf))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y))) x)
Y : C
f : Y ⟶ unop (op X)
hf :
  Sieve.arrows
    (imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x))
    f
refine_2 : T f hf ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ Sieve.pullback f (Sieve.bind S.arrows T) ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
apply J.superset_covering (Sieve.le_pullback_bind _ _ _ hf)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Sieve.le_pullback_bind
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
inst_5 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op X))
S : Sieve.{v, u} X :=
  imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦
    equalizerSieve.{w', v', v, u', u, u_1} (FD := FA) (CD := CA) (F := F₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
            x)
          f hf))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y))) x)
Y : C
f : Y ⟶ unop (op X)
hf :
  Sieve.arrows
    (imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x))
    f
refine_2 :
  Eq (α := CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
            (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
              ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) :
                  (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
                x)
              f hf) :
          CA (F₂.obj (op Y))) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y))) x :
          CA (F₂.obj (op Y))) :
      CA (F₃.obj (op Y)))
⊢ T f hf ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
apply equalizerSieve_mem J f₂

Premises used: CategoryTheory.Presheaf.equalizerSieve_mem
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₃
inst_5 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
⊢ IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)

Tactic:
subst fac
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₁

Tactic:
isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective J f₁ f₂

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₁

Tactic:
exact isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective J f₁ f₂

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
mp : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂) → IsLocallyInjective (FD := FA) (CD := CA) J f₂
mpr : IsLocallyInjective (FD := FA) (CD := CA) J f₂ → IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
⊢ IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂) ↔ IsLocallyInjective (FD := FA) (CD := CA) J f₂

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
h : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
⊢ IsLocallyInjective (FD := FA) (CD := CA) J f₂

Tactic:
isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective J f₁ f₂

Premises used: CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
h : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
⊢ IsLocallyInjective (FD := FA) (CD := CA) J f₂

Tactic:
exact isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective J f₁ f₂

Premises used: CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
h : IsLocallyInjective (FD := FA) (CD := CA) J f₂
⊢ IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
mp : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂) → IsLocallySurjective J (FA := FA) (CA := CA) f₁
mpr : IsLocallySurjective J (FA := FA) (CA := CA) f₁ → IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
⊢ IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂) ↔ IsLocallySurjective J (FA := FA) (CA := CA) f₁

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
h : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₁

Tactic:
isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective J f₁ f₂

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
h : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₁

Tactic:
exact isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective J f₁ f₂

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
h : IsLocallySurjective J (FA := FA) (CA := CA) f₁
⊢ IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F₁ ⟶ F₂
X : C
s : F₂.obj (op X)
hs : Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) s
⊢ imageSieve (FA := TypeCat.Fun) (Subfunctor.toRangeSheafify J f)
      (Subtype.mk (p := fun (x : F₂.obj (op X)) ↦
        Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) x) s hs) ∈
    (J : (a : C) → Set (Sieve a)) X

Tactic:
J.superset_covering ?_ hs

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F₁ ⟶ F₂
X : C
s : F₂.obj (op X)
hs : Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) s
refine :
  (Subfunctor.range f).sieveOfSection s ≤
    imageSieve (FA := TypeCat.Fun) (Subfunctor.toRangeSheafify J f)
      (Subtype.mk (p := fun (x : F₂.obj (op X)) ↦
        Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) x) s hs)
⊢ imageSieve (FA := TypeCat.Fun) (Subfunctor.toRangeSheafify J f)
      (Subtype.mk (p := fun (x : F₂.obj (op X)) ↦
        Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) x) s hs) ∈
    (J : (a : C) → Set (Sieve a)) X

Tactic:
refine J.superset_covering ?_ hs

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F₁ ⟶ F₂
X : C
s : F₂.obj (op X)
hs : Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) s
Y : C
g : Y ⟶ X
t : F₁.obj (op Y)
ht :
  Eq (α := F₂.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
          (a : (fun (X : Type w) ↦ X) (F₁.obj (op Y))) → (fun (X : Type w) ↦ X) (F₂.obj (op Y)))
        t :
      (fun (X : Type w) ↦ X) (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map g.op) :
          (a : (fun (X : Type w) ↦ X) (F₂.obj (op (unop (op X))))) → (fun (X : Type w) ↦ X) (F₂.obj (op Y)))
        s :
      (fun (X : Type w) ↦ X) (F₂.obj (op Y)))
⊢ (imageSieve (FA := TypeCat.Fun) (Subfunctor.toRangeSheafify J f)
        (Subtype.mk (p := fun (x : F₂.obj (op X)) ↦
          Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) x) s
          hs)).arrows
    g

Tactic:
⟨t, Subtype.ext ht⟩

Premises used: Exists.intro, Subtype.ext
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F₁ ⟶ F₂
X : C
s : F₂.obj (op X)
hs : Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) s
Y : C
g : Y ⟶ X
t : F₁.obj (op Y)
ht :
  Eq (α := F₂.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
          (a : (fun (X : Type w) ↦ X) (F₁.obj (op Y))) → (fun (X : Type w) ↦ X) (F₂.obj (op Y)))
        t :
      (fun (X : Type w) ↦ X) (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map g.op) :
          (a : (fun (X : Type w) ↦ X) (F₂.obj (op (unop (op X))))) → (fun (X : Type w) ↦ X) (F₂.obj (op Y)))
        s :
      (fun (X : Type w) ↦ X) (F₂.obj (op Y)))
⊢ (imageSieve (FA := TypeCat.Fun) (Subfunctor.toRangeSheafify J f)
        (Subtype.mk (p := fun (x : F₂.obj (op X)) ↦
          Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) x) s
          hs)).arrows
    g

Tactic:
exact ⟨t, Subtype.ext ht⟩