mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
s : ¬(ComplexShape.up ℕ).Rel i 0
⊢ (match i, 0 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

pp: case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
s : ¬(ComplexShape.up ℕ).Rel i (0 + 1)
⊢ (match i, 0 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

pp: case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
s : ¬(ComplexShape.up ℕ).Rel i (j + 1 + 1)
⊢ (match i, j + 1 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
s : ¬(ComplexShape.up ℕ).Rel i 0
⊢ (match i, 0 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
s : ¬(ComplexShape.up ℕ).Rel i (0 + 1)
⊢ (match i, 0 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
s : ¬(ComplexShape.up ℕ).Rel i (j + 1 + 1)
⊢ (match i, j + 1 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel j 0
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

pp: case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel j (0 + 1)
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

pp: case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel j (k + 1 + 1)
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel j 0
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel j (0 + 1)
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel j (k + 1 + 1)
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
f : unop x✝¹ ⟶ ⦋n⦌
x✝ : objEquiv.symm f ∈ ⊤.obj x✝¹
⊢ ∃ f_1, (ConcreteCategory.hom (Δ[n].map f_1.op)) (objEquiv.symm (𝟙 ⦋n⦌)) = objEquiv.symm f

Tactic:
exact ⟨f, by simp [map_objEquiv_symm.{u}]⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i 0 → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i 0 = C.d i 0 ≫ 𝟙 (C.X 0)

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i n✝ : ℕ
⊢ (ComplexShape.up ℕ).Rel i (n✝ + 1) →
    𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i (n✝ + 1) = C.d i (n✝ + 1) ≫ 𝟙 (C.X (n✝ + 1))

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i 0 → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i 0 = C.d i 0 ≫ 𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i n✝ : ℕ
⊢ (ComplexShape.up ℕ).Rel i (n✝ + 1) →
    𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i (n✝ + 1) = C.d i (n✝ + 1) ≫ 𝟙 (C.X (n✝ + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f 0 =
    (𝟙 (truncate.obj (C.augment f w))).f 0

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
n✝ : ℕ
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 (truncate.obj (C.augment f w))).f (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f 0 =
    (𝟙 (truncate.obj (C.augment f w))).f 0

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
n✝ : ℕ
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 (truncate.obj (C.augment f w))).f (n✝ + 1)
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f 0 =
    (𝟙 C).f 0

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
n✝ : ℕ
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 C).f (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f 0 =
    (𝟙 C).f 0

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
n✝ : ℕ
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 C).f (n✝ + 1)
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case zero
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.succAbove 0) =
    shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) ∘ ⇑i.succAboveOrderEmb) 0

pp: case succ
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
i✝ : Fin (unop (op ⦋n + 1⦌)).len
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.succAbove i✝.succ) =
    shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) ∘ ⇑i.succAboveOrderEmb) i✝.succ

Tactic:
<;>

Goal state after:
case zero
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.succAbove 0) =
    shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) ∘ ⇑i.succAboveOrderEmb) 0

case succ
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
i✝ : Fin (unop (op ⦋n + 1⦌)).len
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.succAbove i✝.succ) =
    shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) ∘ ⇑i.succAboveOrderEmb) i✝.succ
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i 0 →
    (match i with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 0 1) ⋯).d i 0 =
      C.d i 0 ≫
        match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

pp: case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i (0 + 1) →
    (match i with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 0 1) ⋯).d i (0 + 1) =
      C.d i (0 + 1) ≫
        match 0 + 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

pp: case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i (j + 1 + 1) →
    (match i with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 0 1) ⋯).d i (j + 1 + 1) =
      C.d i (j + 1 + 1) ≫
        match j + 1 + 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i 0 →
    (match i with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 0 1) ⋯).d i 0 =
      C.d i 0 ≫
        match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i (0 + 1) →
    (match i with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 0 1) ⋯).d i (0 + 1) =
      C.d i (0 + 1) ≫
        match 0 + 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i (j + 1 + 1) →
    (match i with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 0 1) ⋯).d i (j + 1 + 1) =
      C.d i (j + 1 + 1) ≫
        match j + 1 + 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case zero
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.predAbove 0) =
    shiftFun (fun x ↦ (SimplexCategory.Hom.toOrderHom φ.down) (i.predAbove x)) 0

