-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem Obj.map_on_summand {Δ Δ' : SimplexCategoryᵒᵖ} (A : Splitting.IndexSet Δ) (θ : Δ ⟶ Δ')
    {Δ'' : SimplexCategory} {e : Δ'.unop ⟶ Δ''} {i : Δ'' ⟶ A.1.unop} [Epi e] [Mono i]
    (fac : e ≫ i = θ.unop ≫ A.e) :
    ((Γ₀.splitting K).cofan Δ).inj A ≫ (Γ₀.obj K).map θ =
      Γ₀.Obj.Termwise.mapMono K i ≫ ((Γ₀.splitting K).cofan Δ').inj (Splitting.IndexSet.mk e)

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ e ≫ 𝟙 Δ'' = e.op.unop ≫ 𝟙 (unop (op Δ''))

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Sigma.ι (summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ map K (A.e.op ≫ θ) =
    Termwise.mapMono K i ≫
      Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op

Tactic:
rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id A.1)
  (show e ≫ i = ((Splitting.IndexSet.e A).op ≫ θ).unop ≫ 𝟙 _ by rw [comp_id, fac]; rfl)]

Result:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e) =
    Termwise.mapMono K i ≫
      Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') ⟨op Δ'', ⟨e, ⋯⟩⟩ =
    Termwise.mapMono K i ≫ 𝟙 (K.X Δ''.len) ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)

Tactic:
rw [id_comp]

Result:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') ⟨op Δ'', ⟨e, ⋯⟩⟩ =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ ((splitting K).ι (unop A.fst).len ≫ map K A.e.op) ≫ map K θ =
    Termwise.mapMono K i ≫ (splitting K).ι Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op

Tactic:
change (_ ≫ (Γ₀.obj K).map A.e.op) ≫ (Γ₀.obj K).map θ = _

Result:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ ((splitting K).ι (unop A.fst).len ≫ (obj K).map A.e.op) ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ (splitting K).ι Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ ((splitting K).ι (unop A.fst).len ≫ (obj K).map A.e.op) ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ (splitting K).ι Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op

Tactic:
rw [assoc, ← Functor.map_comp]

Result:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ (splitting K).ι (unop A.fst).len ≫ (obj K).map (A.e.op ≫ θ) =
    Termwise.mapMono K i ≫ (splitting K).ι Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') ⟨op Δ'', ⟨e, ⋯⟩⟩ =
    Termwise.mapMono K i ≫ Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K e.op

Tactic:
rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id (op Δ''))
    (show e ≫ 𝟙 Δ'' = e.op.unop ≫ 𝟙 _ by simp), Termwise.mapMono_id]

Result:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') ⟨op Δ'', ⟨e, ⋯⟩⟩ =
    Termwise.mapMono K i ≫ 𝟙 (K.X Δ''.len) ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ e ≫ i = (A.e.op ≫ θ).unop ≫ 𝟙 (unop (op (unop A.fst)))

Tactic:
rw [comp_id, fac]

Result:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ θ.unop ≫ A.e = (A.e.op ≫ θ).unop

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ (splitting K).ι (unop A.fst).len ≫ (obj K).map (A.e.op ≫ θ) =
    Termwise.mapMono K i ≫ (splitting K).ι Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op

Tactic:
dsimp [splitting]

Result:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Sigma.ι (summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ map K (A.e.op ≫ θ) =
    Termwise.mapMono K i ≫
      Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op