mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : ChainComplex C ℕ
Δ : SimplexCategory
⊢ mapMono K (𝟙 Δ) = 𝟙 (K.X Δ.len)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
this : Δ ≠ Δ'
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = K.d Δ.len Δ'.len

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ mapMono K i = K.d Δ.len Δ'.len

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
Z : C
Δ : SimplexCategoryᵒᵖ
F : (A : IndexSet Δ) → s.N (unop A.fst).len ⟶ Z
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ s.desc Δ F = F A

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : SimplicialObject C
s : X.Splitting
e : X ≅ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ (e.app Δ).hom = (cofan' s.N Y (fun n ↦ s.ι n ≫ e.hom.app (op ⦋n⦌)) Δ).inj A

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : ChainComplex C ℕ
n : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ ↑i < n + 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ i = ⟨↑i, ⋯⟩.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ mapMono K i = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (s.cofan Δ₁).inj A ≫ X.map p = (s.cofan Δ₂).inj (A.epiComp p)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = ⟨↑i, ⋯⟩.castSucc
⊢ n + 1 + 1 ≤ ↑j.rev.succ + q

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₂ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₂, comm := c₂ }.f n
⊢ f₁ = f₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ mapMono K i ≫ f.f Δ.len = f.f Δ'.len ≫ mapMono K' i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁.Hom S₂
h : ∀ (n : ℕ), Φ₁.f n = Φ₂.f n
⊢ Φ₁ = Φ₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ Z✝ : Split C
Φ₁₂ : X✝.Hom Y✝
Φ₂₃ : Y✝.Hom Z✝
n : ℕ
⊢ X✝.s.ι n ≫ (Φ₁₂.F ≫ Φ₂₃.F).app (op ⦋n⦌) = (Φ₁₂.f n ≫ Φ₂₃.f n) ≫ Z✝.s.ι n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
⊢ Δ.len = Δ''.len + (k + k' + 2)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
⊢ Φ₁.f = Φ₂.f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
n : ℕ
⊢ Φ₁.f n = Φ₂.f n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ = Φ.f (unop A.fst).len ≫ (S₂.s.cofan Δ).inj A

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
⊢ X.σ i ≫ (P (q + 1)).f (n + 1 + 1) = 0

Tactic:
rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp,
          P_succ]
        have v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i) :=
          (HigherFacesVanish.of_P q n).comp_σ hi
        dsimp only [AlternatingFaceMapComplex.obj_X, Nat.succ_eq_add_one, HomologicalComplex.comp_f,
          HomologicalComplex.add_f_apply, HomologicalComplex.id_f]
        rw [← assoc, v.comp_P_eq_self, Preadditive.comp_add,
          comp_id, v.comp_Hσ_eq hi, assoc, ← Fin.succ_mk _ _ i.2,
          SimplicialObject.δ_comp_σ_succ_assoc,
          Fin.eta, decomposition_Q n q, sum_comp, sum_comp, Finset.sum_eq_zero, add_zero,
          add_neg_eq_zero]
        intro j hj
        simp only [Finset.mem_univ, Finset.mem_filter] at hj
        obtain ⟨k, hk⟩ := Nat.le.dest (Nat.lt_succ_iff.mp (Fin.is_lt j))
        rw [add_comm] at hk
        have hi' : i = Fin.castSucc ⟨i, by lia⟩ := by
          ext
          simp only [Fin.castSucc_mk, Fin.eta]
        have eq := hq j.rev.succ (by
          simp only [← hk, Fin.rev_eq j hk.symm, Fin.succ_mk, Fin.val_mk]
          lia)
        rw [assoc, assoc, assoc, hi',
          SimplicialObject.σ_comp_σ_assoc, reassoc_of% eq, zero_comp, comp_zero, comp_zero,
          comp_zero]
        simp only [Fin.rev_eq j hk.symm, Fin.le_iff_val_le_val]
        lia

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ j ∈ Finset.univ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ (AlgebraicTopology.inclusionOfMooreComplexMap X).f (n + 1) ≫ X.δ j.succ = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q
⊢ X.σ i ≫ (P q).f (n + 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ PInfty.f (n + 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X n).Factors (PInfty.f n)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Homotopy (P (q + 1)) (𝟙 K[X])

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).factorThru (PInfty.f (n + 1)) ⋯ ≫ N[X].d (n + 1) n =
    K[X].d (n + 1) n ≫ (NormalizedMooreComplex.objX X n).factorThru (PInfty.f n) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n < q
