awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
α : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))
  (Functor.obj N (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)) :=
  Functor.mapIso N (Iso.app Γ₂N₂ P)
β : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N P))
  (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P)) :=
  Iso.app N₂Γ₂ (Functor.obj N P)
⊢ β.inv ≫ α.inv = 𝟙 (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P))

Tactic:
exact AlgebraicTopology.DoldKan.identity_N₂_objectwise P

Premises used: AlgebraicTopology.DoldKan.identity_N₂_objectwise
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
      (Karoubi.X
        (Functor.obj
          (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C)) ⋙
            Equivalence.functor Preadditive.DoldKan.equivalence)
          X))
      (Karoubi.X (Functor.obj N₁ X)))
    (Karoubi.Hom.f (NatTrans.app (Iso.hom isoN₁) X) :
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
        (Karoubi.X
          (Functor.obj
            (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C)) ⋙
              Equivalence.functor Preadditive.DoldKan.equivalence)
            X))
        (Karoubi.X (Functor.obj N₁ X)))
    (PInfty :
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
        (AlgebraicTopology.AlternatingFaceMapComplex.obj
          (Karoubi.X (Functor.obj (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))) X)))
        (AlgebraicTopology.AlternatingFaceMapComplex.obj
          (Karoubi.X (Functor.obj (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))) X))))

Tactic:
rfl

Premises used: AlgebraicTopology.DoldKan.PInfty, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
X : ChainComplex.{v_1, u_1, 0} C ℕ
h :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X
          (Karoubi.X
            (Functor.obj N₂
              (Functor.obj
                (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
                  Equivalence.inverse Preadditive.DoldKan.equivalence)
                X)))
          i ⟶
        HomologicalComplex.X
          (Karoubi.X
            (Functor.obj N₂
              (Functor.obj (Γ ⋙ Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))) X)))
          i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (Functor.map N₂ (NatTrans.app (Iso.hom isoΓ₀) X))) i)
      (HomologicalComplex.Hom.f PInfty i)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
      (Karoubi.X
        (Functor.obj N₂
          (Functor.obj
            (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
              Equivalence.inverse Preadditive.DoldKan.equivalence)
            X)))
      (Karoubi.X
        (Functor.obj N₂
          (Functor.obj (Γ ⋙ Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))) X))))
    (Karoubi.Hom.f (Functor.map N₂ (NatTrans.app (Iso.hom isoΓ₀) X))) PInfty

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
X : ChainComplex.{v_1, u_1, 0} C ℕ
i : ℕ
⊢ Eq (α :=
    HomologicalComplex.X
        (Karoubi.X
          (Functor.obj N₂
            (Functor.obj
              (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
                Equivalence.inverse Preadditive.DoldKan.equivalence)
              X)))
        i ⟶
      HomologicalComplex.X
        (Karoubi.X
          (Functor.obj N₂
            (Functor.obj (Γ ⋙ Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))) X)))
        i)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Functor.map N₂ (NatTrans.app (Iso.hom isoΓ₀) X))) i)
    (HomologicalComplex.Hom.f PInfty i)

Tactic:
apply comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
⊢ Eq (α := SimplicialObject.{v_1, u_1} C ⥤ ChainComplex.{v_1, u_1, 0} C ℕ) (Equivalence.functor equivalence) N

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Idempotents.DoldKan.N, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
⊢ Eq (α := ChainComplex.{v_1, u_1, 0} C ℕ ⥤ SimplicialObject.{v_1, u_1} C) (Equivalence.inverse equivalence) Γ

Tactic:
rfl

Premises used: CategoryTheory.Idempotents.DoldKan.Γ, CategoryTheory.Functor.comp, AlgebraicTopology.DoldKan.Γ₀, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ Eq (α :=
    Functor.obj (Γ₂ ⋙ N₂) (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K) ⟶
      Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
        (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K))
    (NatTrans.app (Iso.hom N₂Γ₂ToKaroubiIso) K ≫ NatTrans.app (Iso.hom N₁Γ₀) K)
    (Functor.map (Equivalence.functor Preadditive.DoldKan.equivalence) (NatTrans.app (Iso.hom isoΓ₀) K) ≫
      NatTrans.app (Iso.hom isoN₁) (Functor.obj Γ K) ≫ NatTrans.app (Iso.hom N₁Γ₀) K)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ Eq (α :=
    Functor.obj
        (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
          Equivalence.inverse Preadditive.DoldKan.equivalence ⋙ Equivalence.functor Preadditive.DoldKan.equivalence)
        K ⟶
      Functor.obj (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))) K)
    (NatTrans.app (Iso.hom (Equivalence.counitIso Preadditive.DoldKan.equivalence))
        (Functor.obj (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))) K) :
      Functor.obj
          (Equivalence.inverse Preadditive.DoldKan.equivalence ⋙ Equivalence.functor Preadditive.DoldKan.equivalence)
          (Functor.obj (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))) K) ⟶
        Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
          (Functor.obj (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))) K))
    (Functor.map (Equivalence.functor Preadditive.DoldKan.equivalence) (NatTrans.app (Iso.hom isoΓ₀) K) ≫
      NatTrans.app (Iso.hom isoN₁) (Functor.obj Γ K) ≫ NatTrans.app (Iso.hom N₁Γ₀) K)

