C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Sigma.ι (summand K Δ) A ≫ map K θ = Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
simp only [map, colimit.ι_desc, Cofan.mk_ι_app]
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
h : image (θ.unop ≫ Splitting.IndexSet.e A) = Δ''
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
have h := SimplexCategory.image_eq fac
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
h : image (θ.unop ≫ Splitting.IndexSet.e A) = Δ''
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
subst h
case e_a.e_i
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ image.ι (θ.unop ≫ Splitting.IndexSet.e A) = i

case e_a.h.e_6.h
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Splitting.IndexSet.pull A θ = Splitting.IndexSet.mk e
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
congr
no goals
case e_a.e_i
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ image.ι (θ.unop ≫ Splitting.IndexSet.e A) = i
exact SimplexCategory.image_ι_eq fac
case e_a.h.e_6.h
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Splitting.IndexSet.mk (factorThruImage (θ.unop ≫ Splitting.IndexSet.e A)) = Splitting.IndexSet.mk e
case e_a.h.e_6.h
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Splitting.IndexSet.pull A θ = Splitting.IndexSet.mk e
dsimp only [SimplicialObject.Splitting.IndexSet.pull]
case e_a.h.e_6.h.e_f
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ factorThruImage (θ.unop ≫ Splitting.IndexSet.e A) = e
case e_a.h.e_6.h
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Splitting.IndexSet.mk (factorThruImage (θ.unop ≫ Splitting.IndexSet.e A)) = Splitting.IndexSet.mk e
congr
no goals
case e_a.h.e_6.h.e_f
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ factorThruImage (θ.unop ≫ Splitting.IndexSet.e A) = e
exact SimplexCategory.factorThruImage_eq fac