awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 + 1 ≤ q
succ :
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
⊢ 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:
simp only [P_succ, comp_add, comp_id, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
      add_eq_left]

Premises used: HomologicalComplex.add_f_apply, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, HomologicalComplex.comp_f, add_eq_left, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 + 1 ≤ q
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0

Tactic:
(HigherFacesVanish.of_P q n).comp_Hσ_eq_zero (Nat.succ_le_iff.mp hqn)

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, Iff.mp, Nat.succ_le_iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 + 1 ≤ q
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0

Tactic:
exact (HigherFacesVanish.of_P q n).comp_Hσ_eq_zero (Nat.succ_le_iff.mp hqn)

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, Iff.mp, Nat.succ_le_iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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)
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))
⊢ 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)

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)

Premises used: AlgebraicTopology.DoldKan.P_f_0_eq, HomologicalComplex.add_f_apply, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, HomologicalComplex.comp_f, add_eq_left, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 (Q (q + 1)) n)
    (HomologicalComplex.Hom.f (Q q) n)

Tactic:
simp only [Q, HomologicalComplex.sub_f_apply, P_is_eventually_constant hqn]

Premises used: HomologicalComplex.sub_f_apply, AlgebraicTopology.DoldKan.Q, AlgebraicTopology.DoldKan.P_is_eventually_constant
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 : ℕ
⊢ n ≤ n

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y := HomologicalComplex.X K[X] (n + 1))
      ((fun (n : ℕ) ↦ (HomologicalComplex.Hom.f (P n) n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n))
        (n + 1))
      (HomologicalComplex.d K[X] (n + 1) n))
    (HomologicalComplex.d K[X] (n + 1) n ≫
      (fun (n : ℕ) ↦ (HomologicalComplex.Hom.f (P n) n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)) n)

Tactic:
simpa only [← P_is_eventually_constant (show n ≤ n by rfl),
      AlternatingFaceMapComplex.obj_d_eq] using (P (n + 1) : K[X] ⟶ _).comm (n + 1) n

Premises used: AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, HAdd.hAdd, AlgebraicTopology.DoldKan.P_is_eventually_constant, OfNat.ofNat, HomologicalComplex.Hom.comm, AlgebraicTopology.DoldKan.P
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
⊢ HomologicalComplex.Hom.f PInfty 0 = 𝟙 (HomologicalComplex.X K[X] 0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 (P n) n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
dsimp : HSub.hSub (α := X _⦋0⦌ ⟶ X _⦋0⦌) (𝟙 (X _⦋0⦌)) (𝟙 (X _⦋0⦌)) = 0
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (HomologicalComplex.Hom.f QInfty 0) 0

Tactic:
dsimp [QInfty]

Premises used: AlgebraicTopology.DoldKan.QInfty
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
⊢ HSub.hSub (α := X _⦋0⦌ ⟶ X _⦋0⦌) (𝟙 (X _⦋0⦌)) (𝟙 (X _⦋0⦌)) = 0

Tactic:
simp only [sub_self]

Premises used: sub_self
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 (Q n) n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[Y] n) (f.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n)
    (HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))

Tactic:
P_f_naturality n n f

Premises used: AlgebraicTopology.DoldKan.P_f_naturality
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[Y] n) (f.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f QInfty n)
    (HomologicalComplex.Hom.f QInfty n ≫ f.app (op ⦋n⦌))

Tactic:
Q_f_naturality n n f

Premises used: AlgebraicTopology.DoldKan.Q_f_naturality
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 PInfty n) (HomologicalComplex.Hom.f PInfty n)

Tactic:
simp only [PInfty_f, P_f_idem]

Premises used: AlgebraicTopology.DoldKan.P_f_idem, AlgebraicTopology.DoldKan.PInfty_f
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
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)
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (PInfty ≫ PInfty) PInfty

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 ≫ PInfty) n) (HomologicalComplex.Hom.f PInfty n)

Tactic:
PInfty_f_idem n

