awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
α' : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
e : α' ≃ α
P :
  EffectiveEpiFamilyStruct.{v_1, u_1, u_3} (C := C) (B := B) (fun (a : α') ↦ X ((e : (a : α') → α) a)) fun (a : α') ↦
    π ((e : (a : α') → α) a)
W : C
x : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
a : α
obtain :
  ∀ (a : α'),
    Eq (α := X ((e : (a : α') → α) a) ⟶ W)
      (π ((e : (a : α') → α) a) ≫ P.desc (fun (x_1 : α') ↦ x ((e : (a : α') → α) x_1)) ⋯) (x ((e : (a : α') → α) a))
⊢ π a ≫ P.desc (fun (x_1 : α') ↦ x ((e : (a : α') → α) x_1)) ⋯ = x a

Tactic:
obtain ⟨a, rfl⟩ := e.surjective a

Premises used: Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
α' : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
e : α' ≃ α
P :
  EffectiveEpiFamilyStruct.{v_1, u_1, u_3} (C := C) (B := B) (fun (a : α') ↦ X ((e : (a : α') → α) a)) fun (a : α') ↦
    π ((e : (a : α') → α) a)
W : C
x : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
a : α'
⊢ Eq (α := X ((e : (a : α') → α) a) ⟶ W)
    (π ((e : (a : α') → α) a) ≫ P.desc (fun (x_1 : α') ↦ x ((e : (a : α') → α) x_1)) ⋯) (x ((e : (a : α') → α) a))

Tactic:
apply P.fac

Premises used: CategoryTheory.EffectiveEpiFamilyStruct.fac
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
α' : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
e : α' ≃ α
h :
  EffectiveEpiFamily.{v_1, u_1, u_3} (C := C) (B := B) (fun (a : α') ↦ X ((e : (a : α') → α) a)) fun (a : α') ↦
    π ((e : (a : α') → α) a)
⊢ EffectiveEpiFamily X π

Tactic:
.mk <| .intro <| @EffectiveEpiFamily.getStruct _ _ _ _ _ _ h |>.reindex _ _ e

Premises used: CategoryTheory.EffectiveEpiFamily.getStruct, Nonempty.intro, CategoryTheory.EffectiveEpiFamily.mk, CategoryTheory.EffectiveEpiFamilyStruct.reindex
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan.{u_2, v_1, u_1} X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
W : C
e : c.pt ⟶ W
h :
  ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt),
    Eq (α := Z ⟶ (Cofan.mk B π).pt) (g₁ ≫ hc.desc (Cofan.mk B π)) (g₂ ≫ hc.desc (Cofan.mk B π)) → g₁ ≫ e = g₂ ≫ e
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
simp : (g₁ ≫ c.ι.app { as := a₁ : Discrete α }) ≫ e = (g₂ ≫ c.ι.app { as := a₂ : Discrete α }) ≫ e
⊢ Eq (α := Z ⟶ W) (g₁ ≫ (fun (a : α) ↦ (c.ι.app { as := a } ≫ e : X a ⟶ W)) a₁)
    (g₂ ≫ (fun (a : α) ↦ (c.ι.app { as := a } ≫ e : X a ⟶ W)) a₂)

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan.{u_2, v_1, u_1} X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
W : C
e : c.pt ⟶ W
h :
  ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt),
    Eq (α := Z ⟶ (Cofan.mk B π).pt) (g₁ ≫ hc.desc (Cofan.mk B π)) (g₂ ≫ hc.desc (Cofan.mk B π)) → g₁ ≫ e = g₂ ≫ e
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ Eq (α := Z ⟶ (Cofan.mk B π).pt) ((g₁ ≫ c.ι.app { as := a₁ : Discrete α }) ≫ hc.desc (Cofan.mk B π))
    ((g₂ ≫ c.ι.app { as := a₂ : Discrete α }) ≫ hc.desc (Cofan.mk B π))

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan.{u_2, v_1, u_1} X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
W : C
e : c.pt ⟶ W
h :
  ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt),
    Eq (α := Z ⟶ (Cofan.mk B π).pt) (g₁ ≫ hc.desc (Cofan.mk B π)) (g₂ ≫ hc.desc (Cofan.mk B π)) → g₁ ≫ e = g₂ ≫ e
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ (g₁ ≫ c.ι.app { as := a₁ : Discrete α }) ≫ e = (g₂ ≫ c.ι.app { as := a₂ : Discrete α }) ≫ e

Tactic:
exact h (g₁ ≫ c.ι.app ⟨a₁⟩) (g₂ ≫ c.ι.app ⟨a₂⟩) (by simpa)

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.Cocone.ι, CategoryTheory.CategoryStruct.comp, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan.{u_2, v_1, u_1} X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
W : C
e : c.pt ⟶ W
h :
  ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt),
    Eq (α := Z ⟶ (Cofan.mk B π).pt) (g₁ ≫ hc.desc (Cofan.mk B π)) (g₂ ≫ hc.desc (Cofan.mk B π)) → g₁ ≫ e = g₂ ≫ e
x : Discrete α
j : α
⊢ Eq (α := Functor.obj.{u_2, v_1, u_2, u_1} (Discrete.functor X) { as := j : Discrete α } ⟶ W)
    (c.ι.app { as := j : Discrete α } ≫
      CategoryStruct.comp (Y := (Cofan.mk B π).pt) (hc.desc (Cofan.mk B π))
        (EffectiveEpiFamily.desc X π (fun (a : α) ↦ c.ι.app { as := a } ≫ e) ⋯))
    (c.ι.app { as := j } ≫ e)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan.{u_2, v_1, u_1} X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
W : C
e : c.pt ⟶ W
h :
  ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt),
    Eq (α := Z ⟶ (Cofan.mk B π).pt) (g₁ ≫ hc.desc (Cofan.mk B π)) (g₂ ≫ hc.desc (Cofan.mk B π)) → g₁ ≫ e = g₂ ≫ e
m : (Cofan.mk B π).pt ⟶ W
hm : hc.desc (Cofan.mk B π) ≫ m = e
Z : C
x x_1 : α
x_2 : Z ⟶ X x
x_3 : Z ⟶ X x_1
hg : x_2 ≫ π x = x_3 ≫ π x_1
⊢ Eq (α := Z ⟶ W) (x_2 ≫ (fun (a : α) ↦ (c.ι.app { as := a } ≫ e : X a ⟶ W)) x)
    (x_3 ≫ (fun (a : α) ↦ (c.ι.app { as := a } ≫ e : X a ⟶ W)) x_1)

Tactic:
simp [← hm, reassoc_of% hg]
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan.{u_2, v_1, u_1} X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
W : C
e : c.pt ⟶ W
h :
  ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt),
    Eq (α := Z ⟶ (Cofan.mk B π).pt) (g₁ ≫ hc.desc (Cofan.mk B π)) (g₂ ≫ hc.desc (Cofan.mk B π)) → g₁ ≫ e = g₂ ≫ e
m : (Cofan.mk B π).pt ⟶ W
hm : hc.desc (Cofan.mk B π) ≫ m = e
x : α
⊢ π x ≫ m = (fun (a : α) ↦ (c.ι.app { as := a } ≫ e : X a ⟶ W)) x

Tactic:
simp [← hm]
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : EffectiveEpiFamily X π
e : EffectiveEpiStruct (Y := (Cofan.mk (sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X)).pt)
  (IsColimit.desc (coproductIsCoproduct X) (Cofan.mk B π)) :=
  effectiveEpiStructIsColimitDescOfEffectiveEpiFamily X (Cofan.mk (sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X))
    (coproductIsCoproduct X) π
simp :
  ∀ (e : EffectiveEpiStruct (Y := sigmaObj.{u_2, v_1, u_1} X) (colimit.desc (Discrete.functor X) (Cofan.mk B π))),
    EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
⊢ EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)

Tactic:
simp only [Cofan.mk_pt, coproductIsCoproduct, colimit.cocone_x, IsColimit.ofIsoColimit_desc,
    Cocone.ext_inv_hom, Iso.refl_inv, colimit.isColimit_desc, Category.id_comp] at e

Premises used: CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Iso.refl_inv, CategoryTheory.Limits.colimit.cocone_x, CategoryTheory.Limits.Cocone.ext_inv_hom, CategoryTheory.Limits.IsColimit.ofIsoColimit_desc, CategoryTheory.Category.id_comp, CategoryTheory.Limits.colimit.isColimit_desc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : EffectiveEpiFamily X π
e : EffectiveEpiStruct (Y := sigmaObj.{u_2, v_1, u_1} X) (colimit.desc (Discrete.functor X) (Cofan.mk B π))
⊢ EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)

Tactic:
⟨⟨e⟩⟩

Premises used: Nonempty.intro, CategoryTheory.EffectiveEpi.mk
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : EffectiveEpiFamily X π
e : EffectiveEpiStruct (Y := sigmaObj.{u_2, v_1, u_1} X) (colimit.desc (Discrete.functor X) (Cofan.mk B π))
⊢ EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)

Tactic:
exact ⟨⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
inst_2 : HasCoproduct.{u_2, v_1, u_1} X
⊢ Epi (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
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 : α
⊢ π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
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 : α
⊢ e a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
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 : α
rw : π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π)
rw₁ :
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π) ≫
      EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ =
    e a
rw₂ :
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π) ≫
      EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
rw₃ :
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a)
      (Sigma.desc π ≫ EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯) =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
rw₄ rw₅ :
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e) =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
⊢ π a ≫ EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ = e a

Tactic:
rw [(by simp : π a = Sigma.ι X a ≫ Sigma.desc π), (by simp : e a = Sigma.ι X a ≫ Sigma.desc e),
      Category.assoc, EffectiveEpi.fac (Sigma.desc π) (Sigma.desc e) (fun g₁ g₂ hg ↦
      effectiveEpiFamilyStructOfEffectiveEpiDesc_aux h hg)]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc_aux, CategoryTheory.Limits.Sigma.desc, CategoryTheory.EffectiveEpi.fac
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
W : C
x : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : B ⟶ W
hm : ∀ (a : α), π a ≫ x_1 = x a
hm₁ : Eq (α := sigmaObj.{u_2, v_1, u_1} X ⟶ W) (Sigma.desc π ≫ x_1) (Sigma.desc x)
⊢ x_1 = EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc x) ⋯

Tactic:
apply EffectiveEpi.uniq (Sigma.desc π)

Premises used: CategoryTheory.EffectiveEpi.uniq, CategoryTheory.Limits.Sigma.desc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
W : C
x : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : B ⟶ W
hm : ∀ (a : α), π a ≫ x_1 = x a
hm₁ :
  ∀ (b : α),
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X b) (Sigma.desc π ≫ x_1) =
      CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X b) (Sigma.desc x)
⊢ Eq (α := sigmaObj.{u_2, v_1, u_1} X ⟶ W) (Sigma.desc π ≫ x_1) (Sigma.desc x)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
W : C
x : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : B ⟶ W
hm : ∀ (a : α), π a ≫ x_1 = x a
b : α
⊢ CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X b) (Sigma.desc π ≫ x_1) =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X b) (Sigma.desc x)

Tactic:
simpa using hm _
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Enough
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.EffectivelyEnough
X : D
⊢ EffectiveEpi (Y := F.effectiveEpiOverObj X) (F.effectiveEpiOver X)

Tactic:
(EffectivelyEnough.presentation X).some.effectiveEpi

Premises used: CategoryTheory.Functor.EffectivelyEnough.presentation, CategoryTheory.Functor.EffectivePresentation.effectiveEpi, CategoryTheory.Functor.effectiveEpiOverObj, Nonempty.some, CategoryTheory.Functor.effectiveEpiOver
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
α : Type
inst_2 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
⊢ EffectiveEpi (Y := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π) ↔ EffectiveEpiFamily X π

Tactic:
⟨fun h ↦ ⟨⟨@effectiveEpiFamilyStructOfEffectiveEpiDesc _ _ _ _ X π _ h _ _ (fun g ↦
    (FinitaryPreExtensive.isIso_sigmaDesc_fst (fun a ↦ Sigma.ι X a) g inferInstance).epi_of_iso)⟩⟩,
    fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc, inferInstance, Nonempty.intro, CategoryTheory.EffectiveEpiFamily.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
α : Type
inst_2 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
⊢ EffectiveEpi (Y := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π) ↔ EffectiveEpiFamily X π

Tactic:
exact ⟨fun h ↦ ⟨⟨@effectiveEpiFamilyStructOfEffectiveEpiDesc _ _ _ _ X π _ h _ _ (fun g ↦
    (FinitaryPreExtensive.isIso_sigmaDesc_fst (fun a ↦ Sigma.ι X a) g inferInstance).epi_of_iso)⟩⟩,
    fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : FinitaryPreExtensive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : PreservesFiniteCoproducts F
inst_5 : F.ReflectsEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
simp : EffectiveEpi (Y := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)
⊢ EffectiveEpiFamily X π

Tactic:
simp only [← effectiveEpi_desc_iff_effectiveEpiFamily]

Premises used: CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : FinitaryPreExtensive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : PreservesFiniteCoproducts F
inst_5 : F.ReflectsEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
h₁ : EffectiveEpi (Y := F.obj (sigmaObj.{0, v_1, u_1} X)) (F.map (Sigma.desc π))
⊢ EffectiveEpi (Y := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)

Tactic:
apply F.effectiveEpi_of_map

Premises used: CategoryTheory.Functor.effectiveEpi_of_map
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : FinitaryPreExtensive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : PreservesFiniteCoproducts F
inst_5 : F.ReflectsEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
⊢ EffectiveEpi (X := F.obj B) (Y := F.obj (sigmaObj.{0, v_1, u_1} X))
    (CategoryStruct.comp (Y := sigmaObj.{0, v_2, u_2} fun (b : α) ↦ F.obj (X b)) (inv (sigmaComparison F X))
      (Sigma.desc fun (a : α) ↦ F.map (π a)))

Tactic:
(inferInstance :
        EffectiveEpi (inv (sigmaComparison F X) ≫ (Sigma.desc (fun a ↦ F.map (π a)))))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : FinitaryPreExtensive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : PreservesFiniteCoproducts F
inst_5 : F.ReflectsEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
h₁ :
  Eq (α := F.obj (sigmaObj.{0, v_1, u_1} X) ⟶ F.obj B) (F.map (Sigma.desc π))
    (CategoryStruct.comp (Y := sigmaObj.{0, v_2, u_2} fun (b : α) ↦ F.obj (X b)) (inv (sigmaComparison F X))
      (Sigma.desc fun (a : α) ↦ F.map (π a)))
⊢ EffectiveEpi (Y := F.obj (sigmaObj.{0, v_1, u_1} X)) (F.map (Sigma.desc π))

Tactic:
convert!
      (inferInstance :
        EffectiveEpi (inv (sigmaComparison F X) ≫ (Sigma.desc (fun a ↦ F.map (π a)))))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : FinitaryPreExtensive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : PreservesFiniteCoproducts F
inst_5 : F.ReflectsEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
⊢ Eq (α := F.obj (sigmaObj.{0, v_1, u_1} X) ⟶ F.obj B) (F.map (Sigma.desc π))
    (CategoryStruct.comp (Y := sigmaObj.{0, v_2, u_2} fun (b : α) ↦ F.obj (X b)) (inv (sigmaComparison F X))
      (Sigma.desc fun (a : α) ↦ F.map (π a)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : FinitaryPreExtensive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : PreservesFiniteCoproducts F
inst_5 : F.PreservesEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
simp :
  EffectiveEpi.{v_2, u_2} (C := D) (X := F.obj B) (Y := sigmaObj.{0, v_2, u_2} fun (a : α) ↦ F.obj (X a))
    (Sigma.desc fun (a : α) ↦ F.map (π a))
⊢ EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)

Tactic:
simp only [← effectiveEpi_desc_iff_effectiveEpiFamily]

Premises used: CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : FinitaryPreExtensive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : PreservesFiniteCoproducts F
inst_5 : F.PreservesEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
⊢ EffectiveEpi (Y := sigmaObj.{0, v_2, u_2} fun (b : α) ↦ F.obj (X b))
    (CategoryStruct.comp (Y := F.obj (sigmaObj.{0, v_1, u_1} X)) (sigmaComparison F X) (F.map (Sigma.desc π)))

Tactic:
(inferInstance : EffectiveEpi ((sigmaComparison F X) ≫ (F.map (Sigma.desc π))))

Premises used: inferInstance