mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Augmented C
n✝ : SimplexCategoryᵒᵖ
⊢ ({ app := fun A ↦ { left := whiskerLeft (drop.obj A) (x✝² ≫ x✝¹), right := (x✝² ≫ x✝¹).app (point.obj A), w := ⋯ },
                naturality := ⋯ }.app
            x✝).left.app
      n✝ =
    (({ app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝², right := x✝².app (point.obj A), w := ⋯ },
                  naturality := ⋯ } ≫
                { app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝¹, right := x✝¹.app (point.obj A), w := ⋯ },
                  naturality := ⋯ }).app
            x✝).left.app
      n✝

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Augmented C
⊢ ({ app := fun A ↦ { left := whiskerLeft (drop.obj A) (x✝² ≫ x✝¹), right := (x✝² ≫ x✝¹).app (point.obj A), w := ⋯ },
            naturality := ⋯ }.app
        x✝).right =
    (({ app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝², right := x✝².app (point.obj A), w := ⋯ },
              naturality := ⋯ } ≫
            { app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝¹, right := x✝¹.app (point.obj A), w := ⋯ },
              naturality := ⋯ }).app
        x✝).right

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Augmented C
n✝ : SimplexCategoryᵒᵖ
⊢ ({ app := fun A ↦ { left := whiskerLeft (drop.obj A) (x✝² ≫ x✝¹), right := (x✝² ≫ x✝¹).app (point.obj A), w := ⋯ },
                naturality := ⋯ }.app
            x✝).left.app
      n✝ =
    (({ app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝², right := x✝².app (point.obj A), w := ⋯ },
                  naturality := ⋯ } ≫
                { app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝¹, right := x✝¹.app (point.obj A), w := ⋯ },
                  naturality := ⋯ }).app
            x✝).left.app
      n✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Augmented C
⊢ ({ app := fun A ↦ { left := whiskerLeft (drop.obj A) (x✝² ≫ x✝¹), right := (x✝² ≫ x✝¹).app (point.obj A), w := ⋯ },
            naturality := ⋯ }.app
        x✝).right =
    (({ app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝², right := x✝².app (point.obj A), w := ⋯ },
              naturality := ⋯ } ≫
            { app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝¹, right := x✝¹.app (point.obj A), w := ⋯ },
              naturality := ⋯ }).app
        x✝).right
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑0 • X.δ 0) + 0 =
    NormalizedMooreComplex.objD X i ≫ (NormalizedMooreComplex.objX X i).arrow