Tactic:
exact (N₂Γ₂_compatible_with_N₁Γ₀ K).trans (by simp)

Premises used: AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀, Eq.trans
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
⊢ Eq (α :=
    Iso (C := ChainComplex.{v_1, u_1, 0} C ℕ ⥤ ChainComplex.{v_1, u_1, 0} C ℕ)
      (Equivalence.inverse equivalence ⋙ Equivalence.functor equivalence) (𝟭 (ChainComplex.{v_1, u_1, 0} C ℕ)))
    (Equivalence.counitIso equivalence) η

Tactic:
Compatibility.equivalenceCounitIso_eq hη

Premises used: AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_eq, CategoryTheory.Idempotents.DoldKan.η, CategoryTheory.Idempotents.DoldKan.hη
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
w :
  Eq (α :=
    Quiver.Hom (V := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C))
      (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C)))
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
        (Equivalence.inverse Preadditive.DoldKan.equivalence)))
    (Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁)) (Iso.hom Γ₂N₁)
⊢ Eq (α :=
    Iso (C := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C))
      (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C)))
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
        (Equivalence.inverse Preadditive.DoldKan.equivalence)))
    (Compatibility.υ toKaroubiCompN₂IsoN₁) Γ₂N₁

Tactic:
ext1
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
w :
  Eq (α :=
    Quiver.Hom (V := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C))
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂)
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
        (Equivalence.inverse Preadditive.DoldKan.equivalence)))
    (Iso.inv Γ₂N₁ ≫ Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁))
    (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂))
⊢ Eq (α :=
    Quiver.Hom (V := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C))
      (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C)))
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
        (Equivalence.inverse Preadditive.DoldKan.equivalence)))
    (Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁)) (Iso.hom Γ₂N₁)

Tactic:
rw [← cancel_epi Γ₂N₁.inv, Iso.inv_hom_id]

Premises used: AlgebraicTopology.DoldKan.Γ₂N₁, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
w :
  ∀ (X : SimplicialObject.{v_1, u_1} C),
    Eq (α :=
      Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
        Functor.obj
          (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
            (Equivalence.inverse Preadditive.DoldKan.equivalence))
          X)
      (NatTrans.app (Iso.inv Γ₂N₁ ≫ Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁)) X)
      (NatTrans.app (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂)) X)
⊢ Eq (α :=
    Quiver.Hom (V := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C))
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂)
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
        (Equivalence.inverse Preadditive.DoldKan.equivalence)))
    (Iso.inv Γ₂N₁ ≫ Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁))
    (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂))

Tactic:
ext X : 2
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
w :
  Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj
        (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
          (Equivalence.inverse Preadditive.DoldKan.equivalence))
        X)
    (NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) ≫
        CategoryStruct.comp (Y :=
          Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
            (Equivalence.inverse Preadditive.DoldKan.equivalence)
            (Functor.obj (Equivalence.functor Preadditive.DoldKan.equivalence)
              (Functor.obj (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))) X)))
          (NatTrans.app (Iso.hom Γ₂N₂)
            (Functor.obj (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))) X))
          (Functor.map (Equivalence.inverse Preadditive.DoldKan.equivalence)
            (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)))
    (NatTrans.app (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂)) X)
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj
        (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
          (Equivalence.inverse Preadditive.DoldKan.equivalence))
        X)
    (NatTrans.app (Iso.inv Γ₂N₁ ≫ Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁)) X)
    (NatTrans.app (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂)) X)

