mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

pp: case neg
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
·

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f) 0) ((ConcreteCategory.hom f') 0) hff' }

pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f) 0) ((ConcreteCategory.hom f') 0) hff' }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
·

Goal state after:
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f) 0) ((ConcreteCategory.hom f') 0) hff' }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mp
X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (A.toSSet.map f.op))) →
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))

pp: case mpr
X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) →
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (A.toSSet.map f.op))

Tactic:
·

Goal state after:
case mp
X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (A.toSSet.map f.op))) →
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) →
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (A.toSSet.map f.op))

Tactic:
·

Goal state after:
case mpr
X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) →
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (A.toSSet.map f.op))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f) 0) ((ConcreteCategory.hom f') 0) hff' }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
·

Goal state after:
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f) 0) ((ConcreteCategory.hom f') 0) hff' }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_2
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
⊢ { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex ≤ (N.mk ↑y ⋯).subcomplex

Tactic:
·

Goal state after:
case refine_2
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
⊢ { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex ≤ (N.mk ↑y ⋯).subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mp
X : SSet
A B : X.Subcomplex
⊢ A ≤ B → ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)

pp: case mpr
X : SSet
A B : X.Subcomplex
⊢ (∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)) → A ≤ B

Tactic:
·

Goal state after:
case mp
X : SSet
A B : X.Subcomplex
⊢ A ≤ B → ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f) 0) ((ConcreteCategory.hom f') 0) hff' }
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }

pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
·

Goal state after:
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f) 0) ((ConcreteCategory.hom f') 0) hff' }
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
A B : X.Subcomplex
⊢ (∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)) → A ≤ B

Tactic:
·

Goal state after:
case mpr
X : SSet
A B : X.Subcomplex
⊢ (∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)) → A ≤ B
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
·

Goal state after:
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
·

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mp
X : SSet
A : X.Subcomplex
n : ℕ
⊢ A.toSSet.degenerate n = ⊤ → X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)

pp: case mpr
X : SSet
A : X.Subcomplex
n : ℕ
⊢ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌) → A.toSSet.degenerate n = ⊤

Tactic:
·

Goal state after:
case mp
X : SSet
A : X.Subcomplex
n : ℕ
⊢ A.toSSet.degenerate n = ⊤ → X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }

pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
·

Goal state after:
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
A : X.Subcomplex
n : ℕ
⊢ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌) → A.toSSet.degenerate n = ⊤

Tactic:
·

Goal state after:
case mpr
X : SSet
A : X.Subcomplex
n : ℕ
⊢ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌) → A.toSSet.degenerate n = ⊤
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
·

Goal state after:
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }

pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
·

Goal state after:
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
·

Goal state after:
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

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 mp
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n → x ∈ X.degenerate n