awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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 : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
h :
  HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ) =
    HPow.hPow (α := ℤ) (-1) (↑(j.castLT ⋯) : ℕ) * HPow.hPow (α := ℤ) (-1) (↑i : ℕ)
⊢ HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ) =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ))

Tactic:
simp only [φ, Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]

Premises used: pow_add, neg_neg, Fin.val_succ, pow_one, mul_one, mul_neg
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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 : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ) =
    HPow.hPow (α := ℤ) (-1) (↑(j.castLT ⋯) : ℕ) * HPow.hPow (α := ℤ) (-1) (↑i : ℕ)

Tactic:
apply mul_comm

Premises used: mul_comm
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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 : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
h : (i, j).2 ≤ (i, j).1.castSucc
⊢ X.δ j ≫ X.δ i = X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1

Tactic:
rw [CategoryTheory.SimplicialObject.δ_comp_δ'']

Premises used: CategoryTheory.SimplicialObject.δ_comp_δ''
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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 : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (i, j).2 ≤ (i, j).1.castSucc

Tactic:
simpa [S] using hij
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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.X (obj X) n = X _⦋n⦌

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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 (obj X) (n + 1) ⟶ HomologicalComplex.X (obj X) n)
    (HomologicalComplex.d (obj X) (n + 1) n) (∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i)

Tactic:
simp [obj]

Premises used: AlgebraicTopology.AlternatingFaceMapComplex.obj
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
simp :
  Eq (α := X _⦋n + 1⦌ ⟶ Y _⦋n⦌) (f.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • Y.δ i)
    ((∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫ f.app (op ⦋n⦌))
⊢ Eq (α := HomologicalComplex.X (obj X) (n + 1) ⟶ HomologicalComplex.X (obj Y) n)
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (n + 1))
      ((fun (n : ℕ) ↦ (f.app (op ⦋n⦌) : X _⦋n⦌ ⟶ Y _⦋n⦌)) (n + 1)) (HomologicalComplex.d (obj Y) (n + 1) n))
    (HomologicalComplex.d (obj X) (n + 1) n ≫ (fun (n : ℕ) ↦ (f.app (op ⦋n⦌) : X _⦋n⦌ ⟶ Y _⦋n⦌)) n)

Tactic:
simp only [obj, ChainComplex.of_d, objD, Int.reduceNeg]

Premises used: Int.reduceNeg, AlgebraicTopology.AlternatingFaceMapComplex.obj, AlgebraicTopology.AlternatingFaceMapComplex.objD, ChainComplex.of_d
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
rw :
  Eq.{v_1 + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n⦌)
    (∑ j : Fin (n + 2), f.app (op ⦋n + 1⦌) ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • Y.δ j))
    (∑ j : Fin (n + 2), (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ f.app (op ⦋n⦌))
⊢ Eq (α := X _⦋n + 1⦌ ⟶ Y _⦋n⦌) (f.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • Y.δ i)
    ((∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫ f.app (op ⦋n⦌))

Tactic:
rw [comp_sum, sum_comp]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.Preadditive.comp_sum
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
⊢ Eq.{v_1 + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n⦌)
    (∑ j : Fin (n + 2), f.app (op ⦋n + 1⦌) ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • Y.δ j))
    (∑ j : Fin (n + 2), (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ f.app (op ⦋n⦌))

Tactic:
Finset.sum_congr rfl fun _ _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
refine :
  ∀ (x : Fin (n + 2)),
    Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x →
      f.app (op ⦋n + 1⦌) ≫ (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • Y.δ x) =
        (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x) ≫ f.app (op ⦋n⦌)
⊢ Eq.{v_1 + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n⦌)
    (∑ j : Fin (n + 2), f.app (op ⦋n + 1⦌) ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • Y.δ j))
    (∑ j : Fin (n + 2), (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ f.app (op ⦋n⦌))

Tactic:
refine Finset.sum_congr rfl fun _ _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
h : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x
rw :
  HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • f.app (op ⦋n + 1⦌) ≫ Y.δ x =
    HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x ≫ f.app (op ⦋n⦌)
⊢ f.app (op ⦋n + 1⦌) ≫ (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • Y.δ x) =
    (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x) ≫ f.app (op ⦋n⦌)

Tactic:
rw [comp_zsmul, zsmul_comp]

Premises used: CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Preadditive.zsmul_comp
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
h : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x
e_a : f.app (op ⦋n + 1⦌) ≫ Y.δ x = X.δ x ≫ f.app (op ⦋n⦌)
⊢ HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • f.app (op ⦋n + 1⦌) ≫ Y.δ x =
    HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x ≫ f.app (op ⦋n⦌)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
h : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x
e_a : X.δ x ≫ f.app (op ⦋n⦌) = f.app (op ⦋n + 1⦌) ≫ Y.δ x
⊢ f.app (op ⦋n + 1⦌) ≫ Y.δ x = X.δ x ≫ f.app (op ⦋n⦌)

Tactic:
symm
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
h : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x
⊢ X.δ x ≫ f.app (op ⦋n⦌) = f.app (op ⦋n + 1⦌) ≫ Y.δ x

Tactic:
apply f.naturality

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
⊢ Eq (α := HomologicalComplex.X (obj X) n ⟶ HomologicalComplex.X (obj Y) n) (HomologicalComplex.Hom.f (map f) n)
    (f.app (op ⦋n⦌))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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.X (Functor.obj (alternatingFaceMapComplex C) X) n = X _⦋n⦌

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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.d (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) n = AlternatingFaceMapComplex.objD X n

Tactic:
simp [alternatingFaceMapComplex]

Premises used: AlgebraicTopology.alternatingFaceMapComplex
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
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) n) (f.app (op ⦋n⦌))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
h_map :
  autoParam
    (∀ (X Y : SimplicialObject.{v_1, u_1} C) (f : X ⟶ Y),
      Eq (α :=
        Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
          (Functor.obj
            (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
              (F.mapHomologicalComplex (ComplexShape.down ℕ)))
            X)
          (Functor.obj
            (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
              (F.mapHomologicalComplex (ComplexShape.down ℕ)))
            Y))
        (CategoryTheory.Functor.map
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          f)
        (CategoryStruct.comp (Y :=
          Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) (eqToHom ⋯)
          (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D)
              f ≫
            eqToHom ⋯)))
    Functor.ext._auto_1
