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₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
V W : C
i : V ⟶ W
j : W ⟶ U
H : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows j
t' : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₁.obj (op V))
ht' :
  Eq (α := CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₂.obj (op V))) t' :
      CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map i.op) : (a : CA (F₂.obj (op W))) → CA (F₂.obj (op V)))
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op W))) ↦
          Eq (α := CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op W)) :
                  (a : CA (F₂.obj (op W))) → CA (F₃.obj (op W)))
                t :
              CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map j.op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op W)))
                s :
              CA (F₃.obj (op W))))
          H) :
      CA (F₂.obj (op V)))
⊢ (imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s).arrows (i ≫ j)

Tactic:
⟨t', ?_⟩

Premises used: Exists.intro
-- 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₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
V W : C
i : V ⟶ W
j : W ⟶ U
H : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows j
t' : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₁.obj (op V))
ht' :
  Eq (α := CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₂.obj (op V))) t' :
      CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map i.op) : (a : CA (F₂.obj (op W))) → CA (F₂.obj (op V)))
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op W))) ↦
          Eq (α := CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op W)) :
                  (a : CA (F₂.obj (op W))) → CA (F₃.obj (op W)))
                t :
              CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map j.op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op W)))
                s :
              CA (F₃.obj (op W))))
          H) :
      CA (F₂.obj (op V)))
refine :
  Eq (α := CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₃.obj (op V)))
        t' :
      CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map (i ≫ j).op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V)))
        s :
      CA (F₃.obj (op V)))
⊢ (imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s).arrows (i ≫ j)

Tactic:
refine ⟨t', ?_⟩
-- 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₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
⊢ (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ≤
    imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s

Tactic:
have : (Sieve.bind (imageSieve f₂ s) fun _ _ h => imageSieve f₁ h.choose) ≤
        imageSieve (f₁ ≫ f₂) s := by
      rintro V i ⟨W, i, j, H, ⟨t', ht'⟩, rfl⟩
      refine ⟨t', ?_⟩
      rw [op_comp, F₃.map_comp, NatTrans.comp_app, ConcreteCategory.comp_apply,
        ConcreteCategory.comp_apply, ht', NatTrans.naturality_apply, H.choose_spec]
-- 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₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
this :
  (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ≤
    imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s
apply :
  (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ∈
    (J : (a : C) → Set (Sieve a)) U
⊢ imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
apply J.superset_covering this

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₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
this :
  (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ≤
    imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s
hS : imageSieve (FA := FA) (CA := CA) f₂ s ∈ (J : (a : C) → Set (Sieve a)) U
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ U⦄ (H : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows f),
    imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op Y))) ↦
          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)))
                t :
              CA (F₃.obj (op Y)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map f.op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op Y)))
                s :
              CA (F₃.obj (op Y))))
          H) ∈
      (J : (a : C) → Set (Sieve a)) Y
⊢ (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ∈
    (J : (a : C) → Set (Sieve a)) U

Tactic:
apply J.bind_covering

Premises used: CategoryTheory.GrothendieckTopology.bind_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₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
this :
  (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ≤
    imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s
⊢ imageSieve (FA := FA) (CA := CA) f₂ s ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
apply imageSieve_mem

Premises used: 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₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
this :
  (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ≤
    imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s
Y : C
f : Y ⟶ U
H : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows f
⊢ imageSieve (FA := FA) (CA := CA) f₁
      (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op Y))) ↦
        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)))
              t :
            CA (F₃.obj (op Y)))
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map f.op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op Y)))
              s :
            CA (F₃.obj (op Y))))
        H) ∈
    (J : (a : C) → Set (Sieve a)) Y

Tactic:
apply imageSieve_mem

Premises used: 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₂)
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op X))
⊢ imageSieve (FA := FA) (CA := CA) f₂ x ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
J.superset_covering ?_ (imageSieve_mem J (f₁ ≫ f₂) x)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.CategoryStruct.comp, 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₂)
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op X))
refine : imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) x ≤ imageSieve (FA := FA) (CA := CA) f₂ x
⊢ imageSieve (FA := FA) (CA := CA) f₂ x ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
refine J.superset_covering ?_ (imageSieve_mem J (f₁ ≫ f₂) x)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.CategoryStruct.comp, 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₂)
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op X))
Y : C
g : Y ⟶ X
hg : (imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) x).arrows g
⊢ 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₂) x g hg) :
          CA (F₂.obj (op Y))) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map g.op) : (a : CA (F₃.obj (op X))) → CA (F₃.obj (op Y))) x :
      CA (F₃.obj (op Y)))

Tactic:
simpa using app_localPreimage (f₁ ≫ f₂) x g hg

Premises used: CategoryTheory.Presheaf.app_localPreimage, CategoryTheory.CategoryStruct.comp
-- 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₂)
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op X))
Y : C
g : Y ⟶ X
hg : (imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) x).arrows g
⊢ (imageSieve (FA := FA) (CA := CA) f₂ x).arrows g

Tactic:
exact ⟨f₁.app _ (localPreimage (f₁ ≫ f₂) x g hg),
      by simpa using app_localPreimage (f₁ ≫ f₂) x g hg⟩
-- 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₃
⊢ 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 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₂

Tactic:
isLocallySurjective_of_isLocallySurjective J f₁ f₂

Premises used: CategoryTheory.Presheaf.isLocallySurjective_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 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₂

Tactic:
exact isLocallySurjective_of_isLocallySurjective J f₁ f₂

Premises used: CategoryTheory.Presheaf.isLocallySurjective_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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
mp : IsLocallySurjective J (FA := FA) (CA := CA) f₃ → IsLocallySurjective J (FA := FA) (CA := CA) f₂
mpr : IsLocallySurjective J (FA := FA) (CA := CA) f₂ → IsLocallySurjective J (FA := FA) (CA := CA) f₃
⊢ IsLocallySurjective J (FA := FA) (CA := CA) 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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
h : IsLocallySurjective J (FA := FA) (CA := CA) f₃
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₂

Tactic:
isLocallySurjective_of_isLocallySurjective_fac J fac

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
h : IsLocallySurjective J (FA := FA) (CA := CA) f₃
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₂

Tactic:
exact isLocallySurjective_of_isLocallySurjective_fac J fac

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
h : IsLocallySurjective J (FA := FA) (CA := CA) f₂
mpr : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₃

Tactic:
rw [← 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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst_4 : 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