awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ hF.inv.app (G.obj Y) ≫
      (eA.functor ⋙ e'.functor).map (eA.unitIso.hom.app (G.obj Y)) ≫
        (eA.functor ⋙ e'.functor).map (eA.inverse.map (hG.inv.app Y)) ≫
          e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y)) ≫ hG.hom.app Y) ≫
            hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y
have w : hF.inv.app (G.obj Y) ≫
    e'.functor.map (eA.functor.map (eA.unitIso.hom.app (G.obj Y))) ≫
      e'.functor.map (eA.counit.app (eA.functor.obj (G.obj Y))) ≫
        e'.functor.map (hG.inv.app Y) ≫
          e'.functor.map (eA.counitInv.app (e'.inverse.obj (eB.functor.obj Y))) ≫
            e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
              e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y =
  η.hom.app Y
Tactic: simp only [Functor.comp_map, Equivalence.fun_inv_map, comp_obj, id_obj, map_comp, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ hF.inv.app (G.obj Y) ≫
      e'.functor.map (eA.functor.map (eA.unitIso.hom.app (G.obj Y))) ≫
        e'.functor.map (eA.counit.app (eA.functor.obj (G.obj Y))) ≫
          e'.functor.map (hG.inv.app Y) ≫
            e'.functor.map (eA.counitInv.app (e'.inverse.obj (eB.functor.obj Y))) ≫
              e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y
have w : hF.inv.app (G.obj Y) ≫
    e'.functor.map
        (eA.functor.map (eA.unitIso.hom.app (G.obj Y)) ≫
          eA.counit.app (eA.functor.obj (G.obj Y)) ≫
            hG.inv.app Y ≫
              eA.counitInv.app (e'.inverse.obj (eB.functor.obj Y)) ≫
                eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y)) ≫ hG.hom.app Y) ≫
      hF.hom.app (G.obj Y) ≫ η.hom.app Y =
  η.hom.app Y
Tactic: simp only [← e'.functor.map_comp_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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 = ε
⊢ (equivalence hF hG).unitIso = equivalenceUnitIso hG ε
have w : (equivalence hF hG).unitIso.hom = (equivalenceUnitIso hG ε).hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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 = ε
⊢ (equivalence hF hG).unitIso.hom = (equivalenceUnitIso hG ε).hom
have w : (equivalence hF hG).unitIso.hom.app = (equivalenceUnitIso hG ε).hom.app
Tactic: apply NatTrans.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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 = ε
⊢ (equivalence hF hG).unitIso.hom.app = (equivalenceUnitIso hG ε).hom.app
have w : ∀ (X : A), (equivalence hF hG).unitIso.hom.app X = (equivalenceUnitIso hG ε).hom.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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 hF hG).unitIso.hom.app X = (equivalenceUnitIso hG ε).hom.app X
have 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
Tactic: dsimp [equivalence]
-- 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)
⊢ 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)
have 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)
Tactic: by_cases! hqn : n < 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 : ℕ
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)
⊢ 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)
have 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)
Tactic: by_cases! hqn : n < 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 : ℕ
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
⊢ 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)
have 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)
Tactic: rw [Q_is_eventually_constant (show n + 1 ≤ q by lia), hq]
-- 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 : n < q
⊢ 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)
have pos : Eq (α := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} {i : Fin (n + 1) | (↑i : ℕ) < q + 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 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
⊢ Eq (α := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} {i : Fin (n + 1) | (↑i : ℕ) < q + 1}
have 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))
Tactic: ext ⟨x, hx⟩
-- 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 : n < q
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))
have pos : x < q ↔ x < q + 1
Tactic: simp_rw [Finset.mem_filter_univ]
-- 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
⊢ 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)
have 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)
Tactic: obtain ⟨a, ha⟩ := Nat.le.dest hqn
-- 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
⊢ 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)
have 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
Tactic: rw [Q_succ, HomologicalComplex.sub_f_apply, HomologicalComplex.comp_f, hq]
-- 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
⊢ 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
have 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))
Tactic: symm
-- 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
| 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))
have 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)
Tactic: rw [sub_eq_add_neg, add_comm]
-- 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
⊢ ∑ 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))
have 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)
Tactic: conv_rhs => rw [sub_eq_add_neg, add_comm]
-- 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 : 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)
have 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)
Tactic: rw [← @Finset.add_sum_erase _ _ _ _ _ _ q' (by simp [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 : ℕ
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 +
      ∑ 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 : 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: congr