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
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 :
  ∀ (n : ℕ),
    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.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) n
⊢ 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)

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 : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ 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.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X)
      n

Tactic:
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
inst_2 : HasPullbacks.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
x : X ⟶ Y
h : Mono x
x_1 : ℕ
dsimp : Mono (X := X _⦋x_1⦌) (x.app (op ⦋x_1⦌))
⊢ Mono (X := HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) x_1)
    (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) x) x_1)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasPullbacks.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
x : X ⟶ Y
h : Mono x
x_1 : ℕ
⊢ Mono (X := X _⦋x_1⦌) (x.app (op ⦋x_1⦌))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
dsimp :
  Eq (α := P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
    (Karoubi.Hom.f
        (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n) :
      KaroubiFunctorCategoryEmbedding.obj P _⦋n + 1⦌.X ⟶ KaroubiFunctorCategoryEmbedding.obj P _⦋n⦌.X)
    (P.p.app (op ⦋n + 1⦌) ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n)
⊢ Eq (α :=
    (HomologicalComplex.X (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1)).X ⟶
      (HomologicalComplex.X (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) n).X)
    (Karoubi.Hom.f
      (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n))
    (P.p.app (op ⦋n + 1⦌) ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
simp :
  Eq.{v_1 + 1} (α := P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
    (∑ x : Fin (n + 2),
      HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • (SimplicialObject.δ (KaroubiFunctorCategoryEmbedding.obj P) x).f)
    (∑ x : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • P.p.app (op ⦋n + 1⦌) ≫ P.X.δ x)
⊢ Eq (α := P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
    (Karoubi.Hom.f
        (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n) :
      KaroubiFunctorCategoryEmbedding.obj P _⦋n + 1⦌.X ⟶ KaroubiFunctorCategoryEmbedding.obj P _⦋n⦌.X)
    (P.p.app (op ⦋n + 1⦌) ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n)

Tactic:
simp only [AlternatingFaceMapComplex.obj_d_eq, Karoubi.sum_hom, Preadditive.comp_sum,
    Karoubi.zsmul_hom, Preadditive.comp_zsmul]

Premises used: AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, CategoryTheory.Idempotents.Karoubi.sum_hom, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Idempotents.Karoubi.zsmul_hom
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
⊢ Eq.{v_1 + 1} (α := P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
    (∑ x : Fin (n + 2),
      HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • (SimplicialObject.δ (KaroubiFunctorCategoryEmbedding.obj P) x).f)
    (∑ x : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • P.p.app (op ⦋n + 1⦌) ≫ P.X.δ x)

Tactic:
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
inst_2 : HasZeroObject.{v_1, u_1} C
X : SimplicialObject.Augmented.{v_1, u_1} C
refine :
  { f :
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0 ⟶
      Functor.obj SimplicialObject.Augmented.point X //
    Eq (α :=
      HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
        Functor.obj SimplicialObject.Augmented.point X)
      (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 0 ≫ f) 0 }
⊢ Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
    (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X)
    (Functor.obj (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C) X)

Tactic:
refine (ChainComplex.toSingle₀Equiv _ _).symm ?_

Premises used: ChainComplex.toSingle₀Equiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : SimplicialObject.Augmented.{v_1, u_1} C
refine :
  Eq (α :=
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
      Functor.obj SimplicialObject.Augmented.point X)
    (CategoryStruct.comp (Y :=
      HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0)
      (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 0)
      (X.hom.app (op ⦋0⦌)))
    0
⊢ { f :
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0 ⟶
      Functor.obj SimplicialObject.Augmented.point X //
    Eq (α :=
      HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
        Functor.obj SimplicialObject.Augmented.point X)
      (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 0 ≫ f) 0 }

Tactic:
refine ⟨X.hom.app (op ⦋0⦌), ?_⟩
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : SimplicialObject.Augmented.{v_1, u_1} C
dsimp :
  Eq (α := X.left _⦋1⦌ ⟶ X.right)
    (CategoryStruct.comp (Y := X.left _⦋0⦌)
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X.left) 1 0) (X.hom.app (op ⦋0⦌)) :
      X.left _⦋1⦌ ⟶ X.right)
    (0 :
      HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
        Functor.obj SimplicialObject.Augmented.point X)
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
      Functor.obj SimplicialObject.Augmented.point X)
    (CategoryStruct.comp (Y :=
      HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0)
      (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 0)
      (X.hom.app (op ⦋0⦌)))
    0

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : SimplicialObject.Augmented.{v_1, u_1} C
rw :
  HAdd.hAdd (α := X.left _⦋1⦌ ⟶ X.right)
      (X.hom.app (op ⦋HAdd.hAdd (α := ℕ) 0 1⦌) ≫ SimplicialObject.δ (Functor.obj (SimplicialObject.const C) X.right) 0)
      (-X.hom.app (op ⦋HAdd.hAdd (α := ℕ) 0 1⦌) ≫
          SimplicialObject.δ (Functor.obj (SimplicialObject.const C) X.right) 1) =
    0
⊢ Eq (α := X.left _⦋1⦌ ⟶ X.right)
    (CategoryStruct.comp (Y := X.left _⦋0⦌)
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X.left) 1 0) (X.hom.app (op ⦋0⦌)) :
      X.left _⦋1⦌ ⟶ X.right)
    (0 :
      HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
        Functor.obj SimplicialObject.Augmented.point X)

