C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
⊢ (iso s Δ).hom ≫ f = (iso s Δ).hom ≫ g
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
⊢ f = g
rw [← cancel_epi (s.iso Δ).hom]
case w
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
⊢ ∀ (j : Discrete (IndexSet Δ)),
    colimit.ι (Discrete.functor (summand s.N Δ)) j ≫ (iso s Δ).hom ≫ f =
      colimit.ι (Discrete.functor (summand s.N Δ)) j ≫ (iso s Δ).hom ≫ g
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
⊢ (iso s Δ).hom ≫ f = (iso s Δ).hom ≫ g
apply colimit.hom_ext
case w.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
A : IndexSet Δ
⊢ colimit.ι (Discrete.functor (summand s.N Δ)) { as := A } ≫ (iso s Δ).hom ≫ f =
    colimit.ι (Discrete.functor (summand s.N Δ)) { as := A } ≫ (iso s Δ).hom ≫ g
case w
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
⊢ ∀ (j : Discrete (IndexSet Δ)),
    colimit.ι (Discrete.functor (summand s.N Δ)) j ≫ (iso s Δ).hom ≫ f =
      colimit.ι (Discrete.functor (summand s.N Δ)) j ≫ (iso s Δ).hom ≫ g
rintro ⟨A⟩
no goals
case w.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
A : IndexSet Δ
⊢ colimit.ι (Discrete.functor (summand s.N Δ)) { as := A } ≫ (iso s Δ).hom ≫ f =
    colimit.ι (Discrete.functor (summand s.N Δ)) { as := A } ≫ (iso s Δ).hom ≫ g
simpa only [ιSummand_eq, iso_hom, map, colimit.ι_desc_assoc, Cofan.mk_ι_app] using h A