Tactic:
rw [add_zero, Fin.val_zero, pow_zero, one_zsmul]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ X.δ 0 =
    NormalizedMooreComplex.objD X i ≫ (NormalizedMooreComplex.objX X i).arrow
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case zero
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 =
    (match 0 with
      | 0 => (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow
      | n.succ =>
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
          ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯) ≫
      (match 0 with
        | 0 => ⊤
        | n.succ => Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow

pp: case succ
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
n✝ : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 =
    (match n✝ + 1 with
      | 0 => (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow
      | n.succ =>
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
          ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯) ≫
      (match n✝ + 1 with
        | 0 => ⊤
        | n.succ => Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow

Tactic:
<;>

Goal state after:
case zero
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 =
    (match 0 with
      | 0 => (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow
      | n.succ =>
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
          ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯) ≫
      (match 0 with
        | 0 => ⊤
        | n.succ => Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow

case succ
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
n✝ : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 =
    (match n✝ + 1 with
      | 0 => (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow
      | n.succ =>
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
          ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯) ≫
      (match n✝ + 1 with
        | 0 => ⊤
        | n.succ => Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ ((whiskeringObj C D X✝).map f ≫ { left := η.app (point.obj x✝), right := whiskerLeft (drop.obj x✝) η, w := ⋯ }).left =
    ({ left := η.app (point.obj x✝¹), right := whiskerLeft (drop.obj x✝¹) η, w := ⋯ } ≫
        (whiskeringObj C D Y✝).map f).left

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
n✝ : SimplexCategory
⊢ ((whiskeringObj C D X✝).map f ≫
            { left := η.app (point.obj x✝), right := whiskerLeft (drop.obj x✝) η, w := ⋯ }).right.app
      n✝ =
    ({ left := η.app (point.obj x✝¹), right := whiskerLeft (drop.obj x✝¹) η, w := ⋯ } ≫
            (whiskeringObj C D Y✝).map f).right.app
      n✝

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ ((whiskeringObj C D X✝).map f ≫ { left := η.app (point.obj x✝), right := whiskerLeft (drop.obj x✝) η, w := ⋯ }).left =
    ({ left := η.app (point.obj x✝¹), right := whiskerLeft (drop.obj x✝¹) η, w := ⋯ } ≫
        (whiskeringObj C D Y✝).map f).left

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
n✝ : SimplexCategory
⊢ ((whiskeringObj C D X✝).map f ≫
            { left := η.app (point.obj x✝), right := whiskerLeft (drop.obj x✝) η, w := ⋯ }).right.app
      n✝ =
    ({ left := η.app (point.obj x✝¹), right := whiskerLeft (drop.obj x✝¹) η, w := ⋯ } ≫
            (whiskeringObj C D Y✝).map f).right.app
      n✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : ¬y = i
⊢ (Hom.toOrderHom θ) y.succ = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) y)

Tactic:
dsimp [δ]
      rw [Fin.succAbove_of_le_castSucc i.succ _]
      simp only [Fin.lt_def, Fin.le_iff_val_le_val, Fin.val_succ, Fin.val_castSucc,
        Nat.lt_succ_iff, Fin.ext_iff] at h' h'' ⊢
      lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y

Tactic:
rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩

Goal state after:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case h.last
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
x : Fin (Δ.len + 1)
j : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
hj : j ≠ Fin.last (n + 1)
⊢ (Fin.last (n + 1)).succAbove (((Fin.last n).predAbove (Fin.last (n + 1))).predAbove j) = j

pp: case h.cast
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
x : Fin (Δ.len + 1)
j : Fin (n + 2)
i✝ : Fin (n + 1)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i✝.castSucc
hj : j ≠ i✝.castSucc
⊢ i✝.castSucc.succAbove (((Fin.last n).predAbove i✝.castSucc).predAbove j) = j

Tactic:
<;>

Goal state after:
case h.last
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
x : Fin (Δ.len + 1)
j : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
hj : j ≠ Fin.last (n + 1)
⊢ (Fin.last (n + 1)).succAbove (((Fin.last n).predAbove (Fin.last (n + 1))).predAbove j) = j

case h.cast
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
x : Fin (Δ.len + 1)
j : Fin (n + 2)
i✝ : Fin (n + 1)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i✝.castSucc
hj : j ≠ i✝.castSucc
⊢ i✝.castSucc.succAbove (((Fin.last n).predAbove i✝.castSucc).predAbove j) = j
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ Arrow.Hom.left (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)) = Arrow.Hom.left A

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ Arrow.Hom.right (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)) = Arrow.Hom.right A

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ Arrow.Hom.left (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)) = Arrow.Hom.left A

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ Arrow.Hom.right (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)) = Arrow.Hom.right A
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
⊢ X.nonDegenerate 0 = Set.univ

Tactic:
by
  simp [nonDegenerate]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n ↔ x ∉ X.nonDegenerate n

Tactic:
by
  simp [nonDegenerate]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case a
X : SSet
x✝¹ x✝ : X.N
h : x✝¹.subcomplex = x✝.subcomplex
⊢ x✝¹ ≤ x✝

pp: case a
X : SSet
x✝¹ x✝ : X.N
h : x✝¹.subcomplex = x✝.subcomplex
⊢ x✝ ≤ x✝¹

Tactic:
<;>

Goal state after:
case a
X : SSet
x✝¹ x✝ : X.N
h : x✝¹.subcomplex = x✝.subcomplex
⊢ x✝¹ ≤ x✝

case a
X : SSet
x✝¹ x✝ : X.N
h : x✝¹.subcomplex = x✝.subcomplex
⊢ x✝ ≤ x✝¹
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : X _⦋m⦌
hx : (ConcreteCategory.hom (X.map f.op)) y ∈ A.obj (op ⦋n⦌)
this : IsSplitEpi f
⊢ y ∈ A.obj (op ⦋m⦌)

Tactic:
simpa [Set.mem_preimage, ← op_comp, ← comp_apply, ← Functor.map_comp] using
      A.map (section_ f).op hx

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: case e'_2.e'_6
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : (nerveEquiv (nerveEquiv.symm x₀) ⟶ nerveEquiv (nerveEquiv.symm x₂)) = (x₀ ⟶ x₂)
e_3✝ : nerveEquiv (nerveEquiv.symm x₀) = x₀
e_4✝ : nerveEquiv (nerveEquiv.symm x₁) = x₁
⊢ homEquiv (edgeMk f₀₁) = f₀₁

pp: case e'_2.e'_7
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : (nerveEquiv (nerveEquiv.symm x₀) ⟶ nerveEquiv (nerveEquiv.symm x₂)) = (x₀ ⟶ x₂)
e_4✝ : nerveEquiv (nerveEquiv.symm x₁) = x₁
e_5✝ : nerveEquiv (nerveEquiv.symm x₂) = x₂
⊢ homEquiv (edgeMk f₁₂) = f₁₂

pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : (nerveEquiv (nerveEquiv.symm x₀) ⟶ nerveEquiv (nerveEquiv.symm x₂)) = (x₀ ⟶ x₂)
⊢ homEquiv (edgeMk f₀₂) = f₀₂

Tactic:
<;>

Goal state after:
case e'_2.e'_6
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : (nerveEquiv (nerveEquiv.symm x₀) ⟶ nerveEquiv (nerveEquiv.symm x₂)) = (x₀ ⟶ x₂)
e_3✝ : nerveEquiv (nerveEquiv.symm x₀) = x₀
e_4✝ : nerveEquiv (nerveEquiv.symm x₁) = x₁
⊢ homEquiv (edgeMk f₀₁) = f₀₁

case e'_2.e'_7
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : (nerveEquiv (nerveEquiv.symm x₀) ⟶ nerveEquiv (nerveEquiv.symm x₂)) = (x₀ ⟶ x₂)
e_4✝ : nerveEquiv (nerveEquiv.symm x₁) = x₁
e_5✝ : nerveEquiv (nerveEquiv.symm x₂) = x₂
⊢ homEquiv (edgeMk f₁₂) = f₁₂

case e'_3
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : (nerveEquiv (nerveEquiv.symm x₀) ⟶ nerveEquiv (nerveEquiv.symm x₂)) = (x₀ ⟶ x₂)
⊢ homEquiv (edgeMk f₀₂) = f₀₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : ComposableArrows C 0
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ homEquiv e₀₁ ≫ homEquiv e₁₂ = homEquiv e₀₂

Tactic:
obtain ⟨x₀, rfl⟩ := nerveEquiv.symm.surjective x₀
  obtain ⟨x₁, rfl⟩ := nerveEquiv.symm.surjective x₁
  obtain ⟨x₂, rfl⟩ := nerveEquiv.symm.surjective x₂
  obtain ⟨f₀₁, rfl⟩ := edgeMk_surjective e₀₁
  obtain ⟨f₁₂, rfl⟩ := edgeMk_surjective e₁₂
  obtain ⟨f₀₂, rfl⟩ := edgeMk_surjective e₀₂
  convert! (nerve.nonempty_compStruct_iff _ _ _).1 ⟨h⟩ <;> apply homEquiv_edgeMk

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

Goal state before:
pp: case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i j : ℕ
hij : (ComplexShape.down ℕ).Rel i j
h✝ : Even i
⊢ f ≫ (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯).d i j = (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯).d i j ≫ f

pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i j : ℕ
hij : (ComplexShape.down ℕ).Rel i j
h✝ : ¬Even i
⊢ f ≫ (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯).d i j = (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯).d i j ≫ f

Tactic:
<;>

Goal state after:
case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i j : ℕ
hij : (ComplexShape.down ℕ).Rel i j
h✝ : Even i
⊢ f ≫ (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯).d i j = (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯).d i j ≫ f

case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i j : ℕ
hij : (ComplexShape.down ℕ).Rel i j
h✝ : ¬Even i
⊢ f ≫ (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯).d i j = (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯).d i j ≫ f
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case zero
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
hn : Even 0
h₀ : 0 ≠ 0
⊢ ∀ (Z : C) (g : Z ⟶ (HomologicalComplex.sc (alternatingConst.obj X) 0).X₂),
    g ≫ (HomologicalComplex.sc (alternatingConst.obj X) 0).g = 0 → g = 0

pp: case succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n✝ : ℕ
hn : Even (n✝ + 1)
h₀ : n✝ + 1 ≠ 0
⊢ ∀ (Z : C) (g : Z ⟶ (HomologicalComplex.sc (alternatingConst.obj X) (n✝ + 1)).X₂),
    g ≫ (HomologicalComplex.sc (alternatingConst.obj X) (n✝ + 1)).g = 0 → g = 0

Tactic:
<;>

Goal state after:
case zero
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
hn : Even 0
h₀ : 0 ≠ 0
⊢ ∀ (Z : C) (g : Z ⟶ (HomologicalComplex.sc (alternatingConst.obj X) 0).X₂),
    g ≫ (HomologicalComplex.sc (alternatingConst.obj X) 0).g = 0 → g = 0

case succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n✝ : ℕ
hn : Even (n✝ + 1)
h₀ : n✝ + 1 ≠ 0
⊢ ∀ (Z : C) (g : Z ⟶ (HomologicalComplex.sc (alternatingConst.obj X) (n✝ + 1)).X₂),
    g ≫ (HomologicalComplex.sc (alternatingConst.obj X) (n✝ + 1)).g = 0 → g = 0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
j : ℕ
⊢ (C.augment f w).d (0 + 1) (j + 1) = C.d 0 j

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
j n✝ : ℕ
⊢ (C.augment f w).d (n✝ + 1 + 1) (j + 1) = C.d (n✝ + 1) j

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
j : ℕ
⊢ (C.augment f w).d (0 + 1) (j + 1) = C.d 0 j

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
j n✝ : ℕ
⊢ (C.augment f w).d (n✝ + 1 + 1) (j + 1) = C.d (n✝ + 1) j
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i : ℕ
⊢ (ComplexShape.down ℕ).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 : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i n✝ : ℕ
⊢ (ComplexShape.down ℕ).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 : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i : ℕ
⊢ (ComplexShape.down ℕ).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 : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i n✝ : ℕ
⊢ (ComplexShape.down ℕ).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 : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 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 : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i : ℕ
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f
      (i + 1) =
    (𝟙 (truncate.obj (C.augment f w))).f (i + 1)

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 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 : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i : ℕ
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f
      (i + 1) =
    (𝟙 (truncate.obj (C.augment f w))).f (i + 1)
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 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 : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i : ℕ
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f
      (i + 1) =
    (𝟙 C).f (i + 1)

Tactic:
<;>

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 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 : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i : ℕ
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f
      (i + 1) =
    (𝟙 C).f (i + 1)