Tactic:
rw [alternatingFaceMapComplex_obj_d, objD, Fin.sum_univ_two, Fin.val_zero,
      pow_zero, one_smul, Fin.val_one, pow_one, neg_smul, one_smul, add_comp,
      neg_comp, SimplicialObject.δ_naturality, SimplicialObject.δ_naturality]

Premises used: neg_smul, AlgebraicTopology.alternatingFaceMapComplex_obj_d, CategoryTheory.SimplicialObject.δ_naturality, Fin.val_one, pow_zero, one_smul, CategoryTheory.Preadditive.add_comp, pow_one, CategoryTheory.Preadditive.neg_comp, AlgebraicTopology.AlternatingFaceMapComplex.objD, Fin.sum_univ_two, Fin.val_zero
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : SimplicialObject.Augmented.{v_1, u_1} C
⊢ HAdd.hAdd (α := X.left _⦋1⦌ ⟶ X.right)
      (X.hom.app (op ⦋HAdd.hAdd (α := ℕ) 0 1⦌) ≫ SimplicialObject.δ (Functor.obj (SimplicialObject.const C) X.right) 0)
      (-X.hom.app (op ⦋HAdd.hAdd (α := ℕ) 0 1⦌) ≫
          SimplicialObject.δ (Functor.obj (SimplicialObject.const C) X.right) 1) =
    0

Tactic:
apply add_neg_cancel

Premises used: add_neg_cancel
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X Y : SimplicialObject.Augmented.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α := X.left _⦋0⦌ ⟶ Y.right)
    (f.left.app (op ⦋0⦌) ≫
      HomologicalComplex.Hom.f
        ((Equiv.symm (ChainComplex.toSingle₀Equiv (Functor.obj (alternatingFaceMapComplex C) Y.left) Y.right) :
            (a : { f : Y.left _⦋0⦌ ⟶ Y.right // ((alternatingFaceMapComplex C).obj Y.left).d 1 0 ≫ f = 0 }) →
              (alternatingFaceMapComplex C).obj Y.left ⟶ (ChainComplex.single₀ C).obj Y.right)
          (Subtype.mk (p := fun (f : Y.left _⦋0⦌ ⟶ Y.right) ↦
            Eq (α := Y.left _⦋1⦌ ⟶ Y.right)
              (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y.left) 1 0 ≫ f : Y.left _⦋1⦌ ⟶ Y.right)
              (0 :
                HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) Y) 1 ⟶
                  Functor.obj SimplicialObject.Augmented.point Y))
            (Y.hom.app (op ⦋0⦌)) ⋯))
        0)
    (CategoryStruct.comp (Y := X.right)
      (HomologicalComplex.Hom.f
        ((Equiv.symm (ChainComplex.toSingle₀Equiv (Functor.obj (alternatingFaceMapComplex C) X.left) X.right) :
            (a : { f : X.left _⦋0⦌ ⟶ X.right // ((alternatingFaceMapComplex C).obj X.left).d 1 0 ≫ f = 0 }) →
              (alternatingFaceMapComplex C).obj X.left ⟶ (ChainComplex.single₀ C).obj X.right)
          (Subtype.mk (p := fun (f : X.left _⦋0⦌ ⟶ X.right) ↦
            Eq (α := X.left _⦋1⦌ ⟶ X.right)
              (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X.left) 1 0 ≫ f : X.left _⦋1⦌ ⟶ X.right)
              (0 :
                HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
                  Functor.obj SimplicialObject.Augmented.point X))
            (X.hom.app (op ⦋0⦌)) ⋯))
        0)
      (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (ChainComplex.single₀ C) f.right) 0))

