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

Goal state before:
pp: case mpr
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n → (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n

Tactic:
·

Goal state after:
case mpr
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n → (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: n m : ℕ
inst✝ : NeZero n
hm : n ≤ m
⊢ n ≤ m

Tactic:
by lia

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

Goal state before:
pp: case refine_1
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s

Tactic:
·

Goal state after:
case refine_1
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_2
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s

Tactic:
·

Goal state after:
case refine_2
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_3
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s

Tactic:
·

Goal state after:
case refine_3
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_4
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s

Tactic:
·

Goal state after:
case refine_4
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case mp
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i)) → s.obj i.castSucc = s.obj i.succ

pp: case mpr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s.obj i.castSucc = s.obj i.succ → s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))

Tactic:
·

Goal state after:
case mp
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i)) → s.obj i.castSucc = s.obj i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s.obj i.castSucc = s.obj i.succ → s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))

Tactic:
·

Goal state after:
case mpr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s.obj i.castSucc = s.obj i.succ → s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case pos
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
h₁ : i.castSucc < j
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j

pp: case neg
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
h₁ : ¬i.castSucc < j
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j

Tactic:
·

Goal state after:
case pos
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
h₁ : i.castSucc < j
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_5
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s

Tactic:
·

Goal state after:
case refine_5
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case neg
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
h₁ : ¬i.castSucc < j
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j

Tactic:
·

Goal state after:
case neg
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
h₁ : ¬i.castSucc < j
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case zero
X : Type u_1
inst✝ : PartialOrder X
s : nerve X _⦋0⦌
⊢ s ∈ (nerve X).nonDegenerate 0 ↔ StrictMono s.obj

pp: case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ s ∈ (nerve X).nonDegenerate (n + 1) ↔ StrictMono s.obj

Tactic:
·

Goal state after:
case zero
X : Type u_1
inst✝ : PartialOrder X
s : nerve X _⦋0⦌
⊢ s ∈ (nerve X).nonDegenerate 0 ↔ StrictMono s.obj
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_6
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s

Tactic:
·

Goal state after:
case refine_6
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ s ∈ (nerve X).nonDegenerate (n + 1) ↔ StrictMono s.obj

Tactic:
·

Goal state after:
case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ s ∈ (nerve X).nonDegenerate (n + 1) ↔ StrictMono s.obj
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case inl
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i < s.obj j
⊢ s.obj i < s.obj j

pp: case inr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i = s.obj j
⊢ s.obj i < s.obj j

Tactic:
·

Goal state after:
case inl
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i < s.obj j
⊢ s.obj i < s.obj j
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case inr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i = s.obj j
⊢ s.obj i < s.obj j

Tactic:
·

Goal state after:
case inr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i = s.obj j
⊢ s.obj i < s.obj j
Module: Mathlib.Order.Fin.SuccAboveOrderIso

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

pp: case right
n : ℕ
i : Fin (n + 2)
⊢ Function.Surjective fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩

Tactic:
·

Goal state after:
case left
n : ℕ
i : Fin (n + 2)
⊢ Function.Injective fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩
Module: Mathlib.Order.Fin.SuccAboveOrderIso

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

Tactic:
·

Goal state after:
case right
n : ℕ
i : Fin (n + 2)
⊢ Function.Surjective fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩
Module: Mathlib.Order.Fin.SuccAboveOrderIso

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

pp: case right.inr
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
hj✝ : j ∈ {i.succ}ᶜ
hj : ¬j = i.succ
⊢ ∃ a, (fun a ↦ ⟨i.succ.succAboveOrderEmb a, ⋯⟩) a = ⟨j, hj✝⟩

Tactic:
·

Goal state after:
case right.inl
n : ℕ
j : Fin (n + 2)
hj✝ : j ∈ {0}ᶜ
hj : ¬j = 0
⊢ ∃ a, (fun a ↦ ⟨(succAboveOrderEmb 0) a, ⋯⟩) a = ⟨j, hj✝⟩
Module: Mathlib.Order.Fin.SuccAboveOrderIso

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

Tactic:
·

