mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_2 Edge._proof_2).op)) e.edge) =
    (id x).edge

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_2 Edge._proof_2).op)) e.edge) =
    e.edge

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
⊢ s ∈ (nerve X).nonDegenerate n ↔ Function.Injective s.obj

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_2 Edge._proof_2).op)) e.edge) =
    e.edge

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
a : Fin (n + 1)
⊢ i.succAboveOrderEmb a ∈ {i}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
a b : Fin (n + 1)
h : (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) a = (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) b
⊢ i.succAboveOrderEmb a = i.succAboveOrderEmb b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
hj✝ : j ∈ {0}ᶜ
hj : ¬j = 0
⊢ (fun a ↦ ⟨(succAboveOrderEmb 0) a, ⋯⟩) (j.pred hj) = ⟨j, hj✝⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
hj✝ : j ∈ {i.succ}ᶜ
hj : ¬j = i.succ
⊢ (fun a ↦ ⟨i.succ.succAboveOrderEmb a, ⋯⟩) (i.predAbove j) = ⟨j, hj✝⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Function.Bijective fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
a b : Fin (n + 1)
⊢ (Equiv.ofBijective (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) ⋯) a ≤
      (Equiv.ofBijective (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) ⋯) b ↔
    a ≤ b

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_2 Edge._proof_2).op)) e.edge) =
    e.edge

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_2 Edge._proof_2).op)) e.edge) =
    (id y).edge

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_2 Edge._proof_2).op)) e.edge) =
    e.edge

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
⊢ a ∈ {a, b}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
⊢ b ∈ {a, b}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
x✝ : ↥{a, b}
x : α
hx : x ∈ {a, b}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩] a_1 = ⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ a ∈ {a, b, c}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ b ∈ {a, b, c}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ c ∈ {a, b, c}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
x✝ : ↥{a, b, c}
x : α
hx : x ∈ {a, b, c}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩, ⟨c, ⋯⟩] a_1 = ⟨x, hx⟩

Tactic:
by

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

Goal state before:
pp: C D : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v, u} D
F : C ⥤ D
x y : C
f : x ⟶ y
⊢ ComposableArrows.hom ((ConcreteCategory.hom ((nerveMap F).app (op ⦋1⦌))) (ComposableArrows.mk₁ f)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (F.map f)).hom ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
f : ComposableArrows C 0
⊢ 0 < 0 + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u
inst✝ : Preorder α
e : α ≃o Fin (n + 1)
X✝ : SimplexCategory
F : Fin (X✝.len + 1) ⥤ Fin (⦋n⦌.len + 1)
x : Fin (X✝.len + 1)
⊢ ((fun F ↦ F ⋙ ⋯.functor) ((fun F ↦ F ⋙ ⋯.functor) F)).obj x = F.obj x

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u
inst✝ : Preorder α
e : α ≃o Fin (n + 1)
X✝ : SimplexCategory
F : (nerve α).obj (op X✝)
x : Fin ((unop (op X✝)).len + 1)
⊢ ((fun F ↦ F ⋙ ⋯.functor) ((fun F ↦ F ⋙ ⋯.functor) F)).obj x = F.obj x

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.σ (nerve C) 0)) (ComposableArrows.mk₀ x)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (𝟙 x)).hom ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ f).hom ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ g).hom ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (f ≫ g)).hom ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
n : SimplexCategoryᵒᵖ
x y : (nerve C).obj n
h : x.obj = y.obj
⊢ ∀ (i : Fin ((unop n).len + 1)), x.obj i = y.obj i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
n : SimplexCategoryᵒᵖ
x y : (nerve C).obj n
h : x.obj = y.obj
⊢ ∀ (i : ℕ) (hi : i < (unop n).len),
    ComposableArrows.map' x i (i + 1) ⋯ hi = eqToHom ⋯ ≫ ComposableArrows.map' y i (i + 1) ⋯ hi ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.left e.edge = nerveEquiv x

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.right e.edge = nerveEquiv y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : ComposableArrows C 2
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) x) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (x.map' 0 1 δ₂_two._proof_1 δ₂_two._proof_3)).hom ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : ComposableArrows C 2
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) x) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (x.map' 1 2 δ₂_two._proof_3 δ₂_zero._proof_1)).hom ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
x y : ComposableArrows C 0
e : Edge x y
⊢ nerveEquiv x = ComposableArrows.left e.edge

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.right e.edge = nerveEquiv y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
x y : ComposableArrows C 0
e : Edge x y
⊢ (fun f ↦ Edge.mk (ComposableArrows.mk₁ f) ⋯ ⋯) ((fun e ↦ eqToHom ⋯ ≫ ComposableArrows.hom e.edge ≫ eqToHom ⋯) e) = e

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
x y : ComposableArrows C 0
f : nerveEquiv x ⟶ nerveEquiv y
⊢ (fun e ↦ eqToHom ⋯ ≫ ComposableArrows.hom e.edge ≫ eqToHom ⋯) ((fun f ↦ Edge.mk (ComposableArrows.mk₁ f) ⋯ ⋯) f) = f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.mk₁ (homEquiv e) = ComposableArrows.mk₁ (ComposableArrows.hom e.edge)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ edgeMk (𝟙 x) = Edge.id (nerveEquiv.symm x)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : C
e : Edge (nerveEquiv.symm x) (nerveEquiv.symm y)
⊢ x = nerveEquiv (nerveEquiv.symm x)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : C
e : Edge (nerveEquiv.symm x) (nerveEquiv.symm y)
⊢ nerveEquiv (nerveEquiv.symm y) = y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : C
e : Edge (nerveEquiv.symm x) (nerveEquiv.symm y)
⊢ edgeMk (eqToHom ⋯ ≫ homEquiv e ≫ eqToHom ⋯) = e

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : C
f : x ⟶ y
⊢ homEquiv.symm (homEquiv (edgeMk f)) = homEquiv.symm f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : ComposableArrows C 0
⊢ homEquiv (Edge.id x) = 𝟙 (nerveEquiv x)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) (ComposableArrows.mk₂ f₀₁ f₁₂) = (edgeMk f₀₁).edge

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) (ComposableArrows.mk₂ f₀₁ f₁₂) = (edgeMk f₁₂).edge

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) (ComposableArrows.mk₂ f₀₁ f₁₂) = (edgeMk (f₀₁ ≫ f₁₂)).edge

