-- Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean
theorem preComp_φ : (f.preComp g).φ = g.app (op ⦋n + 1⦌) ≫ f.φ

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ (f.preComp g).φ = g.app (op ⦋n + 1⦌) ≫ f.φ

Tactic:
unfold φ preComp

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ PInfty.f (n + 1) ≫ { a := g.app (op ⦋n + 1⦌) ≫ f.a, b := fun i => g.app (op ⦋n⦌) ≫ f.b i }.a +
      ∑ i : Fin (n + 1),
        (P ↑i).f (n + 1) ≫
          X'.δ i.rev.succ ≫ { a := g.app (op ⦋n + 1⦌) ≫ f.a, b := fun i => g.app (op ⦋n⦌) ≫ f.b i }.b i.rev =
    g.app (op ⦋n + 1⦌) ≫ (PInfty.f (n + 1) ≫ f.a + ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ (P (n + 1)).f (n + 1) ≫ g.app (op ⦋n + 1⦌) ≫ f.a +
      ∑ x : Fin (n + 1), (P ↑x).f (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev =
    g.app (op ⦋n + 1⦌) ≫ (P (n + 1)).f (n + 1) ≫ f.a +
      g.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev

Tactic:
congr 1

Result:
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ (P (n + 1)).f (n + 1) ≫ g.app (op ⦋n + 1⦌) ≫ f.a = g.app (op ⦋n + 1⦌) ≫ (P (n + 1)).f (n + 1) ≫ f.a

case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ ∑ x : Fin (n + 1), (P ↑x).f (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev =
    g.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev

Proof state:
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ (P (n + 1)).f (n + 1) ≫ g.app (op ⦋n + 1⦌) ≫ f.a = g.app (op ⦋n + 1⦌) ≫ (P (n + 1)).f (n + 1) ≫ f.a

Tactic:
simp only [P_f_naturality_assoc]

Result:
no goals

Proof state:
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ ∑ x : Fin (n + 1), (P ↑x).f (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev =
    g.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev

Tactic:
simp only [comp_sum, P_f_naturality_assoc, SimplicialObject.δ_naturality_assoc]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ PInfty.f (n + 1) ≫ { a := g.app (op ⦋n + 1⦌) ≫ f.a, b := fun i => g.app (op ⦋n⦌) ≫ f.b i }.a +
      ∑ i : Fin (n + 1),
        (P ↑i).f (n + 1) ≫
          X'.δ i.rev.succ ≫ { a := g.app (op ⦋n + 1⦌) ≫ f.a, b := fun i => g.app (op ⦋n⦌) ≫ f.b i }.b i.rev =
    g.app (op ⦋n + 1⦌) ≫ (PInfty.f (n + 1) ≫ f.a + ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev)

Tactic:
simp only [PInfty_f, comp_add]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ (P (n + 1)).f (n + 1) ≫ g.app (op ⦋n + 1⦌) ≫ f.a +
      ∑ x : Fin (n + 1), (P ↑x).f (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev =
    g.app (op ⦋n + 1⦌) ≫ (P (n + 1)).f (n + 1) ≫ f.a +
      g.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev