awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
| ∑ x : Fin (a + 3),
    (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x))
have a₁ : ∑ i : Fin (a + 1),
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q i.castSucc.castSucc)) : ℕ) *
          HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q i.castSucc.castSucc)) +
    (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1)))) : Fin (n + 3)) : ℕ) *
        HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1))))) +
  (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q (Fin.last (a + 2)))) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
    φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q (Fin.last (a + 2))))
Tactic: rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
| ∑ x : Fin (a + 3),
    (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x))
have a₁ : ∑ i : Fin (a + 2),
    (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q i.castSucc)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q i.castSucc)) +
  (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q (Fin.last (a + 2)))) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
    φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q (Fin.last (a + 2))))
Tactic: · rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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₁ :
  ∑ i : Fin (a + 2),
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i.castSucc)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i.castSucc)) +
    (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 : Fin (a + 3),
    (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x))
have a₂ : ∑ i : Fin (a + 1),
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q i.castSucc.castSucc)) : ℕ) *
          HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q i.castSucc.castSucc)) +
    (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1)))) : Fin (n + 3)) : ℕ) *
        HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1))))) +
  (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q (Fin.last (a + 2)))) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
    φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q (Fin.last (a + 2))))
Tactic: · rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
| HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ x : Fin (a + 2),
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ)) •
        φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
    (∑ x : Fin (a + 3),
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)))
have a₁ : ∑ x : Fin (a + 2),
  (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q x)) : ℕ)) •
    φ ≫ X.δ (Fin.cast sorry (Fin.castAdd q x)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1))
Tactic: congr
    · rw [Fin.sum_univ_castSucc]
    · rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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₁ :
  ∑ x : Fin (a + 2),
    (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ)) •
      φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1))
| HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ x : Fin (a + 2),
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ)) •
        φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
    (∑ x : Fin (a + 3),
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)))
have a₂ : ∑ x : Fin (a + 3),
  (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q x)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
    φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q x))
Tactic: congr
    · rw [Fin.sum_univ_castSucc]
    · rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ x : Fin (a + 2),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ)) •
          φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
      (∑ x : Fin (a + 3),
        (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x))) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩
have conv_lhs : ∑ i : Fin (a + 1),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q i.castSucc)) : ℕ)) •
          φ ≫ X.δ (Fin.cast sorry (Fin.castAdd q i.castSucc)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)) +
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q (Fin.last (a + 1)))) : ℕ)) •
        φ ≫ X.δ (Fin.cast sorry (Fin.castAdd q (Fin.last (a + 1)))) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)) +
    (∑ i : Fin (a + 1),
          (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q i.castSucc.castSucc)) : ℕ) *
              HPow.hPow (α := ℤ) (-1) (a + 1)) •
            φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q i.castSucc.castSucc)) +
        (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1)))) : Fin (n + 3)) : ℕ) *
            HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1))))) +
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q (Fin.last (a + 2)))) : ℕ) *
          HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q (Fin.last (a + 2))))) =
  -φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2)) ≫ X.σ ⟨a, sorry⟩
Tactic: conv_lhs =>
    congr
    · rw [Fin.sum_univ_castSucc]
    · rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ ∑ 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, ⋯⟩
have dsimp : ∑ i : Fin (a + 1),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑i : ℕ)) •
          φ ≫ X.δ (⟨(↑i : ℕ), sorry⟩ : Fin (n + 2)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)) +
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)) +
    (∑ i : Fin (a + 1),
          (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
            φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑i : ℕ), sorry⟩ : Fin (n + 3)) +
        (HPow.hPow (α := ℤ) (-1) (a + 1) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 3)) +
      (HPow.hPow (α := ℤ) (-1) (a + 2) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 2, sorry⟩ : Fin (n + 3))) =
  -φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2)) ≫ X.σ ⟨a, sorry⟩
Tactic: dsimp [Fin.cast, Fin.castLE, Fin.castLT]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ a + b + (c + d + e) = f
have rw : 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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ a + b + (c + d + e) = f
have rw₁ : a + b + (c + 0) = f
Tactic: rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ a + b + (c + d + e) = f
have rw₂ : a + b + c = f
Tactic: rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ a + b + (c + d + e) = f
have rw₃ : b + a + c = f
Tactic: rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ a + b + (c + d + e) = f
have rw₄ : b + (a + c) = f
Tactic: rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ a + b + (c + d + e) = f
have rw₅ : b + (c + a) = f
Tactic: rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ a + b + (c + d + e) = f
have rw₆ : b + 0 = f
Tactic: rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ a + b + (c + d + e) = f
have rw₈ : f = f
Tactic: rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (hypothesis)
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
⊢ ∑ 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, ⋯⟩
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
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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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 : 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, ⋯⟩
have a₁ : (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (a + 1)) •
    φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)) =
  -φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2)) ≫ X.σ ⟨a, sorry⟩
Tactic: apply simplif
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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, ⋯⟩
⊢ ∑ 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, ⋯⟩
have a₂ : (HPow.hPow (α := ℤ) (-1) (a + 1) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 3)) +
    (HPow.hPow (α := ℤ) (-1) (a + 2) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨a + 2, sorry⟩ : Fin (n + 3)) =
  0
Tactic: apply simplif
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ ∑ 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, ⋯⟩
have a₃ : HAdd.hAdd (α := Y ⟶ X _⦋n + 1⦌)
    (∑ i : Fin (a + 1),
      (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑i : ℕ), sorry⟩ : Fin (n + 3)))
    (∑ i : Fin (a + 1),
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑i : ℕ)) •
        φ ≫ X.δ (⟨(↑i : ℕ), sorry⟩ : Fin (n + 2)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1))) =
  0
Tactic: apply simplif