awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⦌
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) 0)
    (X.ιChainComplex x ≫ HomologicalComplex.d (X.chainComplex R) 0 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⦌
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R)
    (CategoryStruct.comp (Y := HomologicalComplex.cycles.{v, u, 0} (X.chainComplex R) 0)
        (HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0
            liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯ :
          R ⟶ HomologicalComplex.cycles.{v, u, 0} (X.chainComplex R) 0)
        (HomologicalComplex.homologyπ (X.chainComplex R) 0 ≫ Iso.hom (X.homology₀Iso R) :
          HomologicalComplex.cycles.{v, u, 0} (X.chainComplex R) 0 ⟶ sigmaObj.{w, v, u} fun (x : 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 [homology₀Iso, HomologicalComplex.homologyπ, SSet.homology,
    HomologicalComplex.liftCycles]

Premises used: HomologicalComplex.homologyπ, SSet.homology, SSet.homology₀Iso, HomologicalComplex.liftCycles
-- 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⦌
⊢ Eq.{v + 1} (α := R ⟶ R)
    (CategoryStruct.comp (Y := HomologicalComplex.cycles.{v, u, 0} (X.chainComplex R) 0)
      (HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0
          liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯ :
        R ⟶ HomologicalComplex.cycles.{v, u, 0} (X.chainComplex R) 0)
      (HomologicalComplex.homologyπ (X.chainComplex R) 0 ≫ X.homology₀ε R :
        HomologicalComplex.cycles.{v, u, 0} (X.chainComplex R) 0 ⟶ R))
    (𝟙 R)

Tactic:
simp [homology₀ε]

Premises used: SSet.homology₀ε
-- 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
inst_4 : X.IsConnected
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)
⊢ IsIso.{v, u} (X := SSet.homology.{w, v, u} X R 0) (X.homology₀ε R)

Tactic:
dsimp [homology₀ε]

Premises used: SSet.homology₀ε
-- 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
inst_4 : X.IsConnected
simp : IsIso.{v, u} (C := C) (X := sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) (Y := R) (Sigma.desc fun (x : X.π₀) ↦ 𝟙 R)
⊢ 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:
simp only [isIso_comp_left_iff]

Premises used: CategoryTheory.isIso_comp_left_iff
-- 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
inst_4 : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
⊢ Eq.{v + 1} (α := R ⟶ 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) :
      R ⟶ R)
    (𝟙 R : R ⟶ R)

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
inst_4 : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
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))
⊢ IsIso.{v, u} (C := C) (X := sigmaObj.{w, v, u} fun (x : X.π₀) ↦ R) (Y := R) (Sigma.desc fun (x : X.π₀) ↦ 𝟙 R)

Tactic:
refine ⟨Sigma.ι (fun _ ↦ R) x, ?_, by 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
inst_4 : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
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)
⊢ 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:
ext y
-- 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
inst_4 : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
y : X.π₀
⊢ x = y

Tactic:
subsingleton
-- 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
inst_4 : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
y : X.π₀
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)
⊢ 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:
obtain rfl : x = y := by subsingleton

Premises used: 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 : C
inst_3 : CategoryWithHomology.{v, u} C
inst_4 : X.IsConnected
x : X.π₀ := Classical.arbitrary 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) 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:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasCoproducts.{w, v, u} C
X Y : SSet
f g : X ⟶ Y
inst_3 : CategoryWithHomology.{v, u} C
H : Homotopy f g
R : C
n : ℕ
⊢ Eq.{v + 1} (α := SSet.homology.{w, v, u} X R n ⟶ SSet.homology.{w, v, u} Y R n) (SSet.homologyMap f R n)
    (SSet.homologyMap g R n)

Tactic:
(H.sSetChainComplexMap R).homologyMap_eq n

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

Tactic:
(H.chainComplexMap R).homologyMap_eq n

Premises used: SSet.Homotopy.chainComplexMap, Homotopy.homologyMap_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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} (α :=
    Quiver.Hom (V := ChainComplex.{v, u, 0} C ℕ)
      (AlgebraicTopology.AlternatingFaceMapComplex.obj
        (Functor.obj (Functor.obj (sigmaConst ⋙ SimplicialObject.whiskering (Type w) C) R) X))
      (X.normalizedChainComplex R))
    (PInfty ≫ X.toNormalizedChainComplex R) (X.toNormalizedChainComplex R)

Tactic:
SimplicialObject.Splitting.PInfty_toNondegComplex _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.SimplicialObject.Splitting.PInfty_toNondegComplex, SSet.normalizedChainComplex, SSet.toNormalizedChainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
⊢ IsSplitEpi (C := ChainComplex.{v, u, 0} C ℕ) (X := X.chainComplex R) (X.toNormalizedChainComplex R)

Tactic:
SimplicialObject.Splitting.isSplitEpi_toNondegComplex _

Premises used: CategoryTheory.Functor.comp, SSet.normalizedChainComplex, AlgebraicTopology.AlternatingFaceMapComplex.obj, CategoryTheory.SimplicialObject.Splitting.isSplitEpi_toNondegComplex, SSet.toNormalizedChainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
⊢ IsSplitMono (C := ChainComplex.{v, u, 0} C ℕ) (X := X.normalizedChainComplex R) (X.fromNormalizedChainComplex R)

Tactic:
SimplicialObject.Splitting.isSplitMono_fromNondegComplex _

Premises used: CategoryTheory.SimplicialObject.Splitting.isSplitMono_fromNondegComplex, CategoryTheory.Functor.comp, SSet.normalizedChainComplex, SSet.fromNormalizedChainComplex, AlgebraicTopology.AlternatingFaceMapComplex.obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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} (α :=
    Quiver.Hom (V := ChainComplex.{v, u, 0} C ℕ) (X.normalizedChainComplex R) (X.normalizedChainComplex R))
    (X.fromNormalizedChainComplex R ≫ X.toNormalizedChainComplex R) (𝟙 (X.normalizedChainComplex R))

Tactic:
SimplicialObject.Splitting.fromNondegComplex_toNondegComplex _

Premises used: CategoryTheory.Functor.comp, SSet.normalizedChainComplex, SSet.fromNormalizedChainComplex, AlgebraicTopology.AlternatingFaceMapComplex.obj, SSet.toNormalizedChainComplex, CategoryTheory.SimplicialObject.Splitting.fromNondegComplex_toNondegComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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 : ℕ
⊢ Hom.f (X.fromNormalizedChainComplex R) n ≫ Hom.f (X.toNormalizedChainComplex R) n =
    𝟙 (HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n)

Tactic:
simp [← HomologicalComplex.comp_f]

Premises used: HomologicalComplex.comp_f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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} (α := Quiver.Hom (V := ChainComplex.{v, u, 0} C ℕ) (X.chainComplex R) (X.chainComplex R))
    (X.toNormalizedChainComplex R ≫ X.fromNormalizedChainComplex R) PInfty

Tactic:
SimplicialObject.Splitting.toNondegComplex_fromNondegComplex _

Premises used: CategoryTheory.Functor.comp, SSet.normalizedChainComplex, SSet.fromNormalizedChainComplex, AlgebraicTopology.AlternatingFaceMapComplex.obj, CategoryTheory.SimplicialObject.Splitting.toNondegComplex_fromNondegComplex, SSet.toNormalizedChainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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 ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n)
    (Hom.f (X.toNormalizedChainComplex R) n ≫ Hom.f (X.fromNormalizedChainComplex R) n) (Hom.f PInfty n)

Tactic:
simp [← HomologicalComplex.comp_f]

