awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W : C} (e : (a : α) → X a ⟶ W)
      (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateFamily X π).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateFamily X π).arrows.category) →
                (Sieve.generateFamily X π).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } =>
              ⋯.choose (p :=
                  fun
                    (g :
                      obj.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT)) ↦
                  g ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT) = obj.hom) ≫
                e (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT),
          naturality := ⋯ :
          NatTrans (Sieve.generateFamily X π).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
T : Over.{v, u} B
a : α
g : T.left ⟶ X a
ha : g ≫ π a = T.hom
x :
  T.hom ≫ m =
    (aux e ⋯).ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T ⋯)
⊢ Eq (α :=
    (Sieve.generateFamily X π).arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T
          ⋯) ⟶
      (aux e ⋯).pt)
    ((Sieve.generateFamily X π).arrows.cocone.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T
          ⋯) ≫
      m)
    ((aux e ⋯).ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T ⋯))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W : C} (e : (a : α) → X a ⟶ W)
      (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateFamily X π).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateFamily X π).arrows.category) →
                (Sieve.generateFamily X π).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } =>
              ⋯.choose (p :=
                  fun
                    (g :
                      obj.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT)) ↦
                  g ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT) = obj.hom) ≫
                e (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT),
          naturality := ⋯ :
          NatTrans (Sieve.generateFamily X π).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
T : Over.{v, u} B
a : α
g : T.left ⟶ X a
ha : g ≫ π a = T.hom
x :
  g ≫ e a =
    (aux e ⋯).ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T ⋯)
⊢ T.hom ≫ m =
    (aux e ⋯).ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T ⋯)

Tactic:
simp only [← ha, Category.assoc, hm]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W : C} (e : (a : α) → X a ⟶ W)
      (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateFamily X π).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateFamily X π).arrows.category) →
                (Sieve.generateFamily X π).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } =>
              ⋯.choose (p :=
                  fun
                    (g :
                      obj.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT)) ↦
                  g ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT) = obj.hom) ≫
                e (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT),
          naturality := ⋯ :
          NatTrans (Sieve.generateFamily X π).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
T : Over.{v, u} B
a : α
g : T.left ⟶ X a
ha : g ≫ π a = T.hom
x :
  g ≫ π a =
    CategoryStruct.comp (Y := X (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) ⋯))
      (Exists.choose (p :=
        fun (g_1 : T.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) ⋯)) ↦
        g_1 ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) ⋯) = T.hom) ⋯)
      (π (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) ⋯))
⊢ g ≫ e a =
    (aux e ⋯).ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T ⋯)

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W : C} (e : (a : α) → X a ⟶ W)
      (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateFamily X π).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateFamily X π).arrows.category) →
                (Sieve.generateFamily X π).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } =>
              ⋯.choose (p :=
                  fun
                    (g :
                      obj.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT)) ↦
                  g ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT) = obj.hom) ≫
                e (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT),
          naturality := ⋯ :
          NatTrans (Sieve.generateFamily X π).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
T : Over.{v, u} B
a : α
g : T.left ⟶ X a
ha : g ≫ π a = T.hom
x :
  ∀ (h1 : ∃ (a : α) (g : T.left ⟶ X a), g ≫ π a = T.hom)
    (h2 :
      ∃ (g : T.left ⟶ X (h1.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom))),
        g ≫ π (h1.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom)) = T.hom),
    g ≫ π a =
      h2.choose (p := fun (g : T.left ⟶ X (h1.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom))) ↦
          g ≫ π (h1.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom)) = T.hom) ≫
        π (h1.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom))
⊢ g ≫ π a =
    CategoryStruct.comp (Y := X (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) ⋯))
      (Exists.choose (p :=
        fun (g_1 : T.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) ⋯)) ↦
        g_1 ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) ⋯) = T.hom) ⋯)
      (π (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) ⋯))

Tactic:
generalize_proofs h1 h2
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W : C} (e : (a : α) → X a ⟶ W)
      (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateFamily X π).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateFamily X π).arrows.category) →
                (Sieve.generateFamily X π).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } =>
              ⋯.choose (p :=
                  fun
                    (g :
                      obj.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT)) ↦
                  g ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT) = obj.hom) ≫
                e (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT),
          naturality := ⋯ :
          NatTrans (Sieve.generateFamily X π).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
T : Over.{v, u} B
a : α
g : T.left ⟶ X a
ha : g ≫ π a = T.hom
h1 : ∃ (a : α) (g : T.left ⟶ X a), g ≫ π a = T.hom
h2 :
  ∃ (g : T.left ⟶ X (h1.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom))),
    g ≫ π (h1.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom)) = T.hom
x x₁ x₂ x₃ : g ≫ π a = T.hom
⊢ g ≫ π a =
    h2.choose (p := fun (g : T.left ⟶ X (h1.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom))) ↦
        g ≫ π (h1.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom)) = T.hom) ≫
      π (h1.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom))

Tactic:
rwa [h2.choose_spec]

Premises used: Exists.choose_spec
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
mp : (Presieve.ofArrows X π).EffectiveEpimorphic → EffectiveEpiFamily X π
mpr : EffectiveEpiFamily X π → (Presieve.ofArrows X π).EffectiveEpimorphic
⊢ (Presieve.ofArrows X π).EffectiveEpimorphic ↔ EffectiveEpiFamily X π

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (IsColimit (generate (Presieve.ofArrows X π)).arrows.cocone)
⊢ Nonempty (IsColimit (generateFamily X π).arrows.cocone)

Tactic:
rw [Sieve.generateFamily_eq] at h

Premises used: CategoryTheory.Sieve.generateFamily_eq
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (IsColimit (generateFamily X π).arrows.cocone)
mp : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ EffectiveEpiFamily X π

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (IsColimit (generateFamily X π).arrows.cocone)
⊢ Nonempty (EffectiveEpiFamilyStruct X π)

Tactic:
apply Nonempty.map (effectiveEpiFamilyStructOfIsColimit _ _) h

Premises used: CategoryTheory.effectiveEpiFamilyStructOfIsColimit, Nonempty.map
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
mpr : Nonempty (IsColimit (generateFamily X π).arrows.cocone)
⊢ Nonempty (IsColimit (generate (Presieve.ofArrows X π)).arrows.cocone)

Tactic:
rw [Sieve.generateFamily_eq]

Premises used: CategoryTheory.Sieve.generateFamily_eq
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Nonempty (IsColimit (generateFamily X π).arrows.cocone)

Tactic:
apply Nonempty.map (isColimitOfEffectiveEpiFamilyStruct _ _) h

Premises used: CategoryTheory.isColimitOfEffectiveEpiFamilyStruct, Nonempty.map
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
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 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
data : FunctorialSurjectiveInjectiveFactorizationData.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_6 : HasWeakSheafify.{v, v', u, u'} J A
f : Arrow (Sheaf.{v, v', u, u'} J A)
⊢ Eq (α := obj (presheafToSheaf J A) (f.left.obj (P := Presheaf.IsSheaf J)) ⟶ f.right)
    (map (presheafToSheaf J A) (Arrow.mk f.hom.hom).hom ≫
      NatTrans.app (Adjunction.counit (sheafificationAdjunction J A)) f.right)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J A)) f.left ≫ f.hom)

Tactic:
(sheafificationAdjunction J A).counit.naturality f.hom

Premises used: CategoryTheory.Arrow.hom, CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
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 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
data : FunctorialSurjectiveInjectiveFactorizationData.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_6 : HasWeakSheafify.{v, v', u, u'} J A
f : Arrow (Sheaf.{v, v', u, u'} J A)
⊢ Eq (α := obj (presheafToSheaf J A) (f.left.obj (P := Presheaf.IsSheaf J)) ⟶ f.right)
    (map (presheafToSheaf J A) (Arrow.mk f.hom.hom).hom ≫
      NatTrans.app (Adjunction.counit (sheafificationAdjunction J A)) f.right)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J A)) f.left ≫ f.hom)

Tactic:
exact (sheafificationAdjunction J A).counit.naturality f.hom

