awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n)
    (X.ιChainComplex x ≫ HomologicalComplex.d (X.chainComplex R) (n + 1) n)
    (∑ i : Fin (n + 2),
      HSMul.hSMul (β := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
        (X.ιChainComplex
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
              (a : (fun (X : Type w) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type w) ↦ X) (X _⦋n⦌))
            x)))

Tactic:
simp [ιChainComplex, chainComplex, chainComplexFunctor, Preadditive.comp_sum]

Premises used: SSet.ιChainComplex, SSet.chainComplexFunctor, CategoryTheory.Preadditive.comp_sum, SSet.chainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x : X _⦋n⦌
dsimp :
  Eq.{v + 1} (α := R ⟶ sigmaObj.{w, v, u} fun (x : Y _⦋n⦌) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : X _⦋n⦌) ↦ R)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : X _⦋n⦌) ↦ R) x)
        (Sigma.desc fun (a : X _⦋n⦌) ↦
          𝟙 R ≫
            Sigma.ι.{w, v, u} (β := Y _⦋n⦌) (C := C) (fun (x : Y _⦋n⦌) ↦ R)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) : (a : X _⦋n⦌) → Y _⦋n⦌) a :
                Y _⦋n⦌)) :
      R ⟶ sigmaObj.{w, v, u} fun (x : Y _⦋n⦌) ↦ R)
    (Sigma.ι.{w, v, u} (β := Y _⦋n⦌) (C := C) (fun (x : Y _⦋n⦌) ↦ R)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) : (a : X _⦋n⦌) → Y _⦋n⦌) x : Y _⦋n⦌) :
      R ⟶ sigmaObj.{w, v, u} fun (x : Y _⦋n⦌) ↦ R)
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (Y.chainComplex R) n)
    (X.ιChainComplex x ≫ HomologicalComplex.Hom.f (chainComplexMap f R) n)
    (Y.ιChainComplex
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type w) ↦ X) (X _⦋n⦌)) → (fun (X : Type w) ↦ X) (Y _⦋n⦌))
        x))

Tactic:
dsimp [chainComplexMap, chainComplexFunctor, ιChainComplex, Sigma.map',
    chainComplex, chainComplexFunctor]

Premises used: SSet.ιChainComplex, SSet.chainComplexFunctor, SSet.chainComplexMap, CategoryTheory.Limits.Sigma.map', SSet.chainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x : X _⦋n⦌
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{w, v, u} fun (x : Y _⦋n⦌) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : X _⦋n⦌) ↦ R)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : X _⦋n⦌) ↦ R) x)
        (Sigma.desc fun (a : X _⦋n⦌) ↦
          𝟙 R ≫
            Sigma.ι.{w, v, u} (β := Y _⦋n⦌) (C := C) (fun (x : Y _⦋n⦌) ↦ R)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) : (a : X _⦋n⦌) → Y _⦋n⦌) a :
                Y _⦋n⦌)) :
      R ⟶ sigmaObj.{w, v, u} fun (x : Y _⦋n⦌) ↦ R)
    (Sigma.ι.{w, v, u} (β := Y _⦋n⦌) (C := C) (fun (x : Y _⦋n⦌) ↦ R)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) : (a : X _⦋n⦌) → Y _⦋n⦌) x : Y _⦋n⦌) :
      R ⟶ sigmaObj.{w, v, u} fun (x : Y _⦋n⦌) ↦ R)

Tactic:
simp [Sigma.ι_desc]

Premises used: CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
T : C
f g : HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n ⟶ T
h : ∀ (x : X _⦋n⦌), X.ιChainComplex x ≫ f = X.ιChainComplex x ≫ g
⊢ f = g

Tactic:
(X.isColimitChainComplexXCofan R n).hom_ext (fun _ ↦ h _)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.as, SSet.isColimitChainComplexXCofan
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
inst_3 : CategoryWithHomology.{v, u} C
n : ℕ
⊢ SSet.homologyMap (𝟙 X) R n = 𝟙 (SSet.homology.{w, v, u} X R n)

Tactic:
simp [SSet.homologyMap]

Premises used: SSet.homologyMap
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X Y Z : SSet
f : X ⟶ Y
g : Y ⟶ Z
R : C
inst_3 : CategoryWithHomology.{v, u} C
n : ℕ
⊢ Eq.{v + 1} (α := SSet.homology.{w, v, u} X R n ⟶ SSet.homology.{w, v, u} Z R n) (SSet.homologyMap (f ≫ g) R n)
    (SSet.homologyMap f R n ≫ SSet.homologyMap g R n)

Tactic:
simp [SSet.homologyMap, HomologicalComplex.homologyMap_comp]

