awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
hqn : n ≤ q
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f (P (q + 1)) n)
    (HomologicalComplex.Hom.f (P q) n)
have zero : ∀ (hqn : 0 ≤ q),
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (HomologicalComplex.Hom.f (P (q + 1)) 0)
    (HomologicalComplex.Hom.f (P q) 0)
Tactic: cases n with
  | zero => simp only [P_f_0_eq]
  | succ n =>
    simp only [P_succ, comp_add, comp_id, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
      add_eq_left]
    exact (HigherFacesVanish.of_P q n).comp_Hσ_eq_zero (Nat.succ_le_iff.mp hqn)
Cleared hypotheses: n, hqn
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
hqn : n ≤ q
zero :
  ∀ (hqn : 0 ≤ q),
    Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
      (HomologicalComplex.Hom.f (P (q + 1)) 0) (HomologicalComplex.Hom.f (P q) 0)
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f (P (q + 1)) n)
    (HomologicalComplex.Hom.f (P q) n)
have succ : ∀ (n : ℕ) (hqn : n + 1 ≤ q),
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (P (q + 1)) (n + 1)) (HomologicalComplex.Hom.f (P q) (n + 1))
Tactic: cases n with
  | zero => simp only [P_f_0_eq]
  | succ n =>
    simp only [P_succ, comp_add, comp_id, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
      add_eq_left]
    exact (HigherFacesVanish.of_P q n).comp_Hσ_eq_zero (Nat.succ_le_iff.mp hqn)
Cleared hypotheses: n, hqn
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (HomologicalComplex.Hom.f QInfty 0) 0
have dsimp : HSub.hSub (α := X _⦋0⦌ ⟶ X _⦋0⦌) (𝟙 (X _⦋0⦌)) (𝟙 (X _⦋0⦌)) = 0
Tactic: dsimp [QInfty]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (PInfty ≫ PInfty) PInfty
have h : ∀ (n : ℕ),
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f (PInfty ≫ PInfty) n) (HomologicalComplex.Hom.f PInfty n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (QInfty ≫ QInfty) QInfty
have h : ∀ (n : ℕ),
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f (QInfty ≫ QInfty) n) (HomologicalComplex.Hom.f QInfty n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f QInfty n) 0
have dsimp : HomologicalComplex.Hom.f PInfty n ≫
    (HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) PInfty).f n =
  0
Tactic: dsimp only [QInfty]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (PInfty ≫ QInfty) 0
have h : ∀ (n : ℕ),
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f (PInfty ≫ QInfty) n) (HomologicalComplex.Hom.f 0 n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f QInfty n ≫ HomologicalComplex.Hom.f PInfty n) 0
have dsimp : (HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) PInfty).f n ≫
    HomologicalComplex.Hom.f PInfty n =
  0
Tactic: dsimp only [QInfty]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (QInfty ≫ PInfty) 0
have h : ∀ (n : ℕ),
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f (QInfty ≫ PInfty) n) (HomologicalComplex.Hom.f 0 n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) PInfty QInfty = 𝟙 K[X]
have dsimp : PInfty + HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) PInfty = 𝟙 K[X]
Tactic: dsimp only [QInfty]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X_1 X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) X)
      (Functor.obj (alternatingFaceMapComplex C) Y))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ PInfty)
    (PInfty ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
have h : ∀ (n : ℕ),
  Eq (α :=
    HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) n ⟶
      HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) n)
    (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ PInfty) n)
    (HomologicalComplex.Hom.f (PInfty ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
have h₃₂ : (P₃.f n).f = P₂.f n
Tactic: have h₃₂ : (P₃.f n).f = P₂.f n := Karoubi.hom_ext_iff.mp (map_PInfty_f (toKaroubi C) Y₂ n)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
⊢ P₄.f n = P₃.f n
have h : Functor.obj
    (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⋙
      karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    Y₂ =
  Functor.obj (Functor.obj (Functor.whiskeringRight SimplexCategoryᵒᵖ C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y₂
Tactic: have h := Functor.congr_obj (toKaroubi_comp_karoubiFunctorCategoryEmbedding _ _) Y₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h :
  Functor.obj
      (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⋙
        karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
      Y₂ =
    Functor.obj (Functor.obj (Functor.whiskeringRight SimplexCategoryᵒᵖ C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y₂
⊢ P₄.f n = P₃.f n
have simp : Eq (α := HomologicalComplex.X K[Y₄] n ⟶ HomologicalComplex.X K[Y₄] n)
  (NatTrans.app (natTransPInfty_f (Karoubi.{v_1, u_1} C) n) Y₄ :
    Functor.obj
        (Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
          (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
        Y₄ ⟶
      Functor.obj
        (Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
          (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
        Y₄)
  (NatTrans.app (natTransPInfty_f (Karoubi.{v_1, u_1} C) n) Y₃)
Tactic: simp only [P₃, P₄, ← natTransPInfty_f_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) 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
have h₄₃ : P₄.f 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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) 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
have h₁₄ : Eq (α :=
  Functor.obj
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
        Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
          (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
      Y ⟶
    Functor.obj
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
        Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
          (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
      Y)
  (NatTrans.app (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi.{v_1, u_1} C) n) Y)
  (CategoryTheory.Functor.map
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
        Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
          (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
      Y.decompId_i ≫
    NatTrans.app (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi.{v_1, u_1} C) n)
        { X := Y.X, p := 𝟙 Y.X, idem := sorry : Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } ≫
      CategoryTheory.Functor.map
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
            (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
        Y.decompId_p)
Tactic: have h₁₄ := Idempotents.natTrans_eq
    ((𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)) ◫
      (natTransPInfty_f (Karoubi C) n)) Y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  (𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n) ≫
      𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌) =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      ((𝟙
              (KaroubiFunctorCategoryEmbedding.obj
                  { X := Y.X, p := 𝟙 Y.X, idem := ⋯ :
                    Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } _⦋n⦌) ≫
            HomologicalComplex.Hom.f PInfty n) ≫
          𝟙
            (KaroubiFunctorCategoryEmbedding.obj
                { X := Y.X, p := 𝟙 Y.X, idem := ⋯ :
                  Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } _⦋n⦌)) ≫
        (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
have h₁₅ : Eq.{v_1 + 1} (α := KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌ ⟶ KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌)
  (HomologicalComplex.Hom.f PInfty n :
    HomologicalComplex.X
        (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n ⟶
      HomologicalComplex.X
        (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n)
  ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
    HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌))
Tactic: rw [id_comp, id_comp, comp_id, comp_id] at h₁₄
Cleared hypotheses: h₁₄
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  Eq.{v_1 + 1} (α := KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌ ⟶ KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n ⟶
        HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n)
    ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌))
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
have rw : Karoubi.Hom.f
    ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)) =
  Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
Tactic: rw [← h₃₂, ← h₄₃, h₁₄]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  Eq.{v_1 + 1} (α := KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌ ⟶ KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n ⟶
        HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n)
    ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌))
⊢ Karoubi.Hom.f
      ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
        HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)) =
    Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
have simp : Y.p.app (op ⦋n⦌) ≫
    CategoryStruct.comp (Y :=
      KaroubiFunctorCategoryEmbedding.obj
            { X := Y.X, p := 𝟙 Y.X, idem := sorry :
              Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } _⦋n⦌.X)
      (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n)) (Y.p.app (op ⦋n⦌)) =
  Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
Tactic: simp only [KaroubiFunctorCategoryEmbedding.map_app_f, Karoubi.decompId_p_f,
    Karoubi.decompId_i_f, Karoubi.comp_f]