awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
neg :
  HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i) ≫
          (P q ≫
                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 + 1) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (Q q) n.succ ≫ X.σ i) ≫
          (P q ≫
                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 + 1) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) =
    0
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))

Tactic:
rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp,
          P_succ]

Premises used: AlgebraicTopology.DoldKan.P_succ, CategoryTheory.Preadditive.add_comp, Nat.succ, AlgebraicTopology.DoldKan.P_add_Q_f, CategoryTheory.Category.id_comp, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
⊢ HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)

Tactic:
have v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i) :=
          (HigherFacesVanish.of_P q n).comp_σ hi
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
neg :
  HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (P q) (n + 1) ≫ X.σ i) ≫
          HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
            HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
              (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (Q q) (n + 1) ≫ X.σ i) ≫
          HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
            HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
              (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) =
    0
⊢ HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i) ≫
          (P q ≫
                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 + 1) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (Q q) n.succ ≫ X.σ i) ≫
          (P q ≫
                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 + 1) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) =
    0

Tactic:
dsimp only [AlternatingFaceMapComplex.obj_X, Nat.succ_eq_add_one, HomologicalComplex.comp_f,
          HomologicalComplex.add_f_apply, HomologicalComplex.id_f]

Premises used: Nat.succ_eq_add_one, HomologicalComplex.add_f_apply, HomologicalComplex.id_f, HomologicalComplex.comp_f, AlgebraicTopology.AlternatingFaceMapComplex.obj_X
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
neg :
  ∀ (x : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} x →
      ((HomologicalComplex.Hom.f (P (↑x : ℕ)) (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.rev) ≫ X.σ i) ≫
          HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
            HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
              (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
        0
⊢ HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (P q) (n + 1) ≫ X.σ i) ≫
          HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
            HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
              (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (Q q) (n + 1) ≫ X.σ i) ≫
          HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
            HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
              (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) =
    0

Tactic:
rw [← assoc, v.comp_P_eq_self, Preadditive.comp_add,
          comp_id, v.comp_Hσ_eq hi, assoc, ← Fin.succ_mk _ _ i.2,
          SimplicialObject.δ_comp_σ_succ_assoc,
          Fin.eta, decomposition_Q n q, sum_comp, sum_comp, Finset.sum_eq_zero, add_zero,
          add_neg_eq_zero]

Premises used: CategoryTheory.Category.assoc, add_neg_eq_zero, Finset.sum_eq_zero, Fin.isLt, CategoryTheory.Preadditive.sum_comp, Fin.eta, CategoryTheory.Category.comp_id, Fin.succ_mk, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self, CategoryTheory.Preadditive.comp_add, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, AlgebraicTopology.DoldKan.decomposition_Q, add_zero, CategoryTheory.SimplicialObject.δ_comp_σ_succ_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} j
⊢ True ∧ (↑j : ℕ) < q

Tactic:
simp only [Finset.mem_univ, Finset.mem_filter] at hj