Premises used: AlgebraicTopology.DoldKan.PInfty_f_idem
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 ≫ PInfty) n) (HomologicalComplex.Hom.f PInfty n)

Tactic:
exact PInfty_f_idem n

Premises used: AlgebraicTopology.DoldKan.PInfty_f_idem
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 QInfty n) (HomologicalComplex.Hom.f QInfty n)

Tactic:
Q_f_idem _ _

Premises used: AlgebraicTopology.DoldKan.Q_f_idem
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
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)
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (QInfty ≫ QInfty) QInfty

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 ≫ QInfty) n) (HomologicalComplex.Hom.f QInfty n)

Tactic:
QInfty_f_idem n

Premises used: AlgebraicTopology.DoldKan.QInfty_f_idem
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 ≫ QInfty) n) (HomologicalComplex.Hom.f QInfty n)

Tactic:
exact QInfty_f_idem n

Premises used: AlgebraicTopology.DoldKan.QInfty_f_idem
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 : ℕ
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
⊢ 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

Tactic:
dsimp only [QInfty]

Premises used: AlgebraicTopology.DoldKan.QInfty
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 : ℕ
⊢ 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:
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, comp_id,
    PInfty_f_idem, sub_self]

Premises used: sub_self, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.PInfty_f_idem, CategoryTheory.Preadditive.comp_sub
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
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)
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (PInfty ≫ QInfty) 0

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 ≫ QInfty) n) (HomologicalComplex.Hom.f 0 n)

Tactic:
apply PInfty_f_comp_QInfty_f

Premises used: AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 : ℕ
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
⊢ 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

Tactic:
dsimp only [QInfty]

Premises used: AlgebraicTopology.DoldKan.QInfty
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 : ℕ
⊢ (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:
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, sub_comp, id_comp,
    PInfty_f_idem, sub_self]

Premises used: sub_self, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, AlgebraicTopology.DoldKan.PInfty_f_idem, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
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)
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (QInfty ≫ PInfty) 0

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 ≫ PInfty) n) (HomologicalComplex.Hom.f 0 n)

Tactic:
apply QInfty_f_comp_PInfty_f

Premises used: AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
dsimp : PInfty + HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) PInfty = 𝟙 K[X]
⊢ HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) PInfty QInfty = 𝟙 K[X]

Tactic:
dsimp only [QInfty]

Premises used: AlgebraicTopology.DoldKan.QInfty
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
⊢ PInfty + HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) PInfty = 𝟙 K[X]

Tactic:
simp only [add_sub_cancel]

Premises used: add_sub_cancel
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 : ℕ
⊢ HAdd.hAdd (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f PInfty n)
      (HomologicalComplex.Hom.f QInfty n) =
    𝟙 (HomologicalComplex.X K[X] n)

Tactic:
HomologicalComplex.congr_hom PInfty_add_QInfty n

Premises used: HomologicalComplex.congr_hom, AlgebraicTopology.DoldKan.PInfty_add_QInfty
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
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)
⊢ 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)

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
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:
PInfty_f_naturality n f

Premises used: AlgebraicTopology.DoldKan.PInfty_f_naturality
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
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:
exact PInfty_f_naturality n f

Premises used: AlgebraicTopology.DoldKan.PInfty_f_naturality
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq.{v_2 + 1} (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n)
    (HomologicalComplex.Hom.f PInfty n) (G.map (HomologicalComplex.Hom.f PInfty n))

Tactic:
simp only [PInfty_f, map_P]

Premises used: AlgebraicTopology.DoldKan.PInfty_f, AlgebraicTopology.DoldKan.map_P
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
change : (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
⊢ Eq.{v_1 + 1} (α :=
    (HomologicalComplex.X K[Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y] n).X ⟶
      (HomologicalComplex.X K[Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y] n).X)
    (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n)) (Y.p.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n)

Tactic:
change (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Premises used: CategoryTheory.Idempotents.Karoubi.Hom.f, HomologicalComplex.Hom.f, CategoryTheory.Idempotents.Karoubi.p, SimplexCategory.mk, Opposite.op, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 = 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)
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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
⊢ 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₂