awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
dsimp :
  ∑ i : Fin (a + 1),
          (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑i : ℕ)) •
            φ ≫ X.δ (⟨(↑i : ℕ), ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) +
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) +
      (∑ i : Fin (a + 1),
            (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
              φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑i : ℕ), ⋯⟩ : Fin (n + 3)) +
          (HPow.hPow (α := ℤ) (-1) (a + 1) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
            φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 3)) +
        (HPow.hPow (α := ℤ) (-1) (a + 2) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 2, ⋯⟩ : Fin (n + 3))) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩
⊢ ∑ i : Fin (a + 1),
          (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i.castSucc)) : ℕ)) •
            φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i.castSucc)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) +
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 1)))) : ℕ)) •
          φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 1)))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) +
      (∑ i : Fin (a + 1),
            (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i.castSucc.castSucc)) : ℕ) *
                HPow.hPow (α := ℤ) (-1) (a + 1)) •
              φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i.castSucc.castSucc)) +
          (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1)))) : Fin (n + 3)) : ℕ) *
              HPow.hPow (α := ℤ) (-1) (a + 1)) •
            φ ≫
              X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1))))) +
        (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2)))) : ℕ) *
            HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2))))) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩

Tactic:
dsimp [Fin.cast, Fin.castLE, Fin.castLT]

Premises used: Fin.castLE, Fin.cast, Fin.castLT
-- 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_1 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a_1 + q
hnaq_shift : ∀ (d : ℕ), n + d = a_1 + d + q
a b c d e f : Y ⟶ X _⦋n + 1⦌
h1 : b = f
h2 : d + e = 0
h3 : c + a = 0
rw : a + b + (c + (d + e)) = f
rw₁ : a + b + (c + 0) = f
rw₂ : a + b + c = f
rw₃ : b + a + c = f
rw₄ : b + (a + c) = f
rw₅ : b + (c + a) = f
rw₆ : b + 0 = f
rw₇ : b = f
rw₈ rw₉ : f = f
⊢ a + b + (c + d + e) = f

Tactic:
rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]

Premises used: add_assoc, add_comm, add_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
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f

Tactic:
have simplif :
    ∀ a b c d e f : Y ⟶ X _⦋n + 1⦌, b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f := by
    intro a b c d e f h1 h2 h3
    rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
-- 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
a₁ :
  (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩
a₂ :
  (HPow.hPow (α := ℤ) (-1) (a + 1) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 3)) +
      (HPow.hPow (α := ℤ) (-1) (a + 2) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 2, ⋯⟩ : Fin (n + 3)) =
    0
a₃ :
  HAdd.hAdd (α := Y ⟶ X _⦋n + 1⦌)
      (∑ i : Fin (a + 1),
        (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑i : ℕ), ⋯⟩ : Fin (n + 3)))
      (∑ i : Fin (a + 1),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑i : ℕ)) •
          φ ≫ X.δ (⟨(↑i : ℕ), ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1))) =
    0
⊢ ∑ i : Fin (a + 1),
          (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑i : ℕ)) •
            φ ≫ X.δ (⟨(↑i : ℕ), ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) +
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) +
      (∑ i : Fin (a + 1),
            (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
              φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑i : ℕ), ⋯⟩ : Fin (n + 3)) +
          (HPow.hPow (α := ℤ) (-1) (a + 1) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
            φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 3)) +
        (HPow.hPow (α := ℤ) (-1) (a + 2) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 2, ⋯⟩ : Fin (n + 3))) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩

Tactic:
apply simplif
-- 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
a₁ : Odd (a + (a + 1))
⊢ (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩

Tactic:
rw [← pow_add, Odd.neg_one_pow, neg_smul, one_zsmul]

Premises used: neg_smul, pow_add, one_zsmul, Odd.neg_one_pow
-- 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ a + (a + 1) = 2 * a + 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
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ Odd (a + (a + 1))

Tactic:
exact ⟨a, 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
a₁ :
  (HPow.hPow (α := ℤ) (-1) (a + 1) * HPow.hPow (α := ℤ) (-1) (a + 1)) • φ ≫ 𝟙 (X _⦋n + 1⦌) +
      (HPow.hPow (α := ℤ) (-1) (a + 2) * HPow.hPow (α := ℤ) (-1) (a + 1)) • φ ≫ 𝟙 (X _⦋n + 1⦌) =
    0
⊢ (HPow.hPow (α := ℤ) (-1) (a + 1) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 3)) +
      (HPow.hPow (α := ℤ) (-1) (a + 2) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 2, ⋯⟩ : Fin (n + 3)) =
    0

Tactic:
rw [X.δ_comp_σ_self' (Fin.castSucc_mk _ _ _).symm,
      X.δ_comp_σ_succ' (Fin.succ_mk _ _ _).symm]

Premises used: CategoryTheory.SimplicialObject.δ_comp_σ_self', CategoryTheory.SimplicialObject.δ_comp_σ_succ', Fin.succ_mk, Eq.symm, Fin.castSucc_mk
-- 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ (HPow.hPow (α := ℤ) (-1) (a + 1) * HPow.hPow (α := ℤ) (-1) (a + 1)) • φ ≫ 𝟙 (X _⦋n + 1⦌) +
      (HPow.hPow (α := ℤ) (-1) (a + 2) * HPow.hPow (α := ℤ) (-1) (a + 1)) • φ ≫ 𝟙 (X _⦋n + 1⦌) =
    0

Tactic:
simp only [comp_id, pow_add _ (a + 1) 1, pow_one, mul_neg, mul_one, neg_mul, neg_smul,
      add_neg_cancel]

Premises used: add_neg_cancel, neg_smul, pow_add, CategoryTheory.Category.comp_id, HAdd.hAdd, pow_one, neg_mul, mul_one, OfNat.ofNat, mul_neg
-- 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
a₁ :
  Eq.{v_1 + 1} (α := Y ⟶ X _⦋n + 1⦌)
    (∑ x : Fin (a + 1),
      ((HPow.hPow (α := ℤ) (-1) (↑x : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑x : ℕ), ⋯⟩ : Fin (n + 3)) +
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑x : ℕ)) •
          φ ≫ X.δ (⟨(↑x : ℕ), ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1))))
    0
⊢ HAdd.hAdd (α := Y ⟶ X _⦋n + 1⦌)
      (∑ i : Fin (a + 1),
        (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑i : ℕ), ⋯⟩ : Fin (n + 3)))
      (∑ i : Fin (a + 1),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑i : ℕ)) •
          φ ≫ X.δ (⟨(↑i : ℕ), ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1))) =
    0

Tactic:
rw [← Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
a₁ :
  ∀ (x : Fin (a + 1)),
    Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ x →
      (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
            φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑x : ℕ), ⋯⟩ : Fin (n + 3)) +
          (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑x : ℕ)) •
            φ ≫ X.δ (⟨(↑x : ℕ), ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) =
        0
⊢ Eq.{v_1 + 1} (α := Y ⟶ X _⦋n + 1⦌)
    (∑ x : Fin (a + 1),
      ((HPow.hPow (α := ℤ) (-1) (↑x : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑x : ℕ), ⋯⟩ : Fin (n + 3)) +
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑x : ℕ)) •
          φ ≫ X.δ (⟨(↑x : ℕ), ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1))))
    0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_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
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
a₁ :
  (HPow.hPow (α := ℤ) (-1) i * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨i, ⋯⟩ : Fin (n + 3)) +
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) i) •
        φ ≫ X.δ (⟨i, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) =
    0
⊢ (HPow.hPow (α := ℤ) (-1) (↑(⟨i, hi⟩ : Fin (a + 1)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑(⟨i, hi⟩ : Fin (a + 1)) : ℕ), ⋯⟩ : Fin (n + 3)) +
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(⟨i, hi⟩ : Fin (a + 1)) : ℕ)) •
        φ ≫ X.δ (⟨(↑(⟨i, hi⟩ : Fin (a + 1)) : ℕ), ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) =
    0

Tactic:
simp only
-- 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
⊢ i < 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
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
⊢ 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
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
dsimp : i ≤ a
⊢ (↑(⟨i, ⋯⟩ : Fin (n + 2)) : ℕ) ≤ (↑(⟨a, ⋯⟩ : Fin (n + 1)).castSucc : ℕ)

Tactic:
dsimp
-- 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
⊢ i ≤ a

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
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
⊢ (⟨i, ⋯⟩ : Fin (n + 2)) ≤ ⟨a, ⋯⟩.castSucc

Tactic:
have hia : (⟨i, by lia⟩ : Fin (n + 2)) ≤
        Fin.castSucc (⟨a, by lia⟩ : Fin (n + 1)) := by
      rw [Fin.le_iff_val_le_val]
      dsimp
      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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
hia : (⟨i, ⋯⟩ : Fin (n + 2)) ≤ ⟨a, ⋯⟩.castSucc
a₁ :
  ∀ (pf : IsRightCancelAdd ℕ) (pf_1 : a + 1 < n + 1 + 1) (pf_2 : i < n + 1 + 2) (pf_3 : i < n + 2) (pf_4 : a < n + 1),
    (HPow.hPow (α := ℤ) (-1) i * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, pf_1⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨i, pf_2⟩ : Fin (n + 3)) +
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) i) •
          φ ≫ X.δ (⟨i, pf_3⟩ : Fin (n + 2)) ≫ X.σ (⟨a, pf_4⟩ : Fin (n + 1)) =
      0
⊢ (HPow.hPow (α := ℤ) (-1) i * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨i, ⋯⟩ : Fin (n + 3)) +
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) i) •
        φ ≫ X.δ (⟨i, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) =
    0

Tactic:
generalize_proofs
-- 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
hia : (⟨i, ⋯⟩ : Fin (n + 2)) ≤ ⟨a, ⋯⟩.castSucc
pf : IsRightCancelAdd ℕ
pf_1 : a + 1 < n + 1 + 1
pf_2 : i < n + 1 + 2
pf_3 : i < n + 2
pf_4 : a < n + 1
a₁ :
  (HPow.hPow (α := ℤ) (-1) i * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.δ (⟨i, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) =
    -(HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) i) •
      φ ≫ X.δ (⟨i, pf_3⟩ : Fin (n + 2)) ≫ X.σ (⟨a, pf_4⟩ : Fin (n + 1))
⊢ (HPow.hPow (α := ℤ) (-1) i * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, pf_1⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨i, pf_2⟩ : Fin (n + 3)) +
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) i) •
        φ ≫ X.δ (⟨i, pf_3⟩ : Fin (n + 2)) ≫ X.σ (⟨a, pf_4⟩ : Fin (n + 1)) =
    0

Tactic:
rw [← Fin.succ_mk (n + 1) a ‹_›, ← Fin.castSucc_mk (n + 2) i ‹_›,
      δ_comp_σ_of_le X hia, add_eq_zero_iff_eq_neg, ← neg_zsmul]

Premises used: neg_zsmul, add_eq_zero_iff_eq_neg, Fin.succ_mk, CategoryTheory.SimplicialObject.δ_comp_σ_of_le, HAdd.hAdd, OfNat.ofNat, Fin.castSucc_mk
-- 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
hia : (⟨i, ⋯⟩ : Fin (n + 2)) ≤ ⟨a, ⋯⟩.castSucc
pf : IsRightCancelAdd ℕ
pf_1 : a + 1 < n + 1 + 1
pf_2 : i < n + 1 + 2
pf_3 : i < n + 2
pf_4 : a < n + 1
a₁ :
  HPow.hPow (α := ℤ) (-1) i * HPow.hPow (α := ℤ) (-1) (a + 1) = -(HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) i)
⊢ (HPow.hPow (α := ℤ) (-1) i * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.δ (⟨i, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) =
    -(HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) i) •
      φ ≫ X.δ (⟨i, pf_3⟩ : Fin (n + 2)) ≫ X.σ (⟨a, pf_4⟩ : Fin (n + 1))

Tactic:
congr 2
-- 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
hia : (⟨i, ⋯⟩ : Fin (n + 2)) ≤ ⟨a, ⋯⟩.castSucc
pf : IsRightCancelAdd ℕ
pf_1 : a + 1 < n + 1 + 1
pf_2 : i < n + 1 + 2
pf_3 : i < n + 2
pf_4 : a < n + 1
⊢ HPow.hPow (α := ℤ) (-1) i * HPow.hPow (α := ℤ) (-1) (a + 1) = -(HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) i)

Tactic:
ring
-- 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 φ
hqn : n < q
simp :
  φ ≫
      HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 1) n ≫ hσ' q n (n + 1) ⋯)
        (hσ' q (n + 1) (n + 2) ⋯ ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) =
    0
⊢ Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0

Tactic:
simp only [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl)]

Premises used: AlgebraicTopology.DoldKan.Hσ, HAdd.hAdd, AlgebraicTopology.DoldKan.c_mk, 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
rw :
  Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) 0
⊢ φ ≫
      HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 1) n ≫ hσ' q n (n + 1) ⋯)
        (hσ' q (n + 1) (n + 2) ⋯ ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) =
    0

Tactic:
rw [hσ'_eq_zero hqn (c_mk (n + 1) n rfl), comp_zero, zero_add]

Premises used: CategoryTheory.Limits.comp_zero, zero_add, HAdd.hAdd, AlgebraicTopology.DoldKan.c_mk, AlgebraicTopology.DoldKan.hσ'_eq_zero, 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
pos :
  ∀ (hqn' : n + 1 < q),
    Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) 0
neg :
  ∀ (hqn' : ¬n + 1 < q),
    Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) 0
⊢ Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) 0

Tactic:
by_cases hqn' : n + 1 < q