Premises used: CategoryTheory.Arrow.hom, CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
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 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
data : FunctorialSurjectiveInjectiveFactorizationData.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_6 : HasWeakSheafify.{v, v', u, u'} J A
x : Arrow (Sheaf.{v, v', u, u'} J A)
⊢ ∀ (U : Cᵒᵖ),
    Function.Surjective.{w + 1, w + 1} (α := CA (x.left.obj (P := Presheaf.IsSheaf J).obj U)) (β :=
      CA
        ((obj
              (MorphismProperty.FunctorialFactorizationData.Z (W₁ :=
                MorphismProperty.functorCategory (MorphismProperty.surjective A (FC := FA) (CC := CA)) Cᵒᵖ) (W₂ :=
                MorphismProperty.functorCategory (MorphismProperty.injective A (FC := FA) (CC := CA)) Cᵒᵖ)
                (MorphismProperty.FunctorialFactorizationData.functorCategory (W₁ :=
                  MorphismProperty.surjective A (FC := FA) (CC := CA)) (W₂ :=
                  MorphismProperty.injective A (FC := FA) (CC := CA)) data Cᵒᵖ))
              (Arrow.mk x.hom.hom)).obj
          U))
      (⇑(ConcreteCategory.hom (FC := FA) (CC := CA)
            (NatTrans.app
              (NatTrans.app
                (MorphismProperty.FunctorialFactorizationData.i (W₁ :=
                  MorphismProperty.functorCategory (MorphismProperty.surjective A (FC := FA) (CC := CA)) Cᵒᵖ) (W₂ :=
                  MorphismProperty.functorCategory (MorphismProperty.injective A (FC := FA) (CC := CA)) Cᵒᵖ)
                  (MorphismProperty.FunctorialFactorizationData.functorCategory (W₁ :=
                    MorphismProperty.surjective A (FC := FA) (CC := CA)) (W₂ :=
                    MorphismProperty.injective A (FC := FA) (CC := CA)) data Cᵒᵖ))
                (Arrow.mk x.hom.hom))
              U)) :
        (a : CA (x.left.obj.obj U)) →
          CA
            (((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).Z.obj (Arrow.mk x.hom.hom)).obj
              U))

Tactic:
apply (data.functorCategory Cᵒᵖ).hi

Premises used: CategoryTheory.MorphismProperty.FunctorialFactorizationData.hi, Opposite, CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
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 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
data : FunctorialSurjectiveInjectiveFactorizationData.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_6 : HasWeakSheafify.{v, v', u, u'} J A
x : Arrow (Sheaf.{v, v', u, u'} J A)
⊢ ∀ (X : Cᵒᵖ),
    Function.Injective.{w + 1, w + 1} (α :=
      CA
        ((obj
              (MorphismProperty.FunctorialFactorizationData.Z (W₁ :=
                MorphismProperty.functorCategory (MorphismProperty.surjective A (FC := FA) (CC := CA)) Cᵒᵖ) (W₂ :=
                MorphismProperty.functorCategory (MorphismProperty.injective A (FC := FA) (CC := CA)) Cᵒᵖ)
                (MorphismProperty.FunctorialFactorizationData.functorCategory (W₁ :=
                  MorphismProperty.surjective A (FC := FA) (CC := CA)) (W₂ :=
                  MorphismProperty.injective A (FC := FA) (CC := CA)) data Cᵒᵖ))
              (Arrow.mk x.hom.hom)).obj
          X))
      (β := CA (x.right.obj (P := Presheaf.IsSheaf J).obj X))
      (⇑(ConcreteCategory.hom (FC := FA) (CC := CA)
            (NatTrans.app
              (NatTrans.app
                (MorphismProperty.FunctorialFactorizationData.p (W₁ :=
                  MorphismProperty.functorCategory (MorphismProperty.surjective A (FC := FA) (CC := CA)) Cᵒᵖ) (W₂ :=
                  MorphismProperty.functorCategory (MorphismProperty.injective A (FC := FA) (CC := CA)) Cᵒᵖ)
                  (MorphismProperty.FunctorialFactorizationData.functorCategory (W₁ :=
                    MorphismProperty.surjective A (FC := FA) (CC := CA)) (W₂ :=
                    MorphismProperty.injective A (FC := FA) (CC := CA)) data Cᵒᵖ))
                (Arrow.mk x.hom.hom))
              X)) :
        (a :
            CA
              (((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).Z.obj (Arrow.mk x.hom.hom)).obj
                X)) →
          CA (x.right.obj.obj X))

Tactic:
apply (data.functorCategory Cᵒᵖ).hp

Premises used: Opposite, CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory, CategoryTheory.MorphismProperty.FunctorialFactorizationData.hp
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
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 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
data : FunctorialSurjectiveInjectiveFactorizationData.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_6 : HasWeakSheafify.{v, v', u, u'} J A
f : Arrow (Sheaf.{v, v', u, u'} J A)
⊢ IsLocallySurjective (FA := FA) (CA := CA)
    ((functorialLocallySurjectiveInjectiveFactorization J (FA := FA) (CA := CA) data).i (W₁ :=
          locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)).app
      f)

Tactic:
apply (functorialLocallySurjectiveInjectiveFactorization J data).hi

Premises used: CategoryTheory.MorphismProperty.FunctorialFactorizationData.hi, CategoryTheory.Sheaf.functorialLocallySurjectiveInjectiveFactorization