⊢ (homotopyPToId X (q + 1)).hom n (n + 1) = (homotopyPToId X q).hom n (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ PInftyToNormalizedMooreComplex X ≫ inclusionOfMooreComplexMap X = PInfty

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Sigma.ι (summand K Δ) A ≫ map K θ = Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X Y : SimplicialObject A
f : X ⟶ Y
⊢ AlternatingFaceMapComplex.map f ≫ PInftyToNormalizedMooreComplex Y =
    PInftyToNormalizedMooreComplex X ≫ NormalizedMooreComplex.map f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ PInfty ≫ PInftyToNormalizedMooreComplex X = PInftyToNormalizedMooreComplex X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
θ : ⦋n⦌ ⟶ Δ'
hθ : ¬Mono θ
⊢ X.map θ.op ≫ PInfty.f n = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X ≫ PInfty = inclusionOfMooreComplexMap X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f n =
    (((dNext n) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) + (prevD n) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) +
      (𝟙 K[X]).f n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
⊢ x✝¹ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
T : C
f : X _⦋n⦌ ⟶ T
hf : DegeneraciesVanish f
U : C
g : T ⟶ U
⊢ DegeneraciesVanish (f ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X ≫ PInftyToNormalizedMooreComplex X = 𝟙 ((normalizedMooreComplex A).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ { app := fun X ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ }, naturality := ⋯ } ≫
      { app := fun X ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ }, naturality := ⋯ } =
    𝟙 N₁

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ DegeneraciesVanish (PInfty.f n)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ { app := fun X ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ }, naturality := ⋯ } ≫
      { app := fun X ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ }, naturality := ⋯ } =
    𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
⊢ θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
T : C
f : X _⦋n⦌ ⟶ T
⊢ DegeneraciesVanish f ↔ QInfty.f n ≫ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ P.p.f n ≫ P.p.f n = P.p.f n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
⊢ colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K θ' ≫ Obj.map K θ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
hij : ¬c.Rel i j
⊢ { f := P.p.f i ≫ P.X.d i j, comm := ⋯ } = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex (Karoubi C) c
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
⊢ (K.d i j).f ≫ (K.d j k).f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex (Karoubi C) c
f : K ⟶ L
i j : ι
hij : c.Rel i j
⊢ (f.f i).f ≫ (obj L).X.d i j = (obj K).X.d i j ≫ (f.f j).f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : HomologicalComplex (Karoubi C) c
⊢ ((inverse ⋙ functor).obj P).X = ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P).X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : HomologicalComplex (Karoubi C) c
⊢ ∀ (i j : ι),
    c.Rel i j →
      ((inverse ⋙ functor).obj P).d i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P).d i j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ ∀ (X Y : HomologicalComplex (Karoubi C) c) (f : X ⟶ Y),
    (inverse ⋙ functor).map f = eqToHom ⋯ ≫ (𝟭 (HomologicalComplex (Karoubi C) c)).map f ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : c.Rel i j
⊢ P.p.f i ≫ ((functor ⋙ inverse).obj P).X.d i j = ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).X.d i j ≫ P.p.f j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
⊢ ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p ≫
      { f := fun n ↦ P.p.f n, comm' := ⋯ } ≫ ((functor ⋙ inverse).obj P).p =
    { f := fun n ↦ P.p.f n, comm' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
⊢ (𝟭 (Karoubi (HomologicalComplex C c))).map φ ≫ { f := { f := fun n ↦ Q.p.f n, comm' := ⋯ }, comm := ⋯ } =
    { f := { f := fun n ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ } ≫ (functor ⋙ inverse).map φ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (b : Splitting.IndexSet Δ),
    Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) b ≫
        (Iso.refl (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))).pt).hom =
      (Splitting.cofan' (fun n ↦ K.X n) (obj K)
            (fun n ↦ Sigma.ι (Obj.summand K (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌))) Δ).inj
        b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : c.Rel i j
⊢ P.p.f i ≫ ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).X.d i j = ((functor ⋙ inverse).obj P).X.d i j ≫ P.p.f j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
⊢ ((functor ⋙ inverse).obj P).p ≫
      { f := fun n ↦ P.p.f n, comm' := ⋯ } ≫ ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p =
    { f := fun n ↦ P.p.f n, comm' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
⊢ (functor ⋙ inverse).map φ ≫ { f := { f := fun n ↦ Q.p.f n, comm' := ⋯ }, comm := ⋯ } =
    { f := { f := fun n ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ } ≫ (𝟭 (Karoubi (HomologicalComplex C c))).map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ { app := fun P ↦ { f := { f := fun n ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ }, naturality := ⋯ } ≫
      { app := fun P ↦ { f := { f := fun n ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ }, naturality := ⋯ } =
    𝟙 (𝟭 (Karoubi (HomologicalComplex C c)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ { app := fun P ↦ { f := { f := fun n ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ }, naturality := ⋯ } ≫
      { app := fun P ↦ { f := { f := fun n ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ }, naturality := ⋯ } =
    𝟙 (functor ⋙ inverse)

Tactic:
by

Goal state after: