CategoryTheory.effectiveEpiFamilyStructCompIso_aux

theorem CategoryTheory.effectiveEpiFamilyStructCompIso_aux : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {B B' : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) (i : B ⟶ B') {W : C} (e : (a : α) → X a ⟶ W), (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp (π a₁) i) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.comp (π a₂) i) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) → ∀ {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₂)

This theorem, `CategoryTheory.effectiveEpiFamilyStructCompIso_aux`, is a statement about morphism composition in a category theory context. Specifically, it states that for any category `C` with objects `B`, `B'`, `W`, and `X(a)` (for any `a` in type `α`), given morphisms `π(a): X(a) ⟶ B`, `i: B ⟶ B'`, and `e(a): X(a) ⟶ W`, if for all other objects `Z` and any two elements `a₁`, `a₂` in type `α` and morphisms `g₁: Z ⟶ X(a₁)`, `g₂: Z ⟶ X(a₂)`, the composition `g₁ ≫ (π(a₁) ≫ i)` is equal to the composition `g₂ ≫ (π(a₂) ≫ i)` implies that the composition `g₁ ≫ e(a₁)` is equal to the composition `g₂ ≫ e(a₂)`, then it follows that if `g₁ ≫ π(a₁)` is equal to `g₂ ≫ π(a₂)`, then `g₁ ≫ e(a₁)` is also equal to `g₂ ≫ e(a₂)`. In short, it's a statement about the preservation of equality between certain compositions of morphisms.

More concisely: If for all objects `Z` and morphisms `g₁, g₂: Z ⟶ X(a)` in a category `C` with objects `B`, `B'`, `W`, and `X(a)`, the equalities `g₁ ≫ π(a₁) = g₂ ≫ π(a₂)` and `g₁ ≫ (π(a₁) ≫ i) = g₂ ≫ (π(a₂) ≫ i)` imply `g₁ ≫ e(a₁) = g₂ ≫ e(a₂)`, then `π` preserves equalities between morphisms `e(a)`.