awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
w : (equivalence hF hG).unitIso.hom.app = (equivalenceUnitIso hG ε).hom.app
⊢ (equivalence hF hG).unitIso.hom = (equivalenceUnitIso hG ε).hom

Tactic:
apply NatTrans.ext

Premises used: CategoryTheory.NatTrans.ext
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
w : ∀ (X : A), (equivalence hF hG).unitIso.hom.app X = (equivalenceUnitIso hG ε).hom.app X
⊢ (equivalence hF hG).unitIso.hom.app = (equivalenceUnitIso hG ε).hom.app

Tactic:
ext X
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
w :
  (equivalence₂ eB hF).unitIso.hom.app X ≫
      (((𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj (eB.inverse.obj (F.obj X))))) ≫
              eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X)))) ≫
            𝟙 (eA.inverse.obj (eA.functor.obj (G.obj (eB.inverse.obj (F.obj X)))))) ≫
          eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X)))) ≫
        𝟙 (G.obj (eB.inverse.obj (F.obj X))) =
    (equivalenceUnitIso hG ε).hom.app X
⊢ (equivalence hF hG).unitIso.hom.app X = (equivalenceUnitIso hG ε).hom.app X

Tactic:
dsimp [equivalence]

Premises used: AlgebraicTopology.DoldKan.Compatibility.equivalence
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ (equivalence₂ eB hF).unitIso.hom.app X ≫
      (((𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj (eB.inverse.obj (F.obj X))))) ≫
              eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X)))) ≫
            𝟙 (eA.inverse.obj (eA.functor.obj (G.obj (eB.inverse.obj (F.obj X)))))) ≫
          eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X)))) ≫
        𝟙 (G.obj (eB.inverse.obj (F.obj X))) =
    (equivalenceUnitIso hG ε).hom.app X

Tactic:
simp only [assoc, comp_id, equivalenceUnitIso_hom_app, equivalence₂_inverse, Functor.comp_obj,
    id_comp, equivalence₂UnitIso_eq eB hF, equivalence₂UnitIso_hom_app,
    ← eA.inverse.map_comp_assoc, assoc, ← hε, υ_hom_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, AlgebraicTopology.DoldKan.Compatibility.υ_hom_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_eq, AlgebraicTopology.DoldKan.Compatibility.equivalence₂_inverse, AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_hom_app, CategoryTheory.Category.id_comp, AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_hom_app, CategoryTheory.Equivalence.inverse
-- 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) ⟶
      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:
simp only [Q_zero, HomologicalComplex.zero_f_apply, Nat.not_lt_zero,
      Finset.filter_false, Finset.sum_empty]

Premises used: Finset.filter_false, HomologicalComplex.zero_f_apply, 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 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)
pos :
  ∀ (hqn : 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 + 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)
neg :
  ∀ (hqn : q ≤ n),
    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 + 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:
by_cases! hqn : n < q
-- 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 : n < q
⊢ n + 1 ≤ 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 : n < q
pos :
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
    (∑ 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 + 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:
rw [Q_is_eventually_constant (show n + 1 ≤ q by lia), hq]

Premises used: AlgebraicTopology.DoldKan.Q_is_eventually_constant
-- 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 : n < q
pos : Eq (α := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} {i : Fin (n + 1) | (↑i : ℕ) < q + 1}
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q + 1,
      HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ 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 : 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 : n < q
pos :
  ∀ (x : ℕ) (hx : x < n + 1),
    Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} (⟨x, hx⟩ : Fin (n + 1)) ↔
      Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q + 1} (⟨x, hx⟩ : Fin (n + 1))
⊢ Eq (α := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} {i : Fin (n + 1) | (↑i : ℕ) < q + 1}

Tactic:
ext ⟨x, hx⟩
-- 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 : n < q
x : ℕ
hx : x < n + 1
pos : x < q ↔ x < q + 1
⊢ Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} (⟨x, hx⟩ : Fin (n + 1)) ↔
    Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q + 1} (⟨x, hx⟩ : Fin (n + 1))

Tactic:
simp_rw [Finset.mem_filter_univ]

Premises used: Finset.mem_filter_univ
-- 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 : n < q
x : ℕ
hx : x < n + 1
⊢ x < q ↔ x < q + 1

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
neg :
  ∀ (a : ℕ) (ha : q + a = n),
    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 + 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:
obtain ⟨a, ha⟩ := Nat.le.dest hqn

Premises used: Nat.le.dest
-- 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
neg :
  HSub.hSub (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
      (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (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 + 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:
rw [Q_succ, HomologicalComplex.sub_f_apply, HomologicalComplex.comp_f, hq]

Premises used: HomologicalComplex.sub_f_apply, HomologicalComplex.comp_f, AlgebraicTopology.DoldKan.Q_succ
-- 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
neg :
  ∑ i : Fin (n + 1) with (↑i : ℕ) < q + 1, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev =
    HSub.hSub (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
      (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1))
⊢ HSub.hSub (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
      (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (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:
symm
-- 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
rw :
  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)
| HSub.hSub (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
    (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1))

Tactic:
rw [sub_eq_add_neg, add_comm]

Premises used: sub_eq_add_neg, add_comm
-- 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
neg :
  ∑ i : Fin (n + 1) with (↑i : ℕ) < q + 1, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.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)
⊢ ∑ i : Fin (n + 1) with (↑i : ℕ) < q + 1, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev =
    HSub.hSub (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ i : Fin (n + 1) with (↑i : ℕ) < q, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev)
      (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1))

Tactic:
conv_rhs => rw [sub_eq_add_neg, add_comm]

Premises used: sub_eq_add_neg, add_comm
-- 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, ⋯⟩
⊢ Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q + 1} q'

Tactic:
simp [q']
-- 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 :
  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)
⊢ ∑ i : Fin (n + 1) with (↑i : ℕ) < q + 1, HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.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)

Tactic:
rw [← @Finset.add_sum_erase _ _ _ _ _ _ q' (by simp [q'])]

Premises used: Finset.add_sum_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, ⋯⟩
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)
neg₁ : Finset.erase {i : Fin (n + 1) | (↑i : ℕ) < q + 1} q' = {i : Fin (n + 1) | (↑i : ℕ) < q}
⊢ 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)

Tactic:
congr