Premises used: HomologicalComplex.homologyMap_comp, SSet.homologyMap
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
x : X _⦋0⦌
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0) (X.ιChainComplex x)
        (fromChainComplexXZero X R) :
      R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) (mk x) : R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)

Tactic:
simp [π₀.fromChainComplexXZero, ιChainComplex]

Premises used: SSet.ιChainComplex, SSet.π₀.fromChainComplexXZero
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
pos :
  ∀ (hn : n ≠ 1),
    Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
      (HomologicalComplex.d (X.chainComplex R) n 0 ≫ fromChainComplexXZero X R) 0
neg :
  ∀ (hn : n = 1),
    Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
      (HomologicalComplex.d (X.chainComplex R) n 0 ≫ fromChainComplexXZero X R) 0
⊢ Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (HomologicalComplex.d (X.chainComplex R) n 0 ≫ fromChainComplexXZero X R) 0

Tactic:
by_cases! hn : n ≠ 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
⊢ ¬1 = n

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
pos :
  Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0) 0 (fromChainComplexXZero X R) :
      HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (0 : HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
pos₁ pos₂ :
  Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) 0 0
⊢ Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (HomologicalComplex.d (X.chainComplex R) n 0 ≫ fromChainComplexXZero X R) 0

Tactic:
rw [HomologicalComplex.shape _ _ _ (by simp; lia), zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
hn : n = 1
neg :
  Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1 ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (HomologicalComplex.d (X.chainComplex R) 1 0 ≫ fromChainComplexXZero X R) 0
⊢ Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (HomologicalComplex.d (X.chainComplex R) n 0 ≫ fromChainComplexXZero X R) 0

Tactic:
subst hn
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
neg :
  ∀ (x : X _⦋1⦌),
    Eq.{v + 1} (α := R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
      (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1) (X.ιChainComplex x)
          (HomologicalComplex.d (X.chainComplex R) 1 0 ≫ fromChainComplexXZero X R) :
        R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
      (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1) (X.ιChainComplex x) 0 :
        R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
⊢ Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1 ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (HomologicalComplex.d (X.chainComplex R) 1 0 ≫ fromChainComplexXZero X R) 0

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
x : X _⦋1⦌
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1) (X.ιChainComplex x)
        (HomologicalComplex.d (X.chainComplex R) 1 0 ≫ fromChainComplexXZero X R) :
      R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1) (X.ιChainComplex x) 0 :
      R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)

Tactic:
simp [π₀.sound (Edge.mk' x)]

Premises used: SSet.π₀.sound, SSet.Edge.mk'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
refine_1 :
  parallelPair
      (HSub.hSub (α :=
        Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
          Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
        (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
        (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
      0 ≅
    parallelPair (X := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1) (Y :=
      HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0) (HomologicalComplex.d (X.chainComplex R) 1 0) 0
refine_2 :
  (Cocone.precompose
          (parallelPair.ext
              (-Iso.refl
                  ((parallelPair
                        (HSub.hSub (α :=
                          Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                            Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                          (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                          (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                        0).obj
                    WalkingParallelPair.zero))
              (Iso.refl
                ((parallelPair
                      (HSub.hSub (α :=
                        Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                          Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                        (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                        (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                      0).obj
                  WalkingParallelPair.one))
              ⋯ ⋯).inv).obj
      (Preadditive.cokernelCoforkOfCofork
        (Cofork.ofπ (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (↾π₀.mk)) ⋯)) ≅
    CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯
⊢ IsColimit.{0, v, 0, u} (F :=
    parallelPair (X := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1) (Y :=
      HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0) (HomologicalComplex.d (X.chainComplex R) 1 0) 0)
    (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯)

Tactic:
refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1
    (Preadditive.isColimitCokernelCoforkOfCofork
      ((isColimitMapCoconeCoforkEquiv _ _).1
        (isColimitOfPreserves (sigmaConst.obj R) X.isColimitCoforkπ₀)))

Premises used: CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, Equiv.toFun, CategoryTheory.Limits.sigmaConst, SSet.isColimitCoforkπ₀, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.Preadditive.isColimitCokernelCoforkOfCofork, CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
⊢ (parallelPair
            (HSub.hSub (α :=
              Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
              (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
              (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
            0).map
        WalkingParallelPairHom.right ≫
      Iso.hom
        (Iso.refl
          ((parallelPair
                (HSub.hSub (α :=
                  Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                    Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                  (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                  (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                0).obj
            WalkingParallelPair.one)) =
    Iso.hom
        (-Iso.refl
            ((parallelPair
                  (HSub.hSub (α :=
                    Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                      Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                    (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                    (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                  0).obj
              WalkingParallelPair.zero)) ≫
      CategoryTheory.Functor.map
        (parallelPair (X := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1) (Y :=
          HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0) (HomologicalComplex.d (X.chainComplex R) 1 0) 0)
        WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
refine_1 :
  (parallelPair
            (HSub.hSub (α :=
              Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
              (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
              (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
            0).map
        WalkingParallelPairHom.left ≫
      Iso.hom
        (Iso.refl
          ((parallelPair
                (HSub.hSub (α :=
                  Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                    Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                  (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                  (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                0).obj
            WalkingParallelPair.one)) =
    Iso.hom
        (-Iso.refl
            ((parallelPair
                  (HSub.hSub (α :=
                    Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                      Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                    (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                    (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                  0).obj
              WalkingParallelPair.zero)) ≫
      CategoryTheory.Functor.map
        (parallelPair (X := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1) (Y :=
          HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0) (HomologicalComplex.d (X.chainComplex R) 1 0) 0)
        WalkingParallelPairHom.left
⊢ parallelPair
      (HSub.hSub (α :=
        Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
          Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
        (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
        (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
      0 ≅
    parallelPair (X := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1) (Y :=
      HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0) (HomologicalComplex.d (X.chainComplex R) 1 0) 0

Tactic:
refine parallelPair.ext (-Iso.refl _) (Iso.refl _) ?_ (by simp)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.parallelPair.ext, Neg.neg
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
⊢ (parallelPair
            (HSub.hSub (α :=
              Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
              (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
              (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
            0).map
        WalkingParallelPairHom.left ≫
      Iso.hom
        (Iso.refl
          ((parallelPair
                (HSub.hSub (α :=
                  Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                    Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                  (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                  (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                0).obj
            WalkingParallelPair.one)) =
    Iso.hom
        (-Iso.refl
            ((parallelPair
                  (HSub.hSub (α :=
                    Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                      Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                    (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                    (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                  0).obj
              WalkingParallelPair.zero)) ≫
      CategoryTheory.Functor.map
        (parallelPair (X := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 1) (Y :=
          HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0) (HomologicalComplex.d (X.chainComplex R) 1 0) 0)
        WalkingParallelPairHom.left

Tactic:
simp [chainComplex, SSet.chainComplexFunctor, sub_eq_neg_add]

Premises used: sub_eq_neg_add, SSet.chainComplexFunctor, SSet.chainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq.{v + 1} (α :=
    ShortComplex.X₂.{v, u} (HomologicalComplex.sc' (X.chainComplex R) 1 0 0) ⟶
      ShortComplex.X₃.{v, u} (HomologicalComplex.sc' (X.chainComplex R) 1 0 0))
    (ShortComplex.g (HomologicalComplex.sc' (X.chainComplex R) 1 0 0)) 0
⊢ Eq.{v + 1} (α :=
    ShortComplex.X₂.{v, u} (HomologicalComplex.sc' (X.chainComplex R) 1 0 0) ⟶
      ShortComplex.X₃.{v, u} (HomologicalComplex.sc' (X.chainComplex R) 1 0 0))
    (ShortComplex.g (HomologicalComplex.sc' (X.chainComplex R) 1 0 0)) 0

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
⊢ Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0 ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (ShortComplex.LeftHomologyData.π (ShortComplex.HomologyData.left (X.homologyData₀ R)) :
      ShortComplex.LeftHomologyData.K.{v, u} (S := HomologicalComplex.sc' (X.chainComplex R) 1 0 0)
          (ShortComplex.HomologyData.left (X.homologyData₀ R)) ⟶
        ShortComplex.LeftHomologyData.H.{v, u} (S := HomologicalComplex.sc' (X.chainComplex R) 1 0 0)
          (ShortComplex.HomologyData.left (X.homologyData₀ R)))
    (π₀.fromChainComplexXZero X R)

Tactic:
rfl

Premises used: SSet.π₀.fromChainComplexXZero, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.Sigma.map', rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
⊢ Eq.{v + 1} (α :=
    HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0 ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0)
    (ShortComplex.LeftHomologyData.i (ShortComplex.HomologyData.left (X.homologyData₀ R)) :
      ShortComplex.LeftHomologyData.K.{v, u} (S := HomologicalComplex.sc' (X.chainComplex R) 1 0 0)
          (ShortComplex.HomologyData.left (X.homologyData₀ R)) ⟶
        ShortComplex.X₂.{v, u} (HomologicalComplex.sc' (X.chainComplex R) 1 0 0))
    (𝟙 (HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0))

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R T : C
f : T ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0
⊢ ShortComplex.LeftHomologyData.liftK (ShortComplex.HomologyData.left (X.homologyData₀ R)) f ⋯ = f

Tactic:
ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_liftK ..

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork, CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_liftK
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
inst_3 : CategoryWithHomology.{v, u} C
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
inst_3 : CategoryWithHomology.{v, u} C
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
inst_3 : CategoryWithHomology.{v, u} C
x : X _⦋0⦌
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
simp