Goal state after:
case right.inr
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
hj✝ : j ∈ {i.succ}ᶜ
hj : ¬j = i.succ
⊢ ∃ a, (fun a ↦ ⟨i.succ.succAboveOrderEmb a, ⋯⟩) a = ⟨j, hj✝⟩
Module: Mathlib.Order.Fin.Finset

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

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

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
b x : α
hab : x < b
x✝ : ↥{x, b}
hx : x ∈ {x, b}
⊢ ∃ a, ![⟨x, ⋯⟩, ⟨b, ⋯⟩] a = ⟨x, hx⟩
Module: Mathlib.Order.Fin.Finset

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

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a x : α
hab : a < x
x✝ : ↥{a, x}
hx : x ∈ {a, x}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨x, ⋯⟩] a_1 = ⟨x, hx⟩
Module: Mathlib.Order.Fin.Finset

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

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

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

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
b c : α
hbc : b < c
x : α
hab : x < b
x✝ : ↥{x, b, c}
hx : x ∈ {x, b, c}
⊢ ∃ a, ![⟨x, ⋯⟩, ⟨b, ⋯⟩, ⟨c, ⋯⟩] a = ⟨x, hx⟩
Module: Mathlib.Order.Fin.Finset

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

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

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a c x : α
hab : a < x
hbc : x < c
x✝ : ↥{a, x, c}
hx : x ∈ {a, x, c}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨x, ⋯⟩, ⟨c, ⋯⟩] a_1 = ⟨x, hx⟩
Module: Mathlib.Order.Fin.Finset

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

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
x : α
hbc : b < x
x✝ : ↥{a, b, x}
hx : x ∈ {a, b, x}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩, ⟨x, ⋯⟩] a_1 = ⟨x, hx⟩
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 lia

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

Goal state before:
pp: case e'_2
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₁₂)) := ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : ComposableArrows C 1 = (fun X ↦ X) (nerve C _⦋1⦌)
⊢ ComposableArrows.arrowEquiv.symm (Arrow.mk (f₀₁ ≫ f₁₂)) =
    (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h'.simplex

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₀₁ ≫ f₁₂)) := ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : ComposableArrows C 1 = (fun X ↦ X) (nerve C _⦋1⦌)
⊢ ComposableArrows.arrowEquiv.symm (Arrow.mk f₀₂) = (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h.simplex

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₀₂)
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h'.simplex =
    (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h.simplex

Tactic:
·

Goal state after:
case e'_2
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₁₂)) := ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : ComposableArrows C 1 = (fun X ↦ X) (nerve C _⦋1⦌)
⊢ ComposableArrows.arrowEquiv.symm (Arrow.mk (f₀₁ ≫ f₁₂)) =
    (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h'.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
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₀₁ ≫ f₁₂)) := ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : ComposableArrows C 1 = (fun X ↦ X) (nerve C _⦋1⦌)
⊢ ComposableArrows.arrowEquiv.symm (Arrow.mk f₀₂) = (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h.simplex

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₀₂)
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h'.simplex =
    (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h.simplex

Tactic:
·

Goal state after:
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₀₁ ≫ f₁₂)) := ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : ComposableArrows C 1 = (fun X ↦ X) (nerve C _⦋1⦌)
⊢ ComposableArrows.arrowEquiv.symm (Arrow.mk f₀₂) = (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h.simplex
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₀₂)
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h'.simplex =
    (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h.simplex

Tactic:
·

Goal state after:
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₀₂)
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h'.simplex =
    (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h.simplex
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
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
⊢ φ ≫ φ = 0

pp: case neg
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
⊢ φ ≫ ψ = 0

pp: case pos
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
⊢ ψ ≫ φ = 0

pp: case neg
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
⊢ ψ ≫ ψ = 0

Tactic:
·

Goal state after:
case pos
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
⊢ φ ≫ φ = 0
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case neg
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
⊢ φ ≫ ψ = 0

pp: case pos
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
⊢ ψ ≫ φ = 0

pp: case neg
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
⊢ ψ ≫ ψ = 0

Tactic:
·

Goal state after:
case neg
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
⊢ φ ≫ ψ = 0
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
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
⊢ ψ ≫ φ = 0

pp: case neg
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
⊢ ψ ≫ ψ = 0

Tactic:
·

Goal state after:
case pos
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
⊢ ψ ≫ φ = 0
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case neg
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
⊢ ψ ≫ ψ = 0

Tactic:
·

Goal state after:
case neg
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
⊢ ψ ≫ ψ = 0