h_obj :
  ∀ (X : SimplicialObject.{v_1, u_1} C),
    Eq (α := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
      (Functor.obj
        (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
          (F.mapHomologicalComplex (ComplexShape.down ℕ)))
        X)
      (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X)
⊢ Eq (α := SimplicialObject.{v_1, u_1} C ⥤ HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
    (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
      (F.mapHomologicalComplex (ComplexShape.down ℕ)))
    (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D)

Tactic:
apply CategoryTheory.Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
h_map :
  ∀ (n : ℕ),
    Eq (α :=
      HomologicalComplex.X
          (Functor.obj
            (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
              (F.mapHomologicalComplex (ComplexShape.down ℕ)))
            X)
          n ⟶
        HomologicalComplex.X
          (Functor.obj
            (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
              (F.mapHomologicalComplex (ComplexShape.down ℕ)))
            Y)
          n)
      (HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          f)
        n)
      (HomologicalComplex.Hom.f
        (CategoryStruct.comp (Y :=
          Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) (eqToHom ⋯)
          (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D)
              f ≫
            eqToHom ⋯))
        n)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
      (Functor.obj
        (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
          (F.mapHomologicalComplex (ComplexShape.down ℕ)))
        X)
      (Functor.obj
        (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
          (F.mapHomologicalComplex (ComplexShape.down ℕ)))
        Y))
    (CategoryTheory.Functor.map
      (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
        (F.mapHomologicalComplex (ComplexShape.down ℕ)))
      f)
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) (eqToHom ⋯)
      (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) f ≫
        eqToHom ⋯))

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          X)
        n ⟶
      HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          Y)
        n)
    (HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map
        (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
          (F.mapHomologicalComplex (ComplexShape.down ℕ)))
        f)
      n)
    (HomologicalComplex.Hom.f
      (CategoryStruct.comp (Y :=
        Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) (eqToHom ⋯)
        (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) f ≫
          eqToHom ⋯))
      n)

Tactic:
simp only [Functor.comp_map, HomologicalComplex.comp_f, alternatingFaceMapComplex_map_f,
      Functor.mapHomologicalComplex_map_f, HomologicalComplex.eqToHom_f, eqToHom_refl, comp_id,
      id_comp, SimplicialObject.whiskering_obj_map_app]

Premises used: HomologicalComplex.eqToHom_f, CategoryTheory.SimplicialObject.whiskering_obj_map_app, CategoryTheory.Functor.mapHomologicalComplex_map_f, AlgebraicTopology.alternatingFaceMapComplex_map_f, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, HomologicalComplex.comp_f, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X : SimplicialObject.{v_1, u_1} C
h_obj :
  ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      Eq (α :=
        HomologicalComplex.X
            (Functor.obj
              (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
                (F.mapHomologicalComplex (ComplexShape.down ℕ)))
              X)
            i ⟶
          HomologicalComplex.X
            (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) j)
        (HomologicalComplex.d
            (Functor.obj
              (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
                (F.mapHomologicalComplex (ComplexShape.down ℕ)))
              X)
            i j ≫
          eqToHom ⋯)
        (eqToHom ⋯ ≫
          HomologicalComplex.d
            (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) i j)
h_obj₁ :
  HomologicalComplex.X
      (Functor.obj
        (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
          (F.mapHomologicalComplex (ComplexShape.down ℕ)))
        X) =
    HomologicalComplex.X (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X)