Tactic:
simp [ChainComplex.toSingle₀Equiv, SimplicialObject.Augmented.w₀]

Premises used: CategoryTheory.SimplicialObject.Augmented.w₀, ChainComplex.toSingle₀Equiv
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : SimplicialObject.Augmented.{v_1, u_1} C
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0 ⟶
      HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C) X) 0)
    (HomologicalComplex.Hom.f (NatTrans.app ε X) 0) (X.hom.app (op ⦋0⦌))

Tactic:
ChainComplex.toSingle₀Equiv_symm_apply_f_zero _ _

Premises used: ChainComplex.toSingle₀Equiv_symm_apply_f_zero
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : SimplicialObject.Augmented.{v_1, u_1} C
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) (n + 1) ⟶
      HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C) X) (n + 1))
    (HomologicalComplex.Hom.f (NatTrans.app ε X) (n + 1)) 0

Tactic:
rfl

Premises used: dite, rfl
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
A : Type u_2
inst : Category.{v_2, u_2} A
inst_1 : Abelian.{v_2, u_2} A
X : SimplicialObject.{v_2, u_2} A
n : ℕ
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) n = (NormalizedMooreComplex.objX X n).arrow

Tactic:
dsimp [inclusionOfMooreComplexMap]

Premises used: AlgebraicTopology.inclusionOfMooreComplexMap
-- 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 : CosimplicialObject.{v_1, u_1} C
n : ℕ
simp :
  Eq.{v_1 + 1} (α := X ^⦋n⦌ ⟶ X ^⦋n + 1⦌) (∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i)
    (∑ x : Fin (n + 2),
      HPow.hPow (α := ℤ) (-1) (↑x : ℕ) •
        ((Functor.obj (Equivalence.functor (cosimplicialSimplicialEquiv C)) (op X)).δ x).unop)
⊢ objD X n =
    (AlternatingFaceMapComplex.objD (Functor.obj (Equivalence.functor (cosimplicialSimplicialEquiv C)) (op X)) n).unop

Tactic:
simp only [objD, AlternatingFaceMapComplex.objD, unop_sum, unop_zsmul]

Premises used: CategoryTheory.unop_zsmul, AlgebraicTopology.AlternatingCofaceMapComplex.objD, AlgebraicTopology.AlternatingFaceMapComplex.objD, CategoryTheory.unop_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 : CosimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq.{v_1 + 1} (α := X ^⦋n⦌ ⟶ X ^⦋n + 1⦌) (∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i)
    (∑ x : Fin (n + 2),
      HPow.hPow (α := ℤ) (-1) (↑x : ℕ) •
        ((Functor.obj (Equivalence.functor (cosimplicialSimplicialEquiv C)) (op X)).δ x).unop)

Tactic:
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 : CosimplicialObject.{v_1, u_1} C
n : ℕ
⊢ objD X n ≫ objD X (n + 1) = 0

Tactic:
simp only [d_eq_unop_d, ← unop_comp, AlternatingFaceMapComplex.d_squared, unop_zero]

