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

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
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateSingleton f).arrows.category) →
                (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e,
          naturality := ⋯ :
          NatTrans (Sieve.generateSingleton f).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
m : X ⟶ W
hm : f ≫ m = e
A : Over.{v, u} X
g : A.left ⟶ Y
hA : g ≫ f = A.hom
x : g ≫ f = Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) ⋯ ≫ f
⊢ g ≫ e =
    (aux e ⋯).ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom) A
        ⋯)

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateSingleton f).arrows.category) →
                (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e,
          naturality := ⋯ :
          NatTrans (Sieve.generateSingleton f).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
m : X ⟶ W
hm : f ≫ m = e
A : Over.{v, u} X
g : A.left ⟶ Y
hA : g ≫ f = A.hom
x : ∀ (hh : ∃ (e : A.left ⟶ Y), e ≫ f = A.hom), g ≫ f = hh.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) ≫ f
⊢ g ≫ f = Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) ⋯ ≫ f

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

Tactic:
rwa [hh.choose_spec]

Premises used: Exists.choose_spec
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
mp : (Presieve.singleton f).EffectiveEpimorphic → EffectiveEpi f
mpr : EffectiveEpi f → (Presieve.singleton f).EffectiveEpimorphic
⊢ (Presieve.singleton f).EffectiveEpimorphic ↔ EffectiveEpi f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (generate (Presieve.singleton f)).arrows.cocone)
⊢ Nonempty (IsColimit (generateSingleton f).arrows.cocone)

Tactic:
rw [Sieve.generateSingleton_eq] at h

Premises used: CategoryTheory.Sieve.generateSingleton_eq
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (generateSingleton f).arrows.cocone)
mp : Nonempty (EffectiveEpiStruct f)
⊢ EffectiveEpi f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (generateSingleton f).arrows.cocone)
⊢ Nonempty (EffectiveEpiStruct f)

Tactic:
apply Nonempty.map (effectiveEpiStructOfIsColimit _) h

Premises used: CategoryTheory.effectiveEpiStructOfIsColimit, Nonempty.map
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
mpr : Nonempty (IsColimit (generateSingleton f).arrows.cocone)
⊢ Nonempty (IsColimit (generate (Presieve.singleton f)).arrows.cocone)

Tactic:
rw [Sieve.generateSingleton_eq]

Premises used: CategoryTheory.Sieve.generateSingleton_eq
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (generateSingleton f).arrows.cocone)

Tactic:
apply Nonempty.map (isColimitOfEffectiveEpiStruct _) h

Premises used: CategoryTheory.isColimitOfEffectiveEpiStruct, Nonempty.map
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : EffectiveEpi f
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
inst_2 : F.IsRepresentable
⊢ IsSheafFor F (singleton f)

Tactic:
Presieve.EffectiveEpimorphic.isSheafFor_of_isRepresentable
    ((Sieve.effectiveEpimorphic_singleton f).mpr ‹_›) _

Premises used: Iff.mpr, CategoryTheory.Sieve.effectiveEpimorphic_singleton, CategoryTheory.Presieve.EffectiveEpimorphic.isSheafFor_of_isRepresentable
-- 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
Y₁ Y₂ : C
a : α
q : Y₁ ⟶ X a
e : Y₂ ⟶ Y₁
⊢ (e ≫ q) ≫ π a = e ≫ q ≫ π a

Tactic:
simp
-- 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
Y₁ Y₂ : C
a : α
q : Y₁ ⟶ X a
e : Y₂ ⟶ Y₁
⊢ ∃ (a_1 : α) (g : Y₂ ⟶ X a_1), g ≫ π a_1 = e ≫ q ≫ π a

Tactic:
exact ⟨a, e ≫ q, by simp⟩
-- 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 : ∀ ⦃Y : C⦄ (g : Y ⟶ B), (generate (Presieve.ofArrows X π)).arrows g ↔ (generateFamily X π).arrows g
⊢ generate (Presieve.ofArrows X π) = generateFamily X π

Tactic:
ext Y g
-- 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
Y : C
g : Y ⟶ B
h : (generate (Presieve.ofArrows X π)).arrows g → (generateFamily X π).arrows g
h₁ : (generateFamily X π).arrows g → (generate (Presieve.ofArrows X π)).arrows g
⊢ (generate (Presieve.ofArrows X π)).arrows g ↔ (generateFamily X π).arrows g

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
Y_1 Y : C
a : α
g : Y_1 ⟶ X a
⊢ (generateFamily X π).arrows (g ≫ π a)

Tactic:
⟨a, g, rfl⟩

Premises used: Exists.intro, rfl
-- 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
Y_1 Y : C
a : α
g : Y_1 ⟶ X a
⊢ (generateFamily X π).arrows (g ≫ π a)

Tactic:
exact ⟨a, g, rfl⟩
-- 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
Y : C
a : α
g : Y ⟶ X a
⊢ (generate (Presieve.ofArrows X π)).arrows (g ≫ π a)

Tactic:
⟨_, g, π a, ⟨a⟩, rfl⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, And.intro, Exists.intro, rfl
-- 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
Y : C
a : α
g : Y ⟶ X a
⊢ (generate (Presieve.ofArrows X π)).arrows (g ≫ π a)

