awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} SSet C
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F ⟶ Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := CategoryTheory.Functor.{w, v, w + 1, u} SSet C) (Functor.obj (evaluation SSet C) Δ[n])
          (Functor.obj
            (Functor.obj (C := C ⥤ SSet ⥤ HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (Functor.obj Functor.postcompose₂ (HomologicalComplex.eval C (ComplexShape.down ℕ) n))
              (chainComplexFunctor C))
            (Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F)))
        (NatTrans.app
          {
            app := fun (R : C) ↦
              Sigma.ι.{w, v, u} (β := Δ[n] _⦋n⦌) (C := C) (fun (x : Δ[n] _⦋n⦌) ↦ R)
                ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) :
                  Δ[n] _⦋n⦌),
            naturality := ⋯ }
          (Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F))
        (CategoryTheory.Functor.map (Functor.obj (evaluation SSet C) Δ[n])
          (NatTrans.app
            {
              app := fun (F : CategoryTheory.Functor.{w, v, w + 1, u} SSet C) ↦
                {
                  app := fun (S : SSet.{w}) ↦
                    Sigma.desc fun (α : S _⦋n⦌) ↦ F.map ((Equiv.symm yonedaEquiv : (a : S _⦋n⦌) → Δ[n] ⟶ S) α),
                  naturality := ⋯ },
              naturality := ⋯ }
            F)) :
      Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F ⟶ Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F)
    (𝟙 (Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F) :
      Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F ⟶ Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F)
have dsimp : Eq.{v + 1} (α := F.obj Δ[n] ⟶ F.obj Δ[n])
  (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : Δ[n] _⦋n⦌) ↦ F.obj Δ[n])
      (Sigma.ι.{w, v, u} (β := Δ[n] _⦋n⦌) (C := C) (fun (x : Δ[n] _⦋n⦌) ↦ F.obj Δ[n])
        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌))
      (Sigma.desc fun (α : Δ[n] _⦋n⦌) ↦ F.map ((Equiv.symm yonedaEquiv : (a : Δ[n] _⦋n⦌) → Δ[n] ⟶ Δ[n]) α)) :
    F.obj Δ[n] ⟶ F.obj Δ[n])
  (𝟙 (F.obj Δ[n]) : F.obj Δ[n] ⟶ F.obj Δ[n])
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic (goal)
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 ⟶ 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))
have 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)
Tactic: dsimp [chainComplexMap, chainComplexFunctor, ιChainComplex, Sigma.map',
    chainComplex, chainComplexFunctor]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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 : ℕ
⊢ 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
have 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
Tactic: by_cases! hn : n ≠ 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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
⊢ 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
have 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
Tactic: by_cases! hn : n ≠ 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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
⊢ 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
have 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)
Tactic: rw [HomologicalComplex.shape _ _ _ (by simp; lia), zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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)
⊢ 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
have pos₁ : Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) 0 0
Tactic: rw [HomologicalComplex.shape _ _ _ (by simp; lia), zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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
⊢ 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
have 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
Tactic: subst hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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) 1 ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (HomologicalComplex.d (X.chainComplex R) 1 0 ≫ fromChainComplexXZero X R) 0
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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
⊢ 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) ⋯)
have 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
Tactic: refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1
    (Preadditive.isColimitCokernelCoforkOfCofork
      ((isColimitMapCoconeCoforkEquiv _ _).1
        (isColimitOfPreserves (sigmaConst.obj R) X.isColimitCoforkπ₀)))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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
⊢ 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) ⋯)
have 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))
            sorry sorry).inv).obj
    (Preadditive.cokernelCoforkOfCofork
      (Cofork.ofπ (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (↾π₀.mk)) sorry)) ≅
  CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) sorry
Tactic: refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1
    (Preadditive.isColimitCokernelCoforkOfCofork
      ((isColimitMapCoconeCoforkEquiv _ _).1
        (isColimitOfPreserves (sigmaConst.obj R) X.isColimitCoforkπ₀)))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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 ≅
    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
have 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
Tactic: refine parallelPair.ext (-Iso.refl _) (Iso.refl _) ?_ (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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
inst_4 : X.IsConnected
⊢ IsIso.{v, u} (X := SSet.homology.{w, v, u} X R 0) (X.homology₀ε R)
have dsimp : IsIso.{v, u} (X := SSet.homology.{w, v, u} X R 0) (Y := R)
  (Iso.hom (X.homology₀Iso R) ≫ Sigma.desc fun (x : X.π₀) ↦ 𝟙 R)
Tactic: dsimp [homology₀ε]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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
inst_4 : X.IsConnected
⊢ IsIso.{v, u} (X := SSet.homology.{w, v, u} X R 0) (Y := R)
    (Iso.hom (X.homology₀Iso R) ≫ Sigma.desc fun (x : X.π₀) ↦ 𝟙 R)
have simp : IsIso.{v, u} (C := C) (X := sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) (Y := R) (Sigma.desc fun (x : X.π₀) ↦ 𝟙 R)
Tactic: simp only [isIso_comp_left_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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
inst_4 : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
⊢ IsIso.{v, u} (C := C) (X := sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) (Y := R) (Sigma.desc fun (x : X.π₀) ↦ 𝟙 R)
have refine : Eq.{v + 1} (α :=
  Quiver.Hom.{v, u} (V := C) (sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) (sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R))
  ((Sigma.desc fun (x : X.π₀) ↦ 𝟙 R) ≫ Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) x)
  (𝟙 (sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R))
Tactic: refine ⟨Sigma.ι (fun _ ↦ R) x, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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
inst_4 : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) (sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) (sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R))
    ((Sigma.desc fun (x : X.π₀) ↦ 𝟙 R) ≫ Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) x)
    (𝟙 (sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R))
have h : ∀ (y : X.π₀),
  Eq.{v + 1} (α := R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) y)
        ((Sigma.desc fun (x : X.π₀) ↦ 𝟙 R) ≫ Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) x) :
      R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) y ≫ 𝟙 (sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) :
      R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
Tactic: ext y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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
inst_4 : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
y : X.π₀
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) y)
        ((Sigma.desc fun (x : X.π₀) ↦ 𝟙 R) ≫ Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) x) :
      R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) y ≫ 𝟙 (sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) :
      R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
have h : Eq.{v + 1} (α := R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
  (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) (Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) x)
      ((Sigma.desc fun (x : X.π₀) ↦ 𝟙 R) ≫ Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) x) :
    R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
  (Sigma.ι.{w, v, u} (C := C) (fun (x : X.π₀) ↦ R) x ≫ 𝟙 (sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) :
    R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
Tactic: obtain rfl : x = y := by subsingleton
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
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⦌
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n)
    (X.ιNormalizedChainComplex x ≫ Hom.f (X.fromNormalizedChainComplex R) n) (X.ιChainComplex x ≫ Hom.f PInfty n)
have dsimp : Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n)
  ((X.ιChainComplex x ≫ Hom.f (X.toNormalizedChainComplex R) n) ≫ Hom.f (X.fromNormalizedChainComplex R) n)
  (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n) (X.ιChainComplex x) (Hom.f PInfty n))
Tactic: dsimp [ιNormalizedChainComplex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
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⦌
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n)
    ((X.ιChainComplex x ≫ Hom.f (X.toNormalizedChainComplex R) n) ≫ Hom.f (X.fromNormalizedChainComplex R) n)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n) (X.ιChainComplex x)
      (Hom.f PInfty n))
have rw : Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n) (X.ιChainComplex x ≫ Hom.f PInfty n)
  (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n) (X.ιChainComplex x) (Hom.f PInfty n))
Tactic: rw [Category.assoc, toNormalizedChainComplex_f_fromNormalizedChainComplex_f]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
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⦌
hx : x ∈ X.degenerate n
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n) (X.ιNormalizedChainComplex x) 0
have rw : Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n) (X.ιChainComplex x ≫ Hom.f PInfty n) 0
Tactic: rw [← cancel_mono ((X.fromNormalizedChainComplex R).f n), zero_comp,
    ιNormalizedChainComplex_fromNormalizedChainComplex_f]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
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⦌
hx : x ∈ X.degenerate n
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n) (X.ιChainComplex x ≫ Hom.f PInfty n) 0
have zero : ∀ (x : X _⦋0⦌) (hx : Membership.mem (γ := Set (X _⦋0⦌)) (X.degenerate 0) x),
  Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0) (X.ιChainComplex x ≫ Hom.f PInfty 0) 0
Tactic: obtain _ | n := n
Cleared hypotheses: n, x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
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⦌
hx : x ∈ X.degenerate n
zero :
  ∀ (x : X _⦋0⦌) (hx : Membership.mem (γ := Set (X _⦋0⦌)) (X.degenerate 0) x),
    Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0) (X.ιChainComplex x ≫ Hom.f PInfty 0) 0
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n) (X.ιChainComplex x ≫ Hom.f PInfty n) 0
have succ : ∀ (n : ℕ) (x : X _⦋n + 1⦌) (hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x),
  Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) (n + 1))
    (X.ιChainComplex x ≫ Hom.f PInfty (n + 1)) 0
Tactic: obtain _ | n := n
Cleared hypotheses: n, x, hx