Premises used: HomologicalComplex.comp_f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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} (α :=
    Quiver.Hom (V := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ)) (X.chainComplex R)
      (X.normalizedChainComplex R))
    (HomotopyEquiv.hom (X.homotopyEquivNormalizedChainComplex R)) (X.toNormalizedChainComplex R)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, SSet.toNormalizedChainComplex, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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} (α :=
    Quiver.Hom (V := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ)) (X.normalizedChainComplex R)
      (X.chainComplex R))
    (HomotopyEquiv.inv (X.homotopyEquivNormalizedChainComplex R)) (X.fromNormalizedChainComplex R)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, SSet.fromNormalizedChainComplex, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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.normalizedChainComplex R) n)
    (X.ιChainComplex x ≫ Hom.f (X.toNormalizedChainComplex R) n) (X.ιNormalizedChainComplex x)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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.normalizedChainComplex R) n)
    (X.ιNormalizedChainComplex x ≫ d (X.normalizedChainComplex R) (n + 1) n)
    (∑ i : Fin (n + 2),
      HSMul.hSMul (β := R ⟶ HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n)
        (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
        (X.ιNormalizedChainComplex
          ((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 [ιNormalizedChainComplex, Preadditive.sum_comp,
    -ιChainComplex_toNormalizedChainComplex_f]

Premises used: CategoryTheory.Preadditive.sum_comp, SSet.ιChainComplex_toNormalizedChainComplex_f, SSet.ιNormalizedChainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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⦌
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))
⊢ 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)

Tactic:
dsimp [ιNormalizedChainComplex]

Premises used: SSet.ιNormalizedChainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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⦌
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))
⊢ 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:
rw [Category.assoc, toNormalizedChainComplex_f_fromNormalizedChainComplex_f]

Premises used: CategoryTheory.Category.assoc, SSet.toNormalizedChainComplex_f_fromNormalizedChainComplex_f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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 PInfty n)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n) (X.ιChainComplex x)
      (Hom.f PInfty n))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
rw : Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n) (X.ιChainComplex x ≫ Hom.f PInfty n) 0
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n) (X.ιNormalizedChainComplex x) 0

Tactic:
rw [← cancel_mono ((X.fromNormalizedChainComplex R).f n), zero_comp,
    ιNormalizedChainComplex_fromNormalizedChainComplex_f]

Premises used: HomologicalComplex.Hom.f, SSet.ιNormalizedChainComplex_fromNormalizedChainComplex_f, SSet.fromNormalizedChainComplex, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
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
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n) (X.ιChainComplex x ≫ Hom.f PInfty n) 0

Tactic:
obtain _ | n := n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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⦌
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:
simp at hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x
⊢ ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x

Tactic:
simp only [degenerate_eq_iUnion_range_σ, Set.mem_iUnion, Set.mem_range] at hx

Premises used: Set.mem_range, Set.mem_iUnion, SSet.degenerate_eq_iUnion_range_σ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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⦌
hx :
  ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x
X' : SimplicialObject.{v, u} C :=
  Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst R)) X
succ :
  ∀ (i : Fin (n + 1)) (y : X _⦋n⦌),
    Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) (n + 1))
      (X.ιChainComplex
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y) ≫
        Hom.f PInfty (n + 1))
      0
⊢ 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 ⟨i, y, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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' : SimplicialObject.{v, u} C :=
  Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst R)) X
i : Fin (n + 1)
y : X _⦋n⦌
trans :
  Eq (α :=
    R ⟶
      HomologicalComplex.X.{v, u, 0}
        (AlgebraicTopology.AlternatingFaceMapComplex.obj
          (Functor.obj (Functor.obj (sigmaConst ⋙ SimplicialObject.whiskering (Type w) C) R) X))
        (n + 1))
    (X.ιChainComplex
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y) ≫
      Hom.f PInfty (n + 1))
    (X.ιChainComplex y ≫ X'.σ i ≫ Hom.f PInfty (n + 1))
trans₁ :
  Eq (α :=
    R ⟶
      HomologicalComplex.X.{v, u, 0}
        (AlgebraicTopology.AlternatingFaceMapComplex.obj
          (Functor.obj (Functor.obj (sigmaConst ⋙ SimplicialObject.whiskering (Type w) C) R) X))
        (n + 1))
    (X.ιChainComplex y ≫ X'.σ i ≫ Hom.f PInfty (n + 1)) 0
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) (n + 1))
    (X.ιChainComplex
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y) ≫
      Hom.f PInfty (n + 1))
    0

Tactic:
trans X.ιChainComplex y ≫ X'.σ i ≫ (PInfty (X := X')).f _

Premises used: SSet.ιChainComplex, HomologicalComplex.Hom.f, AlgebraicTopology.DoldKan.PInfty, CategoryTheory.SimplicialObject.σ