pp: case succ
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
i✝ : Fin (unop (op ⦋n + 1 + 1⦌)).len
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.predAbove i✝.succ) =
    shiftFun (fun x ↦ (SimplexCategory.Hom.toOrderHom φ.down) (i.predAbove x)) i✝.succ

Tactic:
<;>

Goal state after:
case zero
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.predAbove 0) =
    shiftFun (fun x ↦ (SimplexCategory.Hom.toOrderHom φ.down) (i.predAbove x)) 0

case succ
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
i✝ : Fin (unop (op ⦋n + 1 + 1⦌)).len
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.predAbove i✝.succ) =
    shiftFun (fun x ↦ (SimplexCategory.Hom.toOrderHom φ.down) (i.predAbove x)) i✝.succ
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
⊢ Fin.cases ((WidePullback.base fun x ↦ f.hom) ≫ S.section_) (WidePullback.π fun x ↦ f.hom) 0 ≫ f.hom =
    WidePullback.base fun x ↦ f.hom

pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i✝ : Fin (unop (op ⦋n + 1⦌)).len
⊢ Fin.cases ((WidePullback.base fun x ↦ f.hom) ≫ S.section_) (WidePullback.π fun x ↦ f.hom) i✝.succ ≫ f.hom =
    WidePullback.base fun x ↦ f.hom

Tactic:
<;>

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
⊢ Fin.cases ((WidePullback.base fun x ↦ f.hom) ≫ S.section_) (WidePullback.π fun x ↦ f.hom) 0 ≫ f.hom =
    WidePullback.base fun x ↦ f.hom

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i✝ : Fin (unop (op ⦋n + 1⦌)).len
⊢ Fin.cases ((WidePullback.base fun x ↦ f.hom) ≫ S.section_) (WidePullback.π fun x ↦ f.hom) i✝.succ ≫ f.hom =
    WidePullback.base fun x ↦ f.hom
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) 0 =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) 0

pp: case a.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
i✝ : Fin (n + 1)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ

Tactic:
<;>

Goal state after:
case a.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) 0 =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) 0

case a.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
i✝ : Fin (n + 1)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.predAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) 0 =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.predAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S (n + 1)) ≫
      WidePullback.π (fun x ↦ f.hom) 0

pp: case a.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
i✝ : Fin (n + 2)
⊢ (ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.predAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.predAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S (n + 1)) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ

Tactic:
<;>

Goal state after:
case a.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.predAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) 0 =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.predAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S (n + 1)) ≫
      WidePullback.π (fun x ↦ f.hom) 0

case a.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
i✝ : Fin (n + 2)
⊢ (ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.predAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.predAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S (n + 1)) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ : I₂
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₂.ε₂ c₁ c₁₂ (i₂, i₁) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)

Tactic:
ComplexShape.σ_ε₁ c₂ c₁₂ h₁ i₂,

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ : I₂
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
⊢ c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁' i₂ * c₂.ε₂ c₁ c₁₂ (i₂, i₁) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} C₃
inst✝³ : Category.{v_4, u_4} C₄
inst✝² : Category.{v_5, u_5} C₁₂
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₁₂ : ρ₁₂.I₁₂
h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂
⊢ ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h =
    (G.map (ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃) ≫
      ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ⋯

Tactic:
subst h₁₂
  rfl

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
⊢ map (𝟙 K) c₁₂ = 𝟙 (K.total c₁₂)

Tactic:
apply (HomologicalComplex.forget _ _).map_injective

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
⊢ (HomologicalComplex.forget C c₁₂).map (map (𝟙 K) c₁₂) = (HomologicalComplex.forget C c₁₂).map (𝟙 (K.total c₁₂))
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : DecidableEq I₁₂
inst✝² : K.HasTotal c₁₂
inst✝¹ : L.HasTotal c₁₂
inst✝ : M.HasTotal c₁₂
⊢ map (φ ≫ ψ) c₁₂ = map φ c₁₂ ≫ map ψ c₁₂

Tactic:
apply (HomologicalComplex.forget _ _).map_injective

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : DecidableEq I₁₂
inst✝² : K.HasTotal c₁₂
inst✝¹ : L.HasTotal c₁₂
inst✝ : M.HasTotal c₁₂
⊢ (HomologicalComplex.forget C c₁₂).map (map (φ ≫ ψ) c₁₂) =
    (HomologicalComplex.forget C c₁₂).map (map φ c₁₂ ≫ map ψ c₁₂)