⊢ Eq (α := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
    (Functor.obj
      (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
        (F.mapHomologicalComplex (ComplexShape.down ℕ)))
      X)
    (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X)

Tactic:
apply HomologicalComplex.ext

Premises used: HomologicalComplex.ext
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X : SimplicialObject.{v_1, u_1} C
j : ℕ
h_obj :
  Eq (α :=
    HomologicalComplex.X
        (Functor.obj (C := ChainComplex.{v_1, u_1, 0} C ℕ) (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (Functor.obj (alternatingFaceMapComplex C) X))
        (j + 1) ⟶
      HomologicalComplex.X
        (Functor.obj (alternatingFaceMapComplex D) ((Functor.obj (SimplicialObject.whiskering C D) F).obj X)) j)
    (HomologicalComplex.d
        (Functor.obj (C := ChainComplex.{v_1, u_1, 0} C ℕ) (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (Functor.obj (alternatingFaceMapComplex C) X))
        (j + 1) j ≫
      eqToHom ⋯)
    (eqToHom ⋯ ≫
      HomologicalComplex.d
        (Functor.obj (alternatingFaceMapComplex D) ((Functor.obj (SimplicialObject.whiskering C D) F).obj X)) (j + 1) j)
⊢ Eq (α :=
    HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          X)
        (j + 1) ⟶
      HomologicalComplex.X
        (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) j)
    (HomologicalComplex.d
        (Functor.obj
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          X)
        (j + 1) j ≫
      eqToHom ⋯)
    (eqToHom ⋯ ≫
      HomologicalComplex.d
        (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) (j + 1) j)

Tactic:
dsimp only [Functor.comp_obj]

Premises used: CategoryTheory.Functor.comp_obj
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X : SimplicialObject.{v_1, u_1} C
j : ℕ
h_obj :
  Eq.{v_2 + 1} (α :=
    HomologicalComplex.X
        (Functor.obj (C := ChainComplex.{v_1, u_1, 0} C ℕ) (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (Functor.obj (alternatingFaceMapComplex C) X))
        (j + 1) ⟶
      HomologicalComplex.X
        (Functor.obj (alternatingFaceMapComplex D) ((Functor.obj (SimplicialObject.whiskering C D) F).obj X)) j)
    (∑ x : Fin (j + 2), HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • F.map (X.δ x))
    (∑ i : Fin (j + 2),
      HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • ((Functor.obj (SimplicialObject.whiskering C D) F).obj X).δ i)
⊢ Eq (α :=
    HomologicalComplex.X
        (Functor.obj (C := ChainComplex.{v_1, u_1, 0} C ℕ) (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (Functor.obj (alternatingFaceMapComplex C) X))
        (j + 1) ⟶
      HomologicalComplex.X
        (Functor.obj (alternatingFaceMapComplex D) ((Functor.obj (SimplicialObject.whiskering C D) F).obj X)) j)
    (HomologicalComplex.d
        (Functor.obj (C := ChainComplex.{v_1, u_1, 0} C ℕ) (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (Functor.obj (alternatingFaceMapComplex C) X))
        (j + 1) j ≫
      eqToHom ⋯)
    (eqToHom ⋯ ≫
      HomologicalComplex.d
        (Functor.obj (alternatingFaceMapComplex D) ((Functor.obj (SimplicialObject.whiskering C D) F).obj X)) (j + 1) j)

Tactic:
simp only [Functor.mapHomologicalComplex_obj_d, alternatingFaceMapComplex_obj_d,
        eqToHom_refl, id_comp, comp_id, AlternatingFaceMapComplex.objD, Functor.map_sum,
        Functor.map_zsmul]

Premises used: CategoryTheory.Functor.mapHomologicalComplex_obj_d, AlgebraicTopology.alternatingFaceMapComplex_obj_d, CategoryTheory.Functor.map_zsmul, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, AlgebraicTopology.AlternatingFaceMapComplex.objD, CategoryTheory.Functor.map_sum, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X : SimplicialObject.{v_1, u_1} C
j : ℕ
⊢ Eq.{v_2 + 1} (α :=
    HomologicalComplex.X
        (Functor.obj (C := ChainComplex.{v_1, u_1, 0} C ℕ) (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (Functor.obj (alternatingFaceMapComplex C) X))
        (j + 1) ⟶
      HomologicalComplex.X
        (Functor.obj (alternatingFaceMapComplex D) ((Functor.obj (SimplicialObject.whiskering C D) F).obj X)) j)
    (∑ x : Fin (j + 2), HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • F.map (X.δ x))
    (∑ i : Fin (j + 2),
      HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • ((Functor.obj (SimplicialObject.whiskering C D) F).obj X).δ i)

Tactic:
rfl