Tactic:
by

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

Goal state before:
pp: 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₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h : f₀₁ ≫ f₁₂ = f₀₂
⊢ (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)

Tactic:
by

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

Goal state before:
pp: 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₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) = ComposableArrows.mk₁ f₁₂
h₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
h'₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) =
    ComposableArrows.mk₁ f₁₂
h'₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
⊢ ComposableArrows.arrowEquiv.symm
      (Arrow.mk (ComposableArrows.map' h'.simplex 0 1 ComposableArrows.homMk₁._proof_4 _proof_246✝)) =
    ComposableArrows.arrowEquiv.symm
      (Arrow.mk (ComposableArrows.map' h.simplex 0 1 ComposableArrows.homMk₁._proof_4 _proof_246✝))

Tactic:
by

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

Goal state before:
pp: 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₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) = ComposableArrows.mk₁ f₁₂
h₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
h'₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) =
    ComposableArrows.mk₁ f₁₂
h'₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
⊢ ComposableArrows.arrowEquiv.symm (Arrow.mk (ComposableArrows.map' h'.simplex 1 2 _proof_246✝ _proof_247✝)) =
    ComposableArrows.arrowEquiv.symm (Arrow.mk (ComposableArrows.map' h.simplex 1 2 _proof_246✝ _proof_247✝))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
⊢ Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)) ↔ f₀₁ ≫ f₁₂ = f₀₂

Tactic:
by

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

Goal state before:
pp: i j : ℕ
h : (up ℕ).Rel i j
⊢ Odd (i + j)

Tactic:
by

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

Goal state before:
pp: i j : ℕ
h : (down ℕ).Rel i j
⊢ Odd (i + j)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j : ℕ
⊢ ¬c.Rel i j → (if hij : c.Rel i j then if hi : Even i then φ else ψ else 0) = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : Even i
hj : Even j
⊢ Odd i

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ (ConcreteCategory.hom (SimplicialObject.σ (nerve C) 0)) (nerveEquiv.symm x) = ComposableArrows.mk₁ (𝟙 x)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : Category.{v, u} D
x y : C
f : x ⟶ y
F : C ⥤ D
⊢ homEquiv ((edgeMk f).map (nerveMap F)) = F.map f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : ¬Even i
hj : ¬Even j
⊢ Even j

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
⊢ ((if hij : c.Rel i j then if hi : Even i then φ else ψ else 0) ≫
      if hij : c.Rel j k then if hi : Even j then φ else ψ else 0) =
    0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
hi : Even i
this : Odd (i + j)
⊢ Odd i

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
⊢ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₁).hom ≫
      { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }.f =
    ((alternatingConst A hOdd hEven hc).sc' i j k).f ≫ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
⊢ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂).hom ≫
      { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }.g =
    ((alternatingConst A hOdd hEven hc).sc' i j k).g ≫ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₃).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
hi : ¬Even i
this : Odd (i + j)
⊢ Even j

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
⊢ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₁).hom ≫
      { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd }.f =
    ((alternatingConst A hOdd hEven hc).sc' i j k).f ≫ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
⊢ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂).hom ≫
      { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd }.g =
    ((alternatingConst A hOdd hEven hc).sc' i j k).g ≫ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₃).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝¹ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Even j
⊢ (alternatingConst A hOdd hEven hc).iCycles j ≫ φ = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝¹ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Odd j
⊢ (alternatingConst A hOdd hEven hc).iCycles j ≫ ψ = 0

Tactic:
by

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

Goal state before:
pp: 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
⊢ f ≫ (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯).d i j = (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯).d i j ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : Even n
h₀ : n ≠ 0
⊢ (HomologicalComplex.sc (alternatingConst.obj X) n).f = 0

Tactic:
by

Goal state after: