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
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 * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩
have a₁ : Odd (a + (a + 1))
Tactic: rw [← pow_add, Odd.neg_one_pow, neg_smul, one_zsmul]
-- 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
⊢ (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
have 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
Tactic: rw [X.δ_comp_σ_self' (Fin.castSucc_mk _ _ _).symm,
      X.δ_comp_σ_succ' (Fin.succ_mk _ _ _).symm]
-- 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
⊢ 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
have 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, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑x : ℕ), sorry⟩ : Fin (n + 3)) +
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑x : ℕ)) •
        φ ≫ X.δ (⟨(↑x : ℕ), sorry⟩ : Fin (n + 2)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1))))
  0
Tactic: rw [← Finset.sum_add_distrib]
-- 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
⊢ 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
have 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, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (⟨(↑x : ℕ), sorry⟩ : Fin (n + 3)) +
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑x : ℕ)) •
          φ ≫ X.δ (⟨(↑x : ℕ), sorry⟩ : Fin (n + 2)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)) =
      0
Tactic: apply Finset.sum_eq_zero
-- 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 : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
⊢ (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
have a₁ : (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 * HPow.hPow (α := ℤ) (-1) i) •
      φ ≫ X.δ (⟨i, sorry⟩ : Fin (n + 2)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)) =
  0
Tactic: simp only
-- 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 : ℕ
hi : i < a + 1
h : Membership.mem (γ := Finset (Fin (a + 1))) Finset.univ (⟨i, hi⟩ : Fin (a + 1))
⊢ (↑(⟨i, ⋯⟩ : Fin (n + 2)) : ℕ) ≤ (↑(⟨a, ⋯⟩ : Fin (n + 1)).castSucc : ℕ)
have dsimp : i ≤ a
Tactic: dsimp
-- 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
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))
⊢ (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
have hia : (⟨i, sorry⟩ : Fin (n + 2)) ≤ ⟨a, sorry⟩.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
-- 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 : ℕ
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
⊢ (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
have 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
Tactic: generalize_proofs
-- 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 : ℕ
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)) •
        φ ≫ 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
have a₁ : (HPow.hPow (α := ℤ) (-1) i * HPow.hPow (α := ℤ) (-1) (a + 1)) •
    φ ≫ X.δ (⟨i, sorry⟩ : Fin (n + 2)) ≫ X.σ (⟨a, sorry⟩ : 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: 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]
-- 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 : ℕ
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)) •
      φ ≫ 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))
have a₁ : HPow.hPow (α := ℤ) (-1) i * HPow.hPow (α := ℤ) (-1) (a + 1) = -(HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) i)
Tactic: congr 2
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
⊢ Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
have 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) sorry)
      (hσ' q (n + 1) (n + 2) sorry ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) =
  0
Tactic: simp only [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl)]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫
      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
have rw : Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
  (φ ≫ hσ' q (n + 1) (n + 2) sorry ≫ 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]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < 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
have pos : ∀ (hqn' : n + 1 < q),
  Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (φ ≫ hσ' q (n + 1) (n + 2) sorry ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) 0
Tactic: by_cases hqn' : n + 1 < q
-- 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 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
⊢ 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
have neg : ∀ (hqn' : ¬n + 1 < q),
  Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (φ ≫ hσ' q (n + 1) (n + 2) sorry ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) 0
Tactic: by_cases hqn' : n + 1 < q
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
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
have pos : Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
  (φ ≫
    CategoryStruct.comp (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 2)) 0
      (HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)))
  0
Tactic: rw [hσ'_eq_zero hqn' (c_mk (n + 2) (n + 1) rfl), zero_comp, comp_zero]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : n + 1 < q
pos :
  Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (φ ≫
      CategoryStruct.comp (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 2)) 0
        (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
have pos₁ : Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1)) (φ ≫ 0) 0
Tactic: rw [hσ'_eq_zero hqn' (c_mk (n + 2) (n + 1) rfl), zero_comp, comp_zero]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : n + 1 < q
pos :
  Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (φ ≫
      CategoryStruct.comp (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 2)) 0
        (HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)))
    0
pos₁ : Eq (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1)) (φ ≫ 0) 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
have pos₂ : Eq.{v_1 + 1} (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1)) 0 0
Tactic: rw [hσ'_eq_zero hqn' (c_mk (n + 2) (n + 1) rfl), zero_comp, comp_zero]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
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
have neg : Eq.{v_1 + 1} (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
  (∑ j : Fin (n + 1 + 2), φ ≫ X.σ 0 ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j)) 0
Tactic: simp only [hσ'_eq (show n + 1 = 0 + q by lia) (c_mk (n + 2) (n + 1) rfl), pow_zero,
      Fin.mk_zero, one_zsmul, eqToHom_refl, comp_id, comp_sum,
      AlternatingFaceMapComplex.obj_d_eq]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ Eq.{v_1 + 1} (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ j : Fin (n + 1 + 2), φ ≫ X.σ 0 ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j)) 0
have neg : φ ≫ X.σ 0 ≫ HSMul.hSMul (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) +
    φ ≫
      X.σ 0 ≫
        HSMul.hSMul (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1⦌) (HPow.hPow (α := ℤ) (-1) (↑(Fin.succ 0) : ℕ))
          (X.δ (Fin.succ 0)) =
  0
Tactic: rw [Fin.sum_univ_succ, Fin.sum_univ_succ, Fintype.sum_eq_zero, add_zero]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
neg :
  φ ≫ X.σ 0 ≫ HSMul.hSMul (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) +
      φ ≫
        X.σ 0 ≫
          HSMul.hSMul (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1⦌) (HPow.hPow (α := ℤ) (-1) (↑(Fin.succ 0) : ℕ))
            (X.δ (Fin.succ 0)) =
    0
⊢ Eq.{v_1 + 1} (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ j : Fin (n + 1 + 2), φ ≫ X.σ 0 ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j)) 0
have neg₁ : ∀ (a : Fin (n + 1)), φ ≫ X.σ 0 ≫ (HPow.hPow (α := ℤ) (-1) (↑a.succ.succ : ℕ) • X.δ a.succ.succ) = 0
Tactic: rw [Fin.sum_univ_succ, Fin.sum_univ_succ, Fintype.sum_eq_zero, add_zero]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ φ ≫ X.σ 0 ≫ (HPow.hPow (α := ℤ) (-1) (↑j.succ.succ : ℕ) • X.δ j.succ.succ) = 0
have neg : j.succ.succ.pred sorry ≠ 0
Tactic: rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
neg : j.succ.succ.pred ⋯ ≠ 0
⊢ φ ≫ X.σ 0 ≫ (HPow.hPow (α := ℤ) (-1) (↑j.succ.succ : ℕ) • X.δ j.succ.succ) = 0
have neg₁ : n + 2 ≤ (↑(j.succ.succ.pred sorry) : ℕ) + q
Tactic: rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
neg : j.succ.succ.pred ⋯ ≠ 0
neg₁ : n + 2 ≤ (↑(j.succ.succ.pred ⋯) : ℕ) + q
⊢ φ ≫ X.σ 0 ≫ (HPow.hPow (α := ℤ) (-1) (↑j.succ.succ : ℕ) • X.δ j.succ.succ) = 0
have neg₂ : Fin.succ 0 < j.succ.succ
Tactic: rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ n + 2 ≤ (↑(j.succ.succ.pred ⋯) : ℕ) + q
have neg : n + 2 ≤ (↑j : ℕ) + 1 + q
Tactic: dsimp
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
⊢ (φ ≫
        (HAdd.hAdd (α :=
              Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (AlternatingFaceMapComplex.obj X)
                (AlternatingFaceMapComplex.obj X))
              (𝟙 (AlternatingFaceMapComplex.obj X)) (Hσ q)).f
          (n + 1)) ≫
      X.δ j.succ =
    0
have dsimp : (φ ≫ HAdd.hAdd (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌) (𝟙 (X _⦋n + 1⦌)) (HomologicalComplex.Hom.f (Hσ q) (n + 1))) ≫ X.δ j.succ =
  0
Tactic: dsimp
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
⊢ (φ ≫ HAdd.hAdd (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌) (𝟙 (X _⦋n + 1⦌)) (HomologicalComplex.Hom.f (Hσ q) (n + 1))) ≫
      X.δ j.succ =
    0
have simp : φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
Tactic: simp only [comp_add, add_comp, comp_id]
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
⊢ φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
have pos : ∀ (hqn : n < q), φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
Tactic: by_cases! hqn : n < q
-- 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
pos : ∀ (hqn : n < q), φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
⊢ φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
have neg : ∀ (hqn : q ≤ n), φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
Tactic: by_cases! hqn : n < q