awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
zero : False
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋0⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty 0 : X.obj (Opposite.op Δ') ⟶ X _⦋0⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0)

Tactic:
exfalso
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
zero :
  Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
⊢ False

Tactic:
apply hθ
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
x y : Fin (⦋0⦌.len + 1)
h :
  Eq (α := Fin (Δ'.len + 1))
    ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
zero :
  ∀
    (h :
      Eq (α := Fin (Δ'.len + 1))
        ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
            ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) :
          Fin (Δ'.len + 1))
        ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))),
    (fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩ = y
⊢ x = y

Tactic:
fin_cases x
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
y : Fin (⦋0⦌.len + 1)
h :
  Eq (α := Fin (Δ'.len + 1))
    ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
        ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      Fin (Δ'.len + 1))
    ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
zero :
  ∀
    (h :
      Eq (α := Fin (Δ'.len + 1))
        ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
          ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
        ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
          ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))),
    Eq (α := Fin (⦋0⦌.len + 1)) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)
⊢ (fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩ = y

Tactic:
fin_cases y
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
h :
  Eq (α := Fin (Δ'.len + 1))
    ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
      ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
    ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
      ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
⊢ Eq (α := Fin (⦋0⦌.len + 1)) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
Δ' : SimplexCategory
n : ℕ
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
succ :
  ∀ (i : Fin (n + 1)) (α : ⦋n⦌ ⟶ Δ') (h : θ = SimplexCategory.σ i ≫ α),
    Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
      (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
      (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))

Tactic:
obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ

Premises used: SimplexCategory.eq_σ_comp_of_not_injective
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
Δ' : SimplexCategory
n : ℕ
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
i : Fin (n + 1)
α : ⦋n⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
succ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (SimplexCategory.σ i ≫ α).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₁ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (α.op ≫ (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₂ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    ((X.map α.op ≫ X.map (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₃ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map α.op ≫ X.map (SimplexCategory.σ i).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₄ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map α.op ≫ X.σ i ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₅ : Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌) (X.map α.op ≫ 0) 0
succ₆ succ₇ : Eq.{v_1 + 1} (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌) 0 0
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))

Tactic:
rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Limits.comp_zero, CategoryTheory.SimplicialObject.σ_def, AlgebraicTopology.DoldKan.σ_comp_PInfty, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
T : C
f : X _⦋0⦌ ⟶ T
⊢ DegeneraciesVanish f ↔ True

Tactic:
Iff.rfl

Premises used: Iff.rfl, AlgebraicTopology.DoldKan.DegeneraciesVanish
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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 : ℕ
T : C
f : X _⦋n + 1⦌ ⟶ T
⊢ DegeneraciesVanish f ↔ ∀ (i : Fin (n + 1)), X.σ i ≫ f = 0

Tactic:
Iff.rfl

Premises used: Iff.rfl, AlgebraicTopology.DoldKan.DegeneraciesVanish
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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 : ℕ
T : C
f : X _⦋n + 1⦌ ⟶ T
hf : DegeneraciesVanish f
i : Fin (n + 1)
⊢ X.σ i ≫ f = 0

Tactic:
hf i
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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 : ℕ
T : C
f : X _⦋n⦌ ⟶ T
hf : DegeneraciesVanish f
U : C
g : T ⟶ U
zero : ∀ {f : X _⦋0⦌ ⟶ T} (hf : DegeneraciesVanish f), DegeneraciesVanish (f ≫ g)
succ : ∀ (n : ℕ) {f : X _⦋n + 1⦌ ⟶ T} (hf : DegeneraciesVanish f), DegeneraciesVanish (f ≫ g)
⊢ DegeneraciesVanish (f ≫ g)

Tactic:
obtain _ | n := n
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
T U : C
g : T ⟶ U
f : X _⦋0⦌ ⟶ T
hf : DegeneraciesVanish f
⊢ DegeneraciesVanish (f ≫ g)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
T U : C
g : T ⟶ U
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : DegeneraciesVanish f
⊢ DegeneraciesVanish (f ≫ g)

Tactic:
simp [degeneraciesVanish_succ_iff, hf.σ_comp_assoc]

Premises used: AlgebraicTopology.DoldKan.DegeneraciesVanish.σ_comp_assoc, AlgebraicTopology.DoldKan.degeneraciesVanish_succ_iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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 : ℕ
zero :
  DegeneraciesVanish.{v_1, u_1} (C := C) (X := X) (n := 0) (T :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0) (HomologicalComplex.Hom.f PInfty 0)
succ :
  ∀ (n : ℕ),
    DegeneraciesVanish.{v_1, u_1} (C := C) (X := X) (n := n + 1) (T :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1)) (HomologicalComplex.Hom.f PInfty (n + 1))
⊢ DegeneraciesVanish.{v_1, u_1} (C := C) (X := X) (T := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n)
    (HomologicalComplex.Hom.f PInfty n)

Tactic:
obtain _ | n := n
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
⊢ DegeneraciesVanish.{v_1, u_1} (C := C) (X := X) (n := 0) (T :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0) (HomologicalComplex.Hom.f PInfty 0)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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 : ℕ
⊢ DegeneraciesVanish.{v_1, u_1} (C := C) (X := X) (n := n + 1) (T :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1)) (HomologicalComplex.Hom.f PInfty (n + 1))

Tactic:
simp [degeneraciesVanish_succ_iff]

Premises used: AlgebraicTopology.DoldKan.degeneraciesVanish_succ_iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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 : ℕ
T : C
f : X _⦋n⦌ ⟶ T
zero :
  ∀ (f : X _⦋0⦌ ⟶ T),
    DegeneraciesVanish f ↔
      Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0 ⟶ T) (HomologicalComplex.Hom.f QInfty 0 ≫ f) 0
succ :
  ∀ (n : ℕ) (f : X _⦋n + 1⦌ ⟶ T),
    DegeneraciesVanish f ↔
      Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
        (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
⊢ DegeneraciesVanish f ↔
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n ⟶ T) (HomologicalComplex.Hom.f QInfty n ≫ f) 0

Tactic:
obtain _ | n := n
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
T : C
f : X _⦋0⦌ ⟶ T
⊢ DegeneraciesVanish f ↔
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0 ⟶ T) (HomologicalComplex.Hom.f QInfty 0 ≫ f) 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
⊢ DegeneraciesVanish f ↔
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
      (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0

Tactic:
⟨fun hf ↦ ?_, fun hf ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
succ :
  ∀ (hf : DegeneraciesVanish f),
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
      (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
succ₁ :
  ∀
    (hf :
      Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
        (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0),
    DegeneraciesVanish f
⊢ DegeneraciesVanish f ↔
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
      (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : DegeneraciesVanish f
⊢ Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
    (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0

Tactic:
simp [QInfty_f, decomposition_Q, Preadditive.sum_comp, hf.σ_comp]

Premises used: AlgebraicTopology.DoldKan.DegeneraciesVanish.σ_comp, AlgebraicTopology.DoldKan.QInfty_f, CategoryTheory.Preadditive.sum_comp, AlgebraicTopology.DoldKan.decomposition_Q
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf :
  Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
    (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
⊢ HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
      f =
    𝟙 (HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1)) ≫ f

Tactic:
have := PInfty_f_add_QInfty_f (n + 1) =≫ f
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf :
  Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
    (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
this :
  HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
      f =
    𝟙 (HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1)) ≫ f
⊢ HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
      f =
    f

Tactic:
rw [Category.id_comp] at this

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf :
  Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
    (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
this :
  HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
      f =
    f
succ :
  ∀ (i : Fin (n + 1)),
    X.σ i ≫
        HAdd.hAdd (α :=
            HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
              HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
            (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
          f =
      0
⊢ DegeneraciesVanish f

Tactic:
rw [degeneraciesVanish_succ_iff, ← this]

Premises used: AlgebraicTopology.DoldKan.degeneraciesVanish_succ_iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf :
  Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
    (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
this :
  HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
      f =
    f
⊢ ∀ (i : Fin (n + 1)),
    X.σ i ≫
        HAdd.hAdd (α :=
            HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
              HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
            (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
          f =
      0

Tactic:
simp [hf]
-- Module: Mathlib.AlgebraicTopology.DoldKan.Equivalence
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
⊢ Eq (α := ChainComplex.{v_1, u_1, 0} A ℕ ⥤ SimplicialObject.{v_1, u_1} A) (Equivalence.inverse equivalence) Γ

Tactic:
rfl

Premises used: CategoryTheory.Idempotents.DoldKan.Γ, CategoryTheory.Functor.comp, AlgebraicTopology.DoldKan.Γ₀, CategoryTheory.Abelian.DoldKan.Γ, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
α : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))
  (Functor.obj N (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)) :=
  Functor.mapIso N (Iso.app Γ₂N₂ P)
β : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N P))
  (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P)) :=
  Iso.app N₂Γ₂ (Functor.obj N P)
symm :
  Eq (α := Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N P) (Functor.obj N P))
    (𝟙 (Functor.obj N P))
    (CategoryStruct.comp (Y :=
      Functor.obj N (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ (Functor.obj N P)))
      (Functor.map N (NatTrans.app (Iso.hom Γ₂N₂) P)) (NatTrans.app (Iso.hom N₂Γ₂) (Functor.obj N P)))
⊢ Eq (α := Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N P) (Functor.obj N P))
    (CategoryStruct.comp (Y :=
      Functor.obj N (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ (Functor.obj N P)))
      (Functor.map N (NatTrans.app (Iso.hom Γ₂N₂) P)) (NatTrans.app (Iso.hom N₂Γ₂) (Functor.obj N P)))
    (𝟙 (Functor.obj N P))

Tactic:
symm
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
α : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))
  (Functor.obj N (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)) :=
  Functor.mapIso N (Iso.app Γ₂N₂ P)
β : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N P))
  (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P)) :=
  Iso.app N₂Γ₂ (Functor.obj N P)
change : 𝟙 (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)) = α.hom ≫ β.hom
⊢ Eq (α := Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N P) (Functor.obj N P))
    (𝟙 (Functor.obj N P))
    (CategoryStruct.comp (Y :=
      Functor.obj N (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ (Functor.obj N P)))
      (Functor.map N (NatTrans.app (Iso.hom Γ₂N₂) P)) (NatTrans.app (Iso.hom N₂Γ₂) (Functor.obj N P)))

Tactic:
change 𝟙 _ = α.hom ≫ β.hom

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
α : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))
  (Functor.obj N (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)) :=
  Functor.mapIso N (Iso.app Γ₂N₂ P)
β : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N P))
  (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P)) :=
  Iso.app N₂Γ₂ (Functor.obj N P)
rw : β.inv ≫ α.inv = 𝟙 (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P))
⊢ 𝟙 (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)) = α.hom ≫ β.hom

Tactic:
rw [← Iso.inv_comp_eq, comp_id, ← comp_id β.hom, ← Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
α : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))
  (Functor.obj N (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)) :=
  Functor.mapIso N (Iso.app Γ₂N₂ P)
β : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N P))
  (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P)) :=
  Iso.app N₂Γ₂ (Functor.obj N P)
⊢ β.inv ≫ α.inv = 𝟙 (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P))

Tactic:
AlgebraicTopology.DoldKan.identity_N₂_objectwise P

Premises used: AlgebraicTopology.DoldKan.identity_N₂_objectwise