Tactic:
exact ⟨_, g, π a, ⟨a⟩, rfl⟩
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
a : α
⊢ 𝟙 (Over.mk (π a)).left ≫ π a = (Over.mk (π a)).hom

Tactic:
simp
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
dsimp :
  Eq (α := Z ⟶ S.pt)
    (g₁ ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a₁)) ⋯))
    (g₂ ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a₂)) ⋯))
⊢ Eq (α := Z ⟶ S.pt)
    (g₁ ≫
      (fun (a : α) ↦
          (S.ι.app
              (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a)) ⋯) :
            (Sieve.generateFamily X π).arrows.diagram.obj
                (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                  (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a)) ⋯) ⟶
              Functor.obj (C := (Sieve.generateFamily X π).arrows.category)
                (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) S.pt)
                (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                  (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a)) ⋯)))
        a₁)
    (g₂ ≫
      (fun (a : α) ↦
          (S.ι.app
              (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a)) ⋯) :
            (Sieve.generateFamily X π).arrows.diagram.obj
                (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                  (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a)) ⋯) ⟶
              Functor.obj (C := (Sieve.generateFamily X π).arrows.category)
                (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) S.pt)
                (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                  (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a)) ⋯)))
        a₂)

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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ 𝟙 (Over.mk (π a₁)).left ≫ π a₁ = (Over.mk (π a₁)).hom

Tactic:
simp
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
A₁ : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (π a₁)) ⋯
⊢ 𝟙 (Over.mk (π a₂)).left ≫ π a₂ = (Over.mk (π a₂)).hom

Tactic:
simp
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
A₁ : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (π a₁)) ⋯
A₂ : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (π a₂)) ⋯
Z' : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (g₁ ≫ π a₁)) ⋯
i₁ : Z' ⟶ A₁ :=
  ObjectProperty.homMk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom) (Over.homMk g₁ ⋯)
i₂ : Z' ⟶ A₂ :=
  ObjectProperty.homMk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom) (Over.homMk g₂ ⋯)
change :
  F.map i₁ ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a₁)) ⋯) =
    F.map i₂ ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a₂)) ⋯)
⊢ Eq (α := Z ⟶ S.pt)
    (g₁ ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a₁)) ⋯))
    (g₂ ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a₂)) ⋯))

Tactic:
change F.map i₁ ≫ _ = F.map i₂ ≫ _

Premises used: CategoryTheory.Functor.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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
A₁ : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (π a₁)) ⋯
A₂ : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (π a₂)) ⋯
Z' : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (g₁ ≫ π a₁)) ⋯
i₁ : Z' ⟶ A₁ :=
  ObjectProperty.homMk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom) (Over.homMk g₁ ⋯)
i₂ : Z' ⟶ A₂ :=
  ObjectProperty.homMk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom) (Over.homMk g₂ ⋯)
⊢ F.map i₁ ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a₁)) ⋯) =
    F.map i₂ ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a₂)) ⋯)

Tactic:
simp only [F, A₁, A₂, S.w]

Premises used: CategoryTheory.Limits.Cocone.w
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
X₁ :
  ∀ (T : Over.{v, u} B) (a : α) (g : T.left ⟶ X a) (hT : g ≫ π a = T.hom),
    Eq (α :=
      (Sieve.generateFamily X π).arrows.diagram.obj
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T
            ⋯) ⟶
        S.pt)
      ((Sieve.generateFamily X π).arrows.cocone.ι.app
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T
            ⋯) ≫
        H.desc
          (fun (a : α) ↦
            S.ι.app
              (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a)) ⋯))
          ⋯)
      (S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T
          ⋯))
⊢ ∀ (j : (Sieve.generateFamily X π).arrows.category),
    (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫
        H.desc
          (fun (a : α) ↦
            S.ι.app
              (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a)) ⋯))
          ⋯ =
      S.ι.app j

Tactic:
⟨T, a, (g : T.left ⟶ X a), hT⟩
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
T : Over.{v, u} B
a : α
g : T.left ⟶ X a
hT : g ≫ π a = T.hom
dsimp :
  T.hom ≫
      H.desc
        (fun (a : α) ↦
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a)) ⋯))
        ⋯ =
    S.ι.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
          ⋯) ⟶
      S.pt)
    ((Sieve.generateFamily X π).arrows.cocone.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T
          ⋯) ≫
      H.desc
        (fun (a : α) ↦
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a)) ⋯))
        ⋯)
    (S.ι.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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
T : Over.{v, u} B
a : α
g : T.left ⟶ X a
hT : g ≫ π a = T.hom
generalize_proofs :
  ∀ (h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom)
    (h₂ :
      ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
        g₁ ≫ π a₁ = g₂ ≫ π a₂ →
          Eq (α := Z ⟶ S.pt)
            (g₁ ≫
              S.ι.app
                (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                  (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a₁)) ⋯))
            (g₂ ≫
              S.ι.app
                (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                  (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a₂)) ⋯)))
    (h₃ : (Sieve.generateFamily X π).arrows T.hom),
    T.hom ≫
        H.desc
          (fun (a : α) ↦
            S.ι.app
              (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a)) ⋯))
          @h₂ =
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T
          h₃)
⊢ T.hom ≫
      H.desc
        (fun (a : α) ↦
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a)) ⋯))
        ⋯ =
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T ⋯)

Tactic:
generalize_proofs h₁ h₂ h₃