Tactic:
rw [NatTrans.comp_app, Γ₂N₁_inv, compatibility_Γ₂N₁_Γ₂N₂_natTrans X, Compatibility.υ_hom_app,
    Preadditive.DoldKan.equivalence_unitIso, Iso.app_inv, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.app_inv, CategoryTheory.Preadditive.DoldKan.equivalence_unitIso, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, AlgebraicTopology.DoldKan.Compatibility.υ_hom_app, CategoryTheory.NatTrans.comp_app, AlgebraicTopology.DoldKan.Γ₂N₁_inv
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
⊢ Eq (α :=
    Iso (C := SimplicialObject.{v_1, u_1} C ⥤ SimplicialObject.{v_1, u_1} C) (𝟭 (SimplicialObject.{v_1, u_1} C))
      (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (Equivalence.functor equivalence)
        (Equivalence.inverse equivalence)))
    (Equivalence.unitIso equivalence) ε

Tactic:
Compatibility.equivalenceUnitIso_eq hε

Premises used: CategoryTheory.Idempotents.DoldKan.ε, AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_eq, CategoryTheory.Idempotents.DoldKan.hε
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 2)
hj₁ : j ≠ 0
hj₂ : n + 2 ≤ (↑j : ℕ) + q
obtain : ∀ (i : Fin (n + 1)) (hj₁ : i.succ ≠ 0) (hj₂ : n + 2 ≤ (↑i.succ : ℕ) + q), φ ≫ X.δ i.succ = 0
⊢ φ ≫ X.δ j = 0

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero hj₁

Premises used: Fin.eq_succ_of_ne_zero, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : i.succ ≠ 0
hj₂ : n + 2 ≤ (↑i.succ : ℕ) + q
apply : n + 1 ≤ (↑i : ℕ) + q
⊢ φ ≫ X.δ i.succ = 0

Tactic:
apply v i
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : i.succ ≠ 0
hj₂ : n + 2 ≤ (↑i : ℕ) + 1 + q
⊢ n + 1 ≤ (↑i : ℕ) + q

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish (q + 1) φ
j : Fin (n + 1)
hj : n + 1 ≤ (↑j : ℕ) + q
⊢ n + 1 ≤ (↑j : ℕ) + (q + 1)

Tactic:
simpa only [← add_assoc] using le_add_right hj

Premises used: add_assoc, le_add_right
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y Z : C
q n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
f : Z ⟶ Y
j : Fin (n + 1)
hj : n + 1 ≤ (↑j : ℕ) + q
rw : f ≫ φ ≫ X.δ j.succ = 0
rw₁ : Eq (α := Z ⟶ X _⦋n⦌) (f ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := Z ⟶ X _⦋n⦌) 0 0
⊢ (f ≫ φ) ≫ X.δ j.succ = 0

Tactic:
rw [assoc, v j hj, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
⊢ a + 1 < n + 2

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
⊢ a < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
d : ℕ
⊢ n + d = a + d + q

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
⊢ ∀ (d : ℕ), n + d = a + d + q

Tactic:
have hnaq_shift (d : ℕ) : n + d = a + d + q := by lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
rw :
  φ ≫
      HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (β :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 1) n ≫
          (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯)
        ((HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (HPow.hPow (α := ℤ) (-1) (a + 1))
              (X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫
            eqToHom ⋯) ≫
          HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1))

Tactic:
rw [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl),
    hσ'_eq hnaq (c_mk (n + 1) n rfl), hσ'_eq (hnaq_shift 1) (c_mk (n + 2) (n + 1) rfl)]

Premises used: AlgebraicTopology.DoldKan.Hσ, HAdd.hAdd, AlgebraicTopology.DoldKan.c_mk, AlgebraicTopology.DoldKan.hσ'_eq, Homotopy.nullHomotopicMap'_f, OfNat.ofNat, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simp :
  HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ j : Fin (n + 2),
        φ ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))))
      (∑ j : Fin (n + 1 + 2),
        φ ≫
          HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (HPow.hPow (α := ℤ) (-1) (a + 1))
              (X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫
            (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j)) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩
⊢ φ ≫
      HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (β :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 1) n ≫
          (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯)
        ((HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (HPow.hPow (α := ℤ) (-1) (a + 1))
              (X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫
            eqToHom ⋯) ≫
          HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩

Tactic:
simp only [AlternatingFaceMapComplex.obj_d_eq, eqToHom_refl, comp_id, comp_sum, sum_comp,
    comp_add]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simp :
  HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ x : Fin (n + 2),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑x : ℕ)) • (φ ≫ X.δ x) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
      (∑ x : Fin (n + 1 + 2),
        (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ x) =
    -(φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2))) ≫ X.σ ⟨a, ⋯⟩
⊢ HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ j : Fin (n + 2),
        φ ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))))
      (∑ j : Fin (n + 1 + 2),
        φ ≫
          HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (HPow.hPow (α := ℤ) (-1) (a + 1))
              (X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫
            (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j)) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩

Tactic:
simp only [comp_zsmul, zsmul_comp, ← assoc, ← mul_zsmul]

Premises used: CategoryTheory.Category.assoc, mul_zsmul, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Preadditive.zsmul_comp