awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (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
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 :
  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)
⊢ HomologicalComplex.Hom.f (P (↑q' : ℕ)) (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev +
      ∑ x ∈ Finset.erase {i : Fin (n + 1) | (↑i : ℕ) < q + 1} q',
        HomologicalComplex.Hom.f (P (↑x : ℕ)) (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.rev =
    HAdd.hAdd (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (-HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1))
      (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
have neg₁ : Finset.erase {i : Fin (n + 1) | (↑i : ℕ) < q + 1} q' = {i : Fin (n + 1) | (↑i : ℕ) < q}
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (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
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, ⋯⟩
⊢ 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)
have hnaq' : n = a + q
Tactic: have hnaq' : n = a + q := by lia
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (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
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
⊢ 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)
have neg : Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ X _⦋n + 1⦌)
  (HomologicalComplex.Hom.f (P (↑q' : ℕ)) (n + 1) ≫ X.δ (Fin.succ (⟨a, sorry⟩ : Fin (n + 1))) ≫ X.σ ⟨a, sorry⟩)
  (HomologicalComplex.Hom.f (P q) (n + 1) ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)))
Tactic: simp only [(HigherFacesVanish.of_P q n).comp_Hσ_eq hnaq', q'.rev_eq hnaq', neg_neg]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (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
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, ⋯⟩
⊢ Finset.erase {i : Fin (n + 1) | (↑i : ℕ) < q + 1} q' = {i : Fin (n + 1) | (↑i : ℕ) < q}
have 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))
Tactic: ext ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (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
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, 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))
have neg : ¬i = q ∧ i < q + 1 ↔ i < q
Tactic: simp_rw [Finset.mem_erase, Finset.mem_filter_univ, q', ne_eq, Fin.mk.injEq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (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
n q : ℕ
⊢ 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)
have 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)
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
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (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
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)
⊢ 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)
have 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)
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
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (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
n : ℕ
⊢ (id X n).φ = 𝟙 (X _⦋n + 1⦌)
have 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))
Tactic: simp only [← P_add_Q_f (n + 1) (n + 1), φ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (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
n : ℕ
⊢ 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))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (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
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))
⊢ 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))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (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
n : ℕ
Z Z' : C
f : MorphComponents X n Z
h : Z ⟶ Z'
⊢ (f.postComp h).φ = f.φ ≫ h
have 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
Tactic: unfold φ postComp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (goal)
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
⊢ (f.preComp g).φ = g.app (op ⦋n + 1⦌) ≫ f.φ
have 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)
Tactic: unfold φ preComp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (goal)
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
⊢ 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)
have 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
Tactic: simp only [PInfty_f, comp_add]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (goal)
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
⊢ 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
have 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
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Decomposition (goal)
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
⊢ 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
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ (φ ≫ X.σ (⟨b, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ j.succ = 0
have rw : j ≠ 0
Tactic: rw [assoc, SimplicialObject.δ_comp_σ_of_gt', Fin.pred_succ, v.comp_δ_eq_zero_assoc _ _ hj,
    zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ (φ ≫ X.σ (⟨b, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ j.succ = 0
have H : (⟨b, sorry⟩ : Fin (n + 1 + 1)).succ < j.succ
Tactic: rw [assoc, SimplicialObject.δ_comp_σ_of_gt', Fin.pred_succ, v.comp_δ_eq_zero_assoc _ _ hj,
    zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ (⟨b + 1, ⋯⟩ : Fin (n + 2 + 1)) < j.succ
have H : (↑(⟨b + 1, sorry⟩ : Fin (n + 2 + 1)) : ℕ) < (↑j : ℕ) + 1
Tactic: rw [Fin.lt_def, Fin.val_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ (↑(⟨b + 1, ⋯⟩ : Fin (n + 2 + 1)) : ℕ) < (↑j : ℕ) + 1
have linarith : (↑j : ℕ) + 1 ≤ (↑(⟨b + 1, sorry⟩ : 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
n q : ℕ
hq :
  ∀ (i : Fin (n + 1)) (hi : n + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
i : Fin (n + 1)
hi : n + 1 ≤ (↑i : ℕ) + (q + 1)
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have pos : ∀ (h : n + 1 ≤ (↑i : ℕ) + q),
  Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
Tactic: by_cases h : n + 1 ≤ (i : ℕ) + q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
n q : ℕ
hq :
  ∀ (i : Fin (n + 1)) (hi : n + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
i : Fin (n + 1)
hi : n + 1 ≤ (↑i : ℕ) + (q + 1)
pos :
  ∀ (h : n + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have neg : ∀ (h : ¬n + 1 ≤ (↑i : ℕ) + q),
  Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
Tactic: by_cases h : n + 1 ≤ (i : ℕ) + q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
n q : ℕ
hq :
  ∀ (i : Fin (n + 1)) (hi : n + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
i : Fin (n + 1)
hi : n + 1 ≤ (↑i : ℕ) + (q + 1)
h : n + 1 ≤ (↑i : ℕ) + q
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have pos : 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) =
  0
Tactic: rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]