awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 q : ℕ
hq :
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (HomologicalComplex.Hom.f (Q q) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ n = a + q

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 q : ℕ
hq :
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (HomologicalComplex.Hom.f (Q q) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ n = a + q

Tactic:
have hnaq' : n = a + q := by lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 q : ℕ
hq :
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (HomologicalComplex.Hom.f (Q q) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
hnaq' : n = a + q
neg :
  Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ X _⦋n + 1⦌)
    (HomologicalComplex.Hom.f (P (↑q' : ℕ)) (n + 1) ≫ X.δ (Fin.succ (⟨a, ⋯⟩ : Fin (n + 1))) ≫ X.σ ⟨a, ⋯⟩)
    (HomologicalComplex.Hom.f (P q) (n + 1) ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
⊢ HomologicalComplex.Hom.f (P (↑q' : ℕ)) (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)

Tactic:
simp only [(HigherFacesVanish.of_P q n).comp_Hσ_eq hnaq', q'.rev_eq hnaq', neg_neg]

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, Fin.rev_eq, neg_neg, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 q : ℕ
hq :
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (HomologicalComplex.Hom.f (Q q) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
hnaq' : n = a + q
⊢ Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ X _⦋n + 1⦌)
    (HomologicalComplex.Hom.f (P (↑q' : ℕ)) (n + 1) ≫ X.δ (Fin.succ (⟨a, ⋯⟩ : Fin (n + 1))) ≫ X.σ ⟨a, ⋯⟩)
    (HomologicalComplex.Hom.f (P q) (n + 1) ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 q : ℕ
hq :
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (HomologicalComplex.Hom.f (Q q) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
neg :
  ∀ (i : ℕ) (hi : i < n + 1),
    (⟨i, hi⟩ : Fin (n + 1)) ∈ Finset.erase {i : Fin (n + 1) | (↑i : ℕ) < q + 1} q' ↔
      Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} (⟨i, hi⟩ : Fin (n + 1))
⊢ Finset.erase {i : Fin (n + 1) | (↑i : ℕ) < q + 1} q' = {i : Fin (n + 1) | (↑i : ℕ) < q}

Tactic:
ext ⟨i, hi⟩
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 q : ℕ
hq :
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (HomologicalComplex.Hom.f (Q q) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
neg : ¬i = q ∧ i < q + 1 ↔ i < q
⊢ (⟨i, hi⟩ : Fin (n + 1)) ∈ Finset.erase {i : Fin (n + 1) | (↑i : ℕ) < q + 1} q' ↔
    Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} (⟨i, hi⟩ : Fin (n + 1))

Tactic:
simp_rw [Finset.mem_erase, Finset.mem_filter_univ, q', ne_eq, Fin.mk.injEq]

Premises used: Fin.mk.injEq, Finset.mem_filter_univ, ne_eq, Finset.mem_erase
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 q : ℕ
hq :
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (HomologicalComplex.Hom.f (Q q) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ¬i = q ∧ i < q + 1 ↔ i < q

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 q : ℕ
zero :
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (HomologicalComplex.Hom.f (Q 0) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < 0, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
succ :
  ∀ (q : ℕ)
    (hq :
      Eq.{v_1 + 1} (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.Hom.f (Q q) (n + 1))
        (∑ i : Fin (n + 1) with (↑i : ℕ) < q,
          HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (HomologicalComplex.Hom.f (Q (q + 1)) (n + 1))
      (∑ i : Fin (n + 1) with (↑i : ℕ) < q + 1,
        HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (HomologicalComplex.Hom.f (Q q) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)

Tactic:
induction q with
  | zero =>
    simp only [Q_zero, HomologicalComplex.zero_f_apply, Nat.not_lt_zero,
      Finset.filter_false, Finset.sum_empty]
  | succ q hq =>
    by_cases! hqn : n < q
    · rw [Q_is_eventually_constant (show n + 1 ≤ q by lia), hq]
      congr 1
      ext ⟨x, hx⟩
      simp_rw [Finset.mem_filter_univ]
      lia
    · obtain ⟨a, ha⟩ := Nat.le.dest hqn
      rw [Q_succ, HomologicalComplex.sub_f_apply, HomologicalComplex.comp_f, hq]
      symm
      conv_rhs => rw [sub_eq_add_neg, add_comm]
      let q' : Fin (n + 1) := ⟨q, Nat.lt_succ_of_le hqn⟩
      rw [← @Finset.add_sum_erase _ _ _ _ _ _ q' (by simp [q'])]
      congr
      · have hnaq' : n = a + q := by lia
        simp only [(HigherFacesVanish.of_P q n).comp_Hσ_eq hnaq', q'.rev_eq hnaq', neg_neg]
        rfl
      · ext ⟨i, hi⟩
        simp_rw [Finset.mem_erase, Finset.mem_filter_univ, q', ne_eq, Fin.mk.injEq]
        lia

Premises used: Fin.mk.injEq, Finset.filter_false, Finset.mem_filter_univ, HomologicalComplex.sub_f_apply, sub_eq_add_neg, neg_neg, HomologicalComplex.comp_f, ne_eq, add_comm, Finset.mem_erase, AlgebraicTopology.DoldKan.Q_is_eventually_constant, HomologicalComplex.zero_f_apply, AlgebraicTopology.DoldKan.Q_succ, Nat.not_lt_zero, Finset.sum_empty, AlgebraicTopology.DoldKan.Q_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 : ℕ
simp :
  HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ X _⦋n + 1⦌)
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (id X n).a)
      (∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev) =
    HAdd.hAdd (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (HomologicalComplex.Hom.f (P (n + 1)) (n + 1)) (HomologicalComplex.Hom.f (Q (n + 1)) (n + 1))
⊢ (id X n).φ = 𝟙 (X _⦋n + 1⦌)

Tactic:
simp only [← P_add_Q_f (n + 1) (n + 1), φ]

Premises used: HAdd.hAdd, OfNat.ofNat, AlgebraicTopology.DoldKan.MorphComponents.φ, AlgebraicTopology.DoldKan.P_add_Q_f
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 : ℕ
e_a :
  Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ X _⦋n + 1⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (id X n).a) (HomologicalComplex.Hom.f (P (n + 1)) (n + 1))
e_a₁ :
  Eq.{v_1 + 1} (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ X _⦋n + 1⦌)
    (∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev)
    (HomologicalComplex.Hom.f (Q (n + 1)) (n + 1))
⊢ HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ X _⦋n + 1⦌)
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (id X n).a)
      (∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev) =
    HAdd.hAdd (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (HomologicalComplex.Hom.f (P (n + 1)) (n + 1)) (HomologicalComplex.Hom.f (Q (n + 1)) (n + 1))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 : ℕ
⊢ Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ X _⦋n + 1⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (id X n).a) (HomologicalComplex.Hom.f (P (n + 1)) (n + 1))

Tactic:
simp only [id, PInfty_f, P_f_idem]

Premises used: AlgebraicTopology.DoldKan.P_f_idem, AlgebraicTopology.DoldKan.PInfty_f, AlgebraicTopology.DoldKan.MorphComponents.id
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ X _⦋n + 1⦌)
    (∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev)
    (∑ i : Fin (n + 1) with (↑i : ℕ) < n + 1,
      HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ X _⦋n + 1⦌)
    (∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev)
    (HomologicalComplex.Hom.f (Q (n + 1)) (n + 1))

Tactic:
exact Eq.trans (by simp) (decomposition_Q n (n + 1)).symm

Premises used: HAdd.hAdd, AlgebraicTopology.DoldKan.decomposition_Q, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 : ℕ
Z Z' : C
f : MorphComponents X n Z
h : Z ⟶ Z'
unfold :
  HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ Z')
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫
        { a := f.a ≫ h, b := fun (i : Fin (n + 1)) ↦ f.b i ≫ h : MorphComponents X n Z' }.a)
      (∑ i : Fin (n + 1),
        HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫
          X.δ i.rev.succ ≫ { a := f.a ≫ h, b := fun (i : Fin (n + 1)) ↦ f.b i ≫ h : MorphComponents X n Z' }.b i.rev) =
    HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ Z)
        (HomologicalComplex.Hom.f PInfty (n + 1) ≫ f.a)
        (∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev) ≫
      h
⊢ (f.postComp h).φ = f.φ ≫ h

Tactic:
unfold φ postComp

Premises used: AlgebraicTopology.DoldKan.MorphComponents.postComp, AlgebraicTopology.DoldKan.MorphComponents.φ
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
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 : ℕ
Z Z' : C
f : MorphComponents X n Z
h : Z ⟶ Z'
⊢ HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ Z')
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫
        { a := f.a ≫ h, b := fun (i : Fin (n + 1)) ↦ f.b i ≫ h : MorphComponents X n Z' }.a)
      (∑ i : Fin (n + 1),
        HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫
          X.δ i.rev.succ ≫ { a := f.a ≫ h, b := fun (i : Fin (n + 1)) ↦ f.b i ≫ h : MorphComponents X n Z' }.b i.rev) =
    HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ Z)
        (HomologicalComplex.Hom.f PInfty (n + 1) ≫ f.a)
        (∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev) ≫
      h

Tactic:
simp only [add_comp, sum_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.sum_comp, CategoryTheory.Preadditive.add_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X X' : SimplicialObject.{v_1, u_1} C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
unfold :
  HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X') (n + 1) ⟶ Z)
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫
        { a := g.app (op ⦋n + 1⦌) ≫ f.a, b := fun (i : Fin (n + 1)) ↦ g.app (op ⦋n⦌) ≫ f.b i :
            MorphComponents X' n Z }.a)
      (∑ i : Fin (n + 1),
        HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫
          X'.δ i.rev.succ ≫
            { a := g.app (op ⦋n + 1⦌) ≫ f.a, b := fun (i : Fin (n + 1)) ↦ g.app (op ⦋n⦌) ≫ f.b i :
                  MorphComponents X' n Z }.b
              i.rev) =
    g.app (op ⦋n + 1⦌) ≫
      HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ Z)
        (HomologicalComplex.Hom.f PInfty (n + 1) ≫ f.a)
        (∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev)
⊢ (f.preComp g).φ = g.app (op ⦋n + 1⦌) ≫ f.φ

Tactic:
unfold φ preComp

Premises used: AlgebraicTopology.DoldKan.MorphComponents.preComp, AlgebraicTopology.DoldKan.MorphComponents.φ
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X X' : SimplicialObject.{v_1, u_1} C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
simp :
  HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X') (n + 1) ⟶ Z)
      (HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ g.app (op ⦋n + 1⦌) ≫ f.a)
      (∑ x : Fin (n + 1),
        HomologicalComplex.Hom.f (P (↑x : ℕ)) (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev) =
    g.app (op ⦋n + 1⦌) ≫ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ f.a +
      g.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev
⊢ HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X') (n + 1) ⟶ Z)
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫
        { a := g.app (op ⦋n + 1⦌) ≫ f.a, b := fun (i : Fin (n + 1)) ↦ g.app (op ⦋n⦌) ≫ f.b i :
            MorphComponents X' n Z }.a)
      (∑ i : Fin (n + 1),
        HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫
          X'.δ i.rev.succ ≫
            { a := g.app (op ⦋n + 1⦌) ≫ f.a, b := fun (i : Fin (n + 1)) ↦ g.app (op ⦋n⦌) ≫ f.b i :
                  MorphComponents X' n Z }.b
              i.rev) =
    g.app (op ⦋n + 1⦌) ≫
      HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ Z)
        (HomologicalComplex.Hom.f PInfty (n + 1) ≫ f.a)
        (∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev)

Tactic:
simp only [PInfty_f, comp_add]

Premises used: AlgebraicTopology.DoldKan.PInfty_f, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X X' : SimplicialObject.{v_1, u_1} C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
e_a :
  HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ g.app (op ⦋n + 1⦌) ≫ f.a =
    g.app (op ⦋n + 1⦌) ≫ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ f.a
e_a₁ :
  Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X') (n + 1) ⟶ Z)
    (∑ x : Fin (n + 1), HomologicalComplex.Hom.f (P (↑x : ℕ)) (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev)
    (g.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev)
⊢ HAdd.hAdd (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X') (n + 1) ⟶ Z)
      (HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ g.app (op ⦋n + 1⦌) ≫ f.a)
      (∑ x : Fin (n + 1),
        HomologicalComplex.Hom.f (P (↑x : ℕ)) (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev) =
    g.app (op ⦋n + 1⦌) ≫ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ f.a +
      g.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X X' : SimplicialObject.{v_1, u_1} C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ g.app (op ⦋n + 1⦌) ≫ f.a =
    g.app (op ⦋n + 1⦌) ≫ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ f.a

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X X' : SimplicialObject.{v_1, u_1} C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X') (n + 1) ⟶ Z)
    (∑ x : Fin (n + 1), HomologicalComplex.Hom.f (P (↑x : ℕ)) (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev)
    (g.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 1), HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev)

Tactic:
simp only [comp_sum, P_f_naturality_assoc, SimplicialObject.δ_naturality_assoc]

Premises used: AlgebraicTopology.DoldKan.P_f_naturality_assoc, CategoryTheory.Preadditive.comp_sum, CategoryTheory.SimplicialObject.δ_naturality_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
Y : C
X : SimplicialObject.{v_1, u_1} C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
⊢ b < n + 1 + 1

Tactic:
simp only [hnbq, Nat.lt_add_one_iff, le_add_iff_nonneg_right, zero_le]

Premises used: zero_le, le_add_iff_nonneg_right, Nat.lt_add_one_iff
-- 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
Y : C
X : SimplicialObject.{v_1, u_1} C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ (↑j : ℕ) + q
rw : j ≠ 0
H : (⟨b, ⋯⟩ : Fin (n + 1 + 1)).succ < j.succ
⊢ (φ ≫ X.σ (⟨b, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ j.succ = 0

Tactic:
rw [assoc, SimplicialObject.δ_comp_σ_of_gt', Fin.pred_succ, v.comp_δ_eq_zero_assoc _ _ hj,
    zero_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero_assoc, Fin.pred_succ, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt', 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
Y : C
X : SimplicialObject.{v_1, u_1} C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ (↑j : ℕ) + q
hj' : j = 0
⊢ False

Tactic:
simp only [hnbq, add_comm b, add_assoc, hj', Fin.val_zero, zero_add, add_le_iff_nonpos_right,
      nonpos_iff_eq_zero, add_eq_zero, false_and, reduceCtorEq] at hj

Premises used: reduceCtorEq, add_le_iff_nonpos_right, add_assoc, false_and, zero_add, add_comm, add_eq_zero, Fin.val_zero, nonpos_iff_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
Y : C
X : SimplicialObject.{v_1, u_1} C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ (↑j : ℕ) + q
H : (↑(⟨b + 1, ⋯⟩ : Fin (n + 2 + 1)) : ℕ) < (↑j : ℕ) + 1
⊢ (⟨b + 1, ⋯⟩ : Fin (n + 2 + 1)) < j.succ

Tactic:
rw [Fin.lt_def, Fin.val_succ]

Premises used: Fin.val_succ, Fin.lt_def
-- 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
Y : C
X : SimplicialObject.{v_1, u_1} C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ (↑j : ℕ) + q
linarith :
  (↑j : ℕ) + 1 ≤ (↑(⟨b + 1, ⋯⟩ : Fin (n + 2 + 1)) : ℕ) →
    -1 + -(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑q : ℤ)) +
          (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - HAdd.hAdd (α := ℤ) (↑(↑j : ℕ) : ℤ) (↑q : ℤ)) +
        (HAdd.hAdd (α := ℤ) (↑(↑j : ℕ) : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) =
      0
⊢ (↑(⟨b + 1, ⋯⟩ : Fin (n + 2 + 1)) : ℕ) < (↑j : ℕ) + 1

Tactic:
linarith
-- 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)
hi : n + 1 ≤ (↑i : ℕ) + 0
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P 0) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))

Tactic:
lia