Premises used: AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d, AlgebraicTopology.AlternatingFaceMapComplex.d_squared, CategoryTheory.unop_comp, CategoryTheory.Limits.unop_zero
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
simp :
  Eq (α := X ^⦋n⦌ ⟶ Y ^⦋n + 1⦌) (f.app ⦋n⦌ ≫ ∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • Y.δ i)
    ((∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫ f.app ⦋n + 1⦌)
⊢ Eq (α := HomologicalComplex.X (obj X) n ⟶ HomologicalComplex.X (obj Y) (n + 1))
    ((fun (n : ℕ) ↦ (f.app ⦋n⦌ : X ^⦋n⦌ ⟶ Y ^⦋n⦌)) n ≫ HomologicalComplex.d (obj Y) n (n + 1))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj X) (n + 1)) (HomologicalComplex.d (obj X) n (n + 1))
      ((fun (n : ℕ) ↦ (f.app ⦋n⦌ : X ^⦋n⦌ ⟶ Y ^⦋n⦌)) (n + 1)))

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

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

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
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
⊢ Eq.{v_1 + 1} (α := X ^⦋n⦌ ⟶ Y ^⦋n + 1⦌) (∑ j : Fin (n + 2), f.app ⦋n⦌ ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • Y.δ j))
    (∑ j : Fin (n + 2), (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ f.app ⦋n + 1⦌)

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

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
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{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 ⦋n⦌ ≫ (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • Y.δ x) =
        (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x) ≫ f.app ⦋n + 1⦌
⊢ Eq.{v_1 + 1} (α := X ^⦋n⦌ ⟶ Y ^⦋n + 1⦌) (∑ j : Fin (n + 2), f.app ⦋n⦌ ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • Y.δ j))
    (∑ j : Fin (n + 2), (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ f.app ⦋n + 1⦌)

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

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
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{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 ⦋n⦌ ≫ Y.δ x = HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x ≫ f.app ⦋n + 1⦌
⊢ f.app ⦋n⦌ ≫ (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • Y.δ x) = (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x) ≫ f.app ⦋n + 1⦌

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
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{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 ⦋n⦌ ≫ Y.δ x = X.δ x ≫ f.app ⦋n + 1⦌
⊢ HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • f.app ⦋n⦌ ≫ Y.δ x = HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x ≫ f.app ⦋n + 1⦌

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
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{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 ⦋n + 1⦌ = f.app ⦋n⦌ ≫ Y.δ x
⊢ f.app ⦋n⦌ ≫ Y.δ x = X.δ x ≫ f.app ⦋n + 1⦌

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
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{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 ⦋n + 1⦌ = f.app ⦋n⦌ ≫ Y.δ x

Tactic:
apply f.naturality

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
f : Arrow.{v, u} C
inst_1 : ∀ (n : ℕ), HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X Y : SimplexCategoryᵒᵖ
g : X ⟶ Y
⊢ ∀ (j : Fin ((Opposite.unop Y).len + 1)),
    Eq (α :=
      (widePullback.{0, v, u} f.right (fun (x : Fin ((Opposite.unop X).len + 1)) ↦ f.left)
          fun (x : Fin ((Opposite.unop X).len + 1)) ↦ f.hom) ⟶
        f.right)
      ((fun (i : Fin ((Opposite.unop Y).len + 1)) ↦
            (WidePullback.π (fun (x : Fin ((Opposite.unop X).len + 1)) ↦ f.hom)
                ((SimplexCategory.Hom.toOrderHom g.unop :
                    (a : Fin ((Opposite.unop Y).len + 1)) → Fin ((Opposite.unop X).len + 1))
                  i) :
              (widePullback.{0, v, u} f.right (fun (x : Fin ((Opposite.unop X).len + 1)) ↦ f.left)
                  fun (x : Fin ((Opposite.unop X).len + 1)) ↦ f.hom) ⟶
                f.left))
          j ≫
        f.hom)
      (WidePullback.base fun (x : Fin ((Opposite.unop X).len + 1)) ↦ f.hom)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
f_1 : Arrow.{v, u} C
inst_1 :
  ∀ (n : ℕ), HasWidePullback.{0, v, u} f_1.right (fun (x : Fin (n + 1)) ↦ f_1.left) fun (x : Fin (n + 1)) ↦ f_1.hom
f g : Arrow.{v, u} C
inst_2 : ∀ (n : ℕ), HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
inst_3 : ∀ (n : ℕ), HasWidePullback.{0, v, u} g.right (fun (x : Fin (n + 1)) ↦ g.left) fun (x : Fin (n + 1)) ↦ g.hom
F : f ⟶ g
n : SimplexCategoryᵒᵖ
j : Fin ((Opposite.unop n).len + 1)
⊢ Eq (α := f.cechNerve.obj n ⟶ g.right)
    ((fun (i : Fin ((Opposite.unop n).len + 1)) ↦
          (WidePullback.π (fun (x : Fin ((Opposite.unop n).len + 1)) ↦ f.hom) i ≫ Hom.left F :
            f.cechNerve.obj n ⟶ g.left))
        j ≫
      g.hom)
    ((WidePullback.base fun (x : Fin ((Opposite.unop n).len + 1)) ↦ f.hom) ≫ Hom.right F)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
G : X ⟶ F.augmentedCechNerve
⊢ Functor.map (𝟭 (SimplicialObject.{v, u} C)) G.left ≫ F.augmentedCechNerve.hom = X.hom ≫ Functor.map (const C) G.right

Tactic:
have := G.w