awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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₂
a : α
h1 : ∃ (a_1 : α) (g : X a ⟶ X a_1), g ≫ π a_1 = π a
h2 :
  ∃ (g : X a ⟶ X (h1.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a))),
    g ≫ π (h1.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a)) = π a
⊢ h2.choose (p := fun (g : X a ⟶ X (h1.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a))) ↦
        g ≫ π (h1.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a)) = π a) ≫
      π (h1.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a)) =
    𝟙 (X a) ≫ π a
have a₁ : π a = 𝟙 (X a) ≫ π a
Tactic: rw [h2.choose_spec, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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₂
a : α
h1 : ∃ (a_1 : α) (g : X a ⟶ X a_1), g ≫ π a_1 = π a
h2 :
  ∃ (g : X a ⟶ X (h1.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a))),
    g ≫ π (h1.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a)) = π a
a₁ : π a = 𝟙 (X a) ≫ π a
⊢ h2.choose (p := fun (g : X a ⟶ X (h1.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a))) ↦
        g ≫ π (h1.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a)) = π a) ≫
      π (h1.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a)) =
    𝟙 (X a) ≫ π a
have a₂ : π a = π a
Tactic: rw [h2.choose_spec, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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
⊢ m = H.desc (aux e ⋯)
have x : ∀ (j : (Sieve.generateFamily X π).arrows.category),
  (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = (aux e sorry).ι.app j
Tactic: apply H.uniq (aux e h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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
⊢ 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 ⋯))
have x : T.hom ≫ m =
  (aux e sorry).ι.app
    (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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
⊢ T.hom ≫ m =
    (aux e ⋯).ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T ⋯)
have x : g ≫ e a =
  (aux e sorry).ι.app
    (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T sorry)
Tactic: simp only [← ha, Category.assoc, hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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
⊢ g ≫ e a =
    (aux e ⋯).ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T ⋯)
have x : g ≫ π a =
  CategoryStruct.comp (Y := X (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) sorry))
    (Exists.choose (p :=
      fun (g_1 : T.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) sorry)) ↦
      g_1 ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) sorry) = T.hom) sorry)
    (π (Exists.choose (p := fun (a : α) ↦ ∃ (g : T.left ⟶ X a), g ≫ π a = T.hom) sorry))
Tactic: apply h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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
⊢ 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) ⋯))
have 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))
Tactic: generalize_proofs h1 h2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ (Presieve.ofArrows X π).EffectiveEpimorphic ↔ EffectiveEpiFamily X π
have mp : (Presieve.ofArrows X π).EffectiveEpimorphic → EffectiveEpiFamily X π
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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 π
⊢ (Presieve.ofArrows X π).EffectiveEpimorphic ↔ EffectiveEpiFamily X π
have mpr : EffectiveEpiFamily X π → (Presieve.ofArrows X π).EffectiveEpimorphic
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (hypothesis)
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)
⊢ EffectiveEpiFamily X π
have h₁ : Nonempty (IsColimit (generateFamily X π).arrows.cocone)
Tactic: rw [Sieve.generateFamily_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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)
⊢ EffectiveEpiFamily X π
have mp : Nonempty (EffectiveEpiFamilyStruct X π)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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 (generate (Presieve.ofArrows X π)).arrows.cocone)
have mpr : Nonempty (IsColimit (generateFamily X π).arrows.cocone)
Tactic: rw [Sieve.generateFamily_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EpiMono (goal)
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)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
⊢ IsLocallySurjective (FA := FA) (CA := CA) φ ↔ Epi φ
have mp : IsLocallySurjective (FA := FA) (CA := CA) φ → Epi φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EpiMono (goal)
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)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
mp : IsLocallySurjective (FA := FA) (CA := CA) φ → Epi φ
⊢ IsLocallySurjective (FA := FA) (CA := CA) φ ↔ Epi φ
have mpr : Epi φ → IsLocallySurjective (FA := FA) (CA := CA) φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EpiMono (hypothesis)
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)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
h : Epi φ
data : MorphismProperty.MapFactorizationData (locallySurjective J A (FA := FA) (CA := CA))
  (locallyInjective J A (FA := FA) (CA := CA)) φ :=
  MorphismProperty.factorizationData (locallySurjective J A (FA := FA) (CA := CA))
    (locallyInjective J A (FA := FA) (CA := CA)) φ
⊢ IsLocallySurjective (FA := FA) (CA := CA) φ
have this : IsLocallySurjective (FA := FA) (CA := CA)
  (data.i (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
Tactic: have : IsLocallySurjective data.i := data.hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EpiMono (hypothesis)
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)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
h : Epi φ
data : MorphismProperty.MapFactorizationData (locallySurjective J A (FA := FA) (CA := CA))
  (locallyInjective J A (FA := FA) (CA := CA)) φ :=
  MorphismProperty.factorizationData (locallySurjective J A (FA := FA) (CA := CA))
    (locallyInjective J A (FA := FA) (CA := CA)) φ
this :
  IsLocallySurjective (FA := FA) (CA := CA)
    (data.i (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
⊢ IsLocallySurjective (FA := FA) (CA := CA) φ
have this₁ : IsLocallyInjective (FD := FA) (CD := CA)
  (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
Tactic: have : IsLocallyInjective data.p := data.hp