-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem karoubi_PInfty_f {Y : Karoubi (SimplicialObject C)} (n : ℕ) :
    ((PInfty : K[(karoubiFunctorCategoryEmbedding _ _).obj Y] ⟶ _).f n).f =
      Y.p.app (op ⦋n⦌) ≫ (PInfty : K[Y.X] ⟶ _).f n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Tactic:
have h₄₃ : P₄.f n = P₃.f n := by
  have h := Functor.congr_obj (toKaroubi_comp_karoubiFunctorCategoryEmbedding _ _) Y₂
  simp only [P₃, P₄, ← natTransPInfty_f_app]
  congr 1

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n

Tactic:
let Y₃ := ((whiskering _ _).obj (toKaroubi C)).obj Y.X

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n

Tactic:
let P₂ : K[Y₂] ⟶ _ := PInfty

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n

Tactic:
let P₃ : K[Y₃] ⟶ _ := PInfty

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  PInfty.f n =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p
eq : Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f = (PInfty.f n).f ≫ Y.p.app (op ⦋n⦌)
⊢ Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f ≫ Y.p.app (op ⦋n⦌) = Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f

Tactic:
rw [← eq, app_idem_assoc Y (op ⦋n⦌)]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n

Tactic:
let Y₂ := Y.X

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n