Premises used: Finset.mem_univ, Finset.mem_filter
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
neg :
  ∀ (k : ℕ) (hk : (↑j : ℕ) + k = n),
    ((HomologicalComplex.Hom.f (P (↑j : ℕ)) (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
        HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
          HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
            (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
      0
⊢ ((HomologicalComplex.Hom.f (P (↑j : ℕ)) (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
        HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
          (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
    0

Tactic:
obtain ⟨k, hk⟩ := Nat.le.dest (Nat.lt_succ_iff.mp (Fin.is_lt j))

Premises used: Fin.is_lt, Nat.lt_succ_iff, Iff.mp, Nat.le.dest
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : (↑j : ℕ) + k = n
⊢ k + (↑j : ℕ) = n

Tactic:
rw [add_comm] at hk

Premises used: add_comm
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
⊢ (↑i : ℕ) < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
h₁ : (↑i : ℕ) = (↑(⟨(↑i : ℕ), ⋯⟩ : Fin (n + 1)).castSucc : ℕ)
⊢ i = ⟨(↑i : ℕ), ⋯⟩.castSucc

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
⊢ (↑i : ℕ) = (↑(⟨(↑i : ℕ), ⋯⟩ : Fin (n + 1)).castSucc : ℕ)

Tactic:
simp only [Fin.castSucc_mk, Fin.eta]

Premises used: Fin.eta, Fin.castSucc_mk
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
⊢ i = ⟨(↑i : ℕ), ⋯⟩.castSucc

Tactic:
have hi' : i = Fin.castSucc ⟨i, by lia⟩ := by
          ext
          simp only [Fin.castSucc_mk, Fin.eta]
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
hi' : i = ⟨(↑i : ℕ), ⋯⟩.castSucc
simp : k + (↑j : ℕ) + 1 + 1 ≤ k + 1 + q
⊢ n + 1 + 1 ≤ (↑j.rev.succ : ℕ) + q

Tactic:
simp only [← hk, Fin.rev_eq j hk.symm, Fin.succ_mk, Fin.val_mk]

Premises used: Fin.rev_eq, Fin.val_mk, Fin.succ_mk, Eq.symm
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
hi' : i = ⟨(↑i : ℕ), ⋯⟩.castSucc
⊢ k + (↑j : ℕ) + 1 + 1 ≤ k + 1 + q

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
hi' : i = ⟨(↑i : ℕ), ⋯⟩.castSucc
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (X.σ j.rev.succ ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))

Tactic:
have eq := hq j.rev.succ (by
          simp only [← hk, Fin.rev_eq j hk.symm, Fin.succ_mk, Fin.val_mk]
          lia)
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
hi' : i = ⟨(↑i : ℕ), ⋯⟩.castSucc
eq :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (X.σ j.rev.succ ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
neg : (⟨(↑i : ℕ), ⋯⟩ : Fin (n + 1)) ≤ j.rev
⊢ ((HomologicalComplex.Hom.f (P (↑j : ℕ)) (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
        HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
          (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
    0

Tactic:
rw [assoc, assoc, assoc, hi',
          SimplicialObject.σ_comp_σ_assoc, reassoc_of% eq, zero_comp, comp_zero, comp_zero,
          comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.SimplicialObject.σ_comp_σ_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
hi' : i = ⟨(↑i : ℕ), ⋯⟩.castSucc
eq :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (X.σ j.rev.succ ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
neg : (↑i : ℕ) ≤ k
⊢ (⟨(↑i : ℕ), ⋯⟩ : Fin (n + 1)) ≤ j.rev

Tactic:
simp only [Fin.rev_eq j hk.symm, Fin.le_iff_val_le_val]

Premises used: Fin.rev_eq, Eq.symm, Fin.le_iff_val_le_val
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
hi' : i = ⟨(↑i : ℕ), ⋯⟩.castSucc
eq :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (X.σ j.rev.succ ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
⊢ (↑i : ℕ) ≤ k

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
n : ℕ
i : Fin (n + 1)
rw : n + 1 ≤ (↑i : ℕ) + (n + 1)
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))

Tactic:
rw [PInfty_f, σ_comp_P_eq_zero X i]

Premises used: AlgebraicTopology.DoldKan.PInfty_f, AlgebraicTopology.DoldKan.σ_comp_P_eq_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
n : ℕ
i : Fin (n + 1)
⊢ n + 1 ≤ (↑i : ℕ) + (n + 1)

Tactic:
simp only [le_add_iff_nonneg_left, zero_le]

Premises used: zero_le, le_add_iff_nonneg_left
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
n : ℕ
Δ' : SimplexCategory
θ : ⦋n⦌ ⟶ Δ'
hθ : ¬Mono θ
⊢ ¬Function.Injective (α := Fin (⦋n⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ'.len + 1))

Tactic:
rw [SimplexCategory.mono_iff_injective] at hθ

Premises used: SimplexCategory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
n : ℕ
Δ' : SimplexCategory
θ : ⦋n⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ'.len + 1))
zero :
  ∀ (θ : ⦋0⦌ ⟶ Δ')
    (hθ :
      ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
          (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))),
    Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋0⦌)
      (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty 0 : X.obj (Opposite.op Δ') ⟶ X _⦋0⦌)
      (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0)
succ :
  ∀ (n : ℕ) (θ : ⦋n + 1⦌ ⟶ Δ')
    (hθ :
      ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
          (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))),
    Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
      (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
      (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty n : X.obj (Opposite.op Δ') ⟶ X _⦋n⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n)

Tactic:
cases n