CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc_aux

theorem CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc_aux : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} {X : α → C} {π : (a : α) → X a ⟶ B} [inst_1 : CategoryTheory.Limits.HasCoproduct X] [inst_2 : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), CategoryTheory.Limits.HasPullback g (CategoryTheory.Limits.Sigma.ι X a)] [inst_3 : ∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Limits.HasCoproduct fun a => CategoryTheory.Limits.pullback g (CategoryTheory.Limits.Sigma.ι X a)] [inst_4 : ∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc fun a => CategoryTheory.Limits.pullback.fst)] {W : C} {e : (a : α) → X a ⟶ W}, (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) → ∀ {Z : C} {g₁ g₂ : Z ⟶ ∐ fun b => X b}, CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Sigma.desc π) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Sigma.desc π) → CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Sigma.desc e) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Sigma.desc e)

This is a lemma in category theory, specifically dealing with coproducts and pullbacks. Given a category `C`, an object `B` in `C`, a type `α` and a function `X` from `α` to objects in `C`, and a family of morphisms `π` from `X a` to `B` for each `a` in `α`. Assuming `X` has a coproduct, and for each `Z` in `C` and each `a` in `α`, there is a pullback of `Z ⟶ ∐ X` and `X a ⟶ ∐ X`. Also, assuming that these pullbacks themselves have coproducts, and that these coproducts are epi. Given another family of morphisms `e` from `X a` to some object `W` in `C`, if for every `Z` in `C`, `a₁` and `a₂` in `α`, and morphisms `g₁` and `g₂` from `Z` to `X a₁` and `X a₂` respectively, the composition of `g₁` with `π a₁` equals the composition of `g₂` with `π a₂` implies that the composition of `g₁` with `e a₁` equals the composition of `g₂` with `e a₂`, then for every `Z` in `C` and morphisms `g₁` and `g₂` from `Z` to the coproduct of `X`, the composition of `g₁` with the descent of `π` equals the composition of `g₂` with the descent of `π` implies that the composition of `g₁` with the descent of `e` equals the composition of `g₂` with the descent of `e`.

More concisely: Given a category `C`, an object `B`, a functor `X : α → Obj C`, a family of morphisms `π : ∏ a, X a → B`, a coproduct `⊕ X` of `X`, and a family of morphisms `e : ∏ a, X a → W`, if for all `Z`, `a₁`, `a₂`, `g₁`, `g₂`, and `π`, `π a₁ ∘ g₁ = π a₂ ∘ g₂` implies `e a₁ ∘ g₁ = e a₂ ∘ g₂`, then `g₁ ∘ Desc π = g₂ ∘ Desc π` implies `g₁ ∘ Desc e = g₂ ∘ Desc e` for all `Z` and morphisms `g₁` and `g₂` from `Z` to `⊕ X`.