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 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
pos₂ pos₃ : Eq.{v_1 + 1} (α := 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

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

Premises used: CategoryTheory.Limits.comp_zero, HAdd.hAdd, AlgebraicTopology.DoldKan.c_mk, AlgebraicTopology.DoldKan.hσ'_eq_zero, CategoryTheory.Limits.zero_comp, 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
hqn' : ¬n + 1 < q
⊢ n + 1 = 0 + q

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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
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
⊢ 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:
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]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, pow_zero, CategoryTheory.Preadditive.comp_sum, one_zsmul, HAdd.hAdd, AlgebraicTopology.DoldKan.c_mk, AlgebraicTopology.DoldKan.hσ'_eq, OfNat.ofNat, rfl, Fin.mk_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 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
neg₁ : ∀ (a : Fin (n + 1)), φ ≫ X.σ 0 ≫ (HPow.hPow (α := ℤ) (-1) (↑a.succ.succ : ℕ) • X.δ a.succ.succ) = 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

Tactic:
rw [Fin.sum_univ_succ, Fin.sum_univ_succ, Fintype.sum_eq_zero, add_zero]

Premises used: Fintype.sum_eq_zero, add_zero, Fin.sum_univ_succ
-- 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
hqn' : ¬n + 1 < q
⊢ φ ≫ 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:
simp only [Fin.val_zero, Fin.val_succ, Fin.val_castSucc, zero_add, pow_zero, one_smul,
        pow_one, neg_smul, comp_neg, ← Fin.castSucc_zero (n := n + 2), δ_comp_σ_self, δ_comp_σ_succ,
        add_neg_cancel]

Premises used: add_neg_cancel, neg_smul, CategoryTheory.Preadditive.comp_neg, Fin.val_succ, zero_add, pow_zero, one_smul, CategoryTheory.SimplicialObject.δ_comp_σ_self, Fin.castSucc_zero, CategoryTheory.SimplicialObject.δ_comp_σ_succ, pow_one, Fin.val_zero, Fin.val_castSucc
-- 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
hqn' : ¬n + 1 < q
j : Fin (n + 1)
neg : j.succ.succ.pred ⋯ ≠ 0
neg₁ : n + 2 ≤ (↑(j.succ.succ.pred ⋯) : ℕ) + q
neg₂ : Fin.succ 0 < j.succ.succ
⊢ φ ≫ X.σ 0 ≫ (HPow.hPow (α := ℤ) (-1) (↑j.succ.succ : ℕ) • X.δ j.succ.succ) = 0

Tactic:
rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]

Premises used: zsmul_zero, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero_assoc, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt', CategoryTheory.Limits.zero_comp
-- 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
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ j.succ.succ.pred ⋯ ≠ 0

Tactic:
simp [Fin.succ_ne_zero]

Premises used: Fin.succ_ne_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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
neg : n + 2 ≤ (↑j : ℕ) + 1 + q
⊢ n + 2 ≤ (↑(j.succ.succ.pred ⋯) : ℕ) + q

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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ n + 2 ≤ (↑j : ℕ) + 1 + q

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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ Fin.succ 0 < j.succ.succ

Tactic:
simp only [Fin.succ_lt_succ_iff, j.succ_pos]

Premises used: Fin.succ_lt_succ_iff, Fin.succ_pos
-- 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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
dsimp :
  (φ ≫ HAdd.hAdd (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌) (𝟙 (X _⦋n + 1⦌)) (HomologicalComplex.Hom.f (Hσ q) (n + 1))) ≫
      X.δ j.succ =
    0
⊢ (φ ≫
        (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

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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
simp : φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
⊢ (φ ≫ HAdd.hAdd (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌) (𝟙 (X _⦋n + 1⦌)) (HomologicalComplex.Hom.f (Hσ q) (n + 1))) ≫
      X.δ j.succ =
    0

Tactic:
simp only [comp_add, add_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add
-- 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 φ
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
neg : ∀ (hqn : q ≤ n), φ ≫ 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

Tactic:
by_cases! hqn : n < q
-- 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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : n < q
⊢ n + 1 ≤ (↑j : ℕ) + q

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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : n < q
pos : φ ≫ X.δ j.succ + 0 ≫ X.δ j.succ = 0
pos₁ : φ ≫ X.δ j.succ + 0 = 0
pos₂ : φ ≫ X.δ j.succ = 0
pos₃ pos₄ : Eq.{v_1 + 1} (α := Y ⟶ X _⦋n⦌) 0 0
⊢ φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0

Tactic:
rw [v.comp_Hσ_eq_zero hqn, zero_comp, add_zero, v j (by lia)]

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, CategoryTheory.Limits.zero_comp, 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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ n
neg : ∀ (a : ℕ) (ha : q + a = n), φ ≫ 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

Tactic:
obtain ⟨a, ha⟩ := Nat.le.dest hqn

Premises used: Nat.le.dest
-- 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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ n = a + q

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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
neg : φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) ≫ X.δ j.succ
⊢ φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0

Tactic:
rw [v.comp_Hσ_eq (show n = a + q by lia), neg_comp, add_neg_eq_zero, assoc, assoc]

Premises used: CategoryTheory.Category.assoc, add_neg_eq_zero, CategoryTheory.Preadditive.neg_comp, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq
-- 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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
neg :
  ∀ {φ : Y ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌} (v : HigherFacesVanish q φ) (j : Fin (HAdd.hAdd (α := ℕ) 0 1))
    (hj₁ : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑j : ℕ) + (q + 1)) (hqn : q ≤ 0) (ha : q + a = 0),
    φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) ≫ X.δ j.succ
neg₁ :
  ∀ (m : ℕ) {φ : Y ⟶ X _⦋m + 1 + 1⦌} (v : HigherFacesVanish q φ) (j : Fin (m + 1 + 1))
    (hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)) (hqn : q ≤ m + 1) (ha : q + a = m + 1),
    φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) ≫ X.δ j.succ

Tactic:
rcases n with - | m
-- 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
q a : ℕ
φ : Y ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌
v : HigherFacesVanish q φ
j : Fin (HAdd.hAdd (α := ℕ) 0 1)
hj₁ : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ 0
ha : q + a = 0
neg : φ ≫ X.δ (Fin.succ 0) = φ ≫ X.δ ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) ≫ X.δ j.succ

Tactic:
simp only [Nat.eq_zero_of_add_eq_zero_left ha, Fin.eq_zero j, Fin.mk_zero,
      δ_comp_σ_succ, comp_id]

Premises used: CategoryTheory.Category.comp_id, Nat.eq_zero_of_add_eq_zero_left, Fin.eq_zero, CategoryTheory.SimplicialObject.δ_comp_σ_succ, Fin.mk_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
q a : ℕ
φ : Y ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌
v : HigherFacesVanish q φ
j : Fin (HAdd.hAdd (α := ℕ) 0 1)
hj₁ : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ 0
ha : q + a = 0
⊢ φ ≫ X.δ (Fin.succ 0) = φ ≫ X.δ ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩

Tactic:
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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
pos : ∀ (hj₂ : a = (↑j : ℕ)), φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
neg : ∀ (hj₂ : ¬a = (↑j : ℕ)), φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ

Tactic:
by_cases hj₂ : a = (j : ℕ)

Premises used: Fin.val
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : a = (↑j : ℕ)
pos : φ ≫ X.δ j.succ = φ ≫ X.δ ⟨(↑j : ℕ) + 1, ⋯⟩
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ

Tactic:
simp only [hj₂, Fin.eta, δ_comp_σ_succ, comp_id]

Premises used: Fin.eta, CategoryTheory.Category.comp_id, CategoryTheory.SimplicialObject.δ_comp_σ_succ
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : a = (↑j : ℕ)
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨(↑j : ℕ) + 1, ⋯⟩

Tactic:
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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
⊢ a ≤ (↑j : ℕ)

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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
⊢ a < (↑j : ℕ)

Tactic:
have haj : a < j := (Ne.le_iff_lt hj₂).mp (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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
⊢ a ≤ m

Tactic:
grind
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
⊢ a ≤ m

Tactic:
have ham : a ≤ m := by grind
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
neg : φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)
neg₁ : Fin.succ ⟨a, ⋯⟩ < j.succ
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ

Tactic:
rw [X.δ_comp_σ_of_gt', j.pred_succ]

Premises used: Fin.pred_succ, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
⊢ (↑(Fin.succ (⟨a, ⋯⟩ : Fin (m + 1 + 1))) : ℕ) < (↑j.succ : ℕ)

Tactic:
simpa only [Fin.val_mk, Fin.val_succ, add_lt_add_iff_right] using haj

Premises used: Fin.val_mk, Fin.val_succ, add_lt_add_iff_right
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
neg : a < m → φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)
neg₁ :
  ∀ (ham'' : a = m),
    φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)

Tactic:
obtain _ | ham'' := ham.lt_or_eq

Premises used: LE.le.lt_or_eq
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
h : a < m
neg :
  φ ≫ X.δ j.succ =
    φ ≫ X.δ j.succ ≫ X.δ (Fin.castLT (⟨a + 1, ⋯⟩ : Fin (m + 1 + 2)) ⋯) ≫ X.σ (Fin.castLT (m := m + 2) ⟨a, ⋯⟩ ⋯)
neg₁ : ⟨a + 1, ⋯⟩ ≤ j.castSucc
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)

Tactic:
rw [← X.δ_comp_δ''_assoc]

Premises used: CategoryTheory.SimplicialObject.δ_comp_δ''_assoc
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
h : a < m
neg : a + 1 ≤ (↑j : ℕ)
⊢ (↑(⟨a + 1, ⋯⟩ : Fin (m + 1 + 2)) : ℕ) ≤ (↑j.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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
h : a < m
⊢ a + 1 ≤ (↑j : ℕ)

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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
h : a < m
⊢ m + 1 + 1 ≤ (↑j : ℕ) + q

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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
h : a < m
⊢ φ ≫ X.δ j.succ =
    φ ≫ X.δ j.succ ≫ X.δ (Fin.castLT (⟨a + 1, ⋯⟩ : Fin (m + 1 + 2)) ⋯) ≫ X.σ (Fin.castLT (m := m + 2) ⟨a, ⋯⟩ ⋯)

Tactic:
simp only [← assoc, v j (by lia), zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.zero_comp
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
ham'' : a = m
neg : φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) ⟨a, ⋯⟩ ⋯)
neg₁ : ⟨a + 1, ⋯⟩ = j.castSucc
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)

Tactic:
rw [X.δ_comp_δ_self'_assoc]

Premises used: CategoryTheory.SimplicialObject.δ_comp_δ_self'_assoc
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
ham'' : a = m
neg : (↑(⟨a + 1, ⋯⟩ : Fin (m + 1 + 2)) : ℕ) = (↑j.castSucc : ℕ)
⊢ ⟨a + 1, ⋯⟩ = j.castSucc

Tactic:
ext
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
ham'' : a = m
neg :
  ∀ (val : ℕ) (isLt : val < m + 1 + 1) (hj₁ : m + 1 + 1 ≤ (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)) : ℕ) + (q + 1))
    (hj₂ : ¬a = (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)) : ℕ)) (haj : a < (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)) : ℕ)),
    (↑(⟨a + 1, ⋯⟩ : Fin (m + 1 + 2)) : ℕ) = (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)).castSucc : ℕ)
⊢ (↑(⟨a + 1, ⋯⟩ : Fin (m + 1 + 2)) : ℕ) = (↑j.castSucc : ℕ)

Tactic:
cases j
-- 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
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
hqn : q ≤ m + 1
ha : q + a = m + 1
ham : a ≤ m
ham'' : a = m
val : ℕ
isLt : val < m + 1 + 1
hj₁ : m + 1 + 1 ≤ (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)) : ℕ) + (q + 1)
hj₂ : ¬a = (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)) : ℕ)
haj : a < (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)) : ℕ)
neg : a + 1 = val
⊢ (↑(⟨a + 1, ⋯⟩ : Fin (m + 1 + 2)) : ℕ) = (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)).castSucc : ℕ)

Tactic:
dsimp