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

Goal state before:
pp: case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
i : Fin (n + 1)
⊢ (X.spine n ((ConcreteCategory.hom m) x)).vertex i =
    Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      i

pp: case hₐ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
i : Fin n
⊢ (X.spine n ((ConcreteCategory.hom m) x)).arrow i =
    Path.arrow
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      i

Tactic:
·

Goal state after:
case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
i : Fin (n + 1)
⊢ (X.spine n ((ConcreteCategory.hom m) x)).vertex i =
    Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case hₐ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
i : Fin n
⊢ (X.spine n ((ConcreteCategory.hom m) x)).arrow i =
    Path.arrow
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      i

Tactic:
·

Goal state after:
case hₐ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
i : Fin n
⊢ (X.spine n ((ConcreteCategory.hom m) x)).arrow i =
    Path.arrow
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      i
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ b ∈ finset f x, b = Fin.last (n + 1)) → ∀ (i : Fin (n + 1)), (f i).castSucc < x

pp: case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ (i : Fin (n + 1)), (f i).castSucc < x) → ∀ b ∈ finset f x, b = Fin.last (n + 1)

Tactic:
·

Goal state after:
case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ b ∈ finset f x, b = Fin.last (n + 1)) → ∀ (i : Fin (n + 1)), (f i).castSucc < x
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ (i : Fin (n + 1)), (f i).castSucc < x) → ∀ b ∈ finset f x, b = Fin.last (n + 1)

Tactic:
·

Goal state after:
case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ (i : Fin (n + 1)), (f i).castSucc < x) → ∀ b ∈ finset f x, b = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
⊢ (∀ b ∈ finset f x, y.castSucc ≤ b) → ∀ i < y, (f i).castSucc < x

pp: case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
⊢ (∀ i < y, (f i).castSucc < x) → ∀ b ∈ finset f x, y.castSucc ≤ b

Tactic:
·

Goal state after:
case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
⊢ (∀ b ∈ finset f x, y.castSucc ≤ b) → ∀ i < y, (f i).castSucc < x
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
⊢ (∀ i < y, (f i).castSucc < x) → ∀ b ∈ finset f x, y.castSucc ≤ b

Tactic:
·

Goal state after:
case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
⊢ (∀ i < y, (f i).castSucc < x) → ∀ b ∈ finset f x, y.castSucc ≤ b
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mpr.inl
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
i : Fin (n + 1)
hi : i.castSucc ∈ finset f x
⊢ y.castSucc ≤ i.castSucc

pp: case mpr.inr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
hi : Fin.last (n + 1) ∈ finset f x
⊢ y.castSucc ≤ Fin.last (n + 1)

Tactic:
·

Goal state after:
case mpr.inl
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
i : Fin (n + 1)
hi : i.castSucc ∈ finset f x
⊢ y.castSucc ≤ i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mpr.inr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
hi : Fin.last (n + 1) ∈ finset f x
⊢ y.castSucc ≤ Fin.last (n + 1)

Tactic:
·

Goal state after:
case mpr.inr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
hi : Fin.last (n + 1) ∈ finset f x
⊢ y.castSucc ≤ Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl
n : ℕ
x : Fin (n + 1)
⊢ map' OrderHom.id x.castSucc = x.castSucc

pp: case inr
n : ℕ
⊢ map' OrderHom.id (Fin.last (n + 1)) = Fin.last (n + 1)

Tactic:
·

Goal state after:
case inl
n : ℕ
x : Fin (n + 1)
⊢ map' OrderHom.id x.castSucc = x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inr
n : ℕ
⊢ map' OrderHom.id (Fin.last (n + 1)) = Fin.last (n + 1)

Tactic:
·

Goal state after:
case inr
n : ℕ
⊢ map' OrderHom.id (Fin.last (n + 1)) = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

pp: case inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
⊢ map' f (map' g (Fin.last (p + 1))) = map' (g.comp f) (Fin.last (p + 1))

Tactic:
·

Goal state after:
case inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : map' g x.castSucc = y.castSucc
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

pp: case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

Tactic:
·

Goal state after:
case inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : map' g x.castSucc = y.castSucc
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : map' f y.castSucc = z.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

pp: case inl.inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
·

Goal state after:
case inl.inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : map' f y.castSucc = z.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inl.left
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
⊢ x.castSucc ≤ ((g.comp f) z).castSucc

pp: case inl.inl.inl.right
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
⊢ ∀ i < z, ((g.comp f) i).castSucc < x.castSucc

Tactic:
·

Goal state after:
case inl.inl.inl.left
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
⊢ x.castSucc ≤ ((g.comp f) z).castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inl.right
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
⊢ ∀ i < z, ((g.comp f) i).castSucc < x.castSucc

Tactic:
·

Goal state after:
case inl.inl.inl.right
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
⊢ ∀ i < z, ((g.comp f) i).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
·

Goal state after:
case inl.inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

Tactic:
·

Goal state after:
case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: case pos
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : s.subcomplex ≤ A
⊢ motive s

pp: case neg
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : ¬s.subcomplex ≤ A
⊢ motive s

Tactic:
·

Goal state after:
case pos
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : s.subcomplex ≤ A
⊢ motive s
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: case neg
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : ¬s.subcomplex ≤ A
⊢ motive s

Tactic:
·

Goal state after:
case neg
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : ¬s.subcomplex ≤ A
⊢ motive s
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
⊢ map' f (map' g (Fin.last (p + 1))) = map' (g.comp f) (Fin.last (p + 1))

Tactic:
·

Goal state after:
case inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
⊢ map' f (map' g (Fin.last (p + 1))) = map' (g.comp f) (Fin.last (p + 1))
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl
n : ℕ
i x : Fin (n + 2)
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

pp: case inr
n : ℕ
i : Fin (n + 2)
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 2)) = i.predAbove (Fin.last (n + 2))

Tactic:
·

Goal state after:
case inl
n : ℕ
i x : Fin (n + 2)
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

pp: case neg
n : ℕ
i x : Fin (n + 2)
hx : i < x
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

Tactic:
·

Goal state after:
case pos
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc.castSucc = x.castSucc

pp: case pos.inr
n : ℕ
i : Fin (n + 2)
hx : Fin.last (n + 1) ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 1)).castSucc = Fin.last (n + 1)

Tactic:
·

Goal state after:
case pos.inl
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc.castSucc = x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl.left
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ x.castSucc ≤ i.succAbove x

pp: case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ ∀ i_1 < x, i.succAbove i_1 < x.castSucc

Tactic:
·

Goal state after:
case pos.inl.left
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ x.castSucc ≤ i.succAbove x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: case mp
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
⊢ { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y } →
    ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x

pp: case mpr
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
⊢ (∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x) →
    { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }

Tactic:
·

Goal state after:
case mp
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
⊢ { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y } →
    ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: case mpr
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
⊢ (∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x) →
    { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }

Tactic:
·

Goal state after:
case mpr
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
⊢ (∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x) →
    { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ (x.cast hd).IsUniquelyCodimOneFace (y.cast ⋯)

Tactic:
by
  simpa only [cast_eq_self]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl.left.inl
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx✝ : x.castSucc ≤ i
hx : x.castSucc < i
⊢ x.castSucc ≤ i.succAbove x

pp: case pos.inl.left.inr
n : ℕ
x : Fin (n + 1)
hx : x.castSucc ≤ x.castSucc
⊢ x.castSucc ≤ x.castSucc.succAbove x

Tactic:
·

Goal state after:
case pos.inl.left.inl
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx✝ : x.castSucc ≤ i
hx : x.castSucc < i
⊢ x.castSucc ≤ i.succAbove x
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl.left.inr
n : ℕ
x : Fin (n + 1)
hx : x.castSucc ≤ x.castSucc
⊢ x.castSucc ≤ x.castSucc.succAbove x

Tactic:
·

Goal state after:
case pos.inl.left.inr
n : ℕ
x : Fin (n + 1)
hx : x.castSucc ≤ x.castSucc
⊢ x.castSucc ≤ x.castSucc.succAbove x
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ ∀ i_1 < x, i.succAbove i_1 < x.castSucc

Tactic:
·

Goal state after:
case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ ∀ i_1 < x, i.succAbove i_1 < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inr
n : ℕ
i : Fin (n + 2)
hx : Fin.last (n + 1) ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 1)).castSucc = Fin.last (n + 1)

Tactic:
·

Goal state after:
case pos.inr
n : ℕ
i : Fin (n + 2)
hx : Fin.last (n + 1) ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 1)).castSucc = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i x : Fin (n + 2)
hx : i < x
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

Tactic:
·

Goal state after:
case neg
n : ℕ
i x : Fin (n + 2)
hx : i < x
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : j.castSucc < i
⊢ i.succAbove j < x.succ

pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : i ≤ j.castSucc
⊢ i.succAbove j < x.succ

Tactic:
·

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : j.castSucc < i
⊢ i.succAbove j < x.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : i ≤ j.castSucc
⊢ i.succAbove j < x.succ

Tactic:
·

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : i ≤ j.castSucc
⊢ i.succAbove j < x.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 2)
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 2)) = i.predAbove (Fin.last (n + 2))

Tactic:
·

Goal state after:
case inr
n : ℕ
i : Fin (n + 2)
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 2)) = i.predAbove (Fin.last (n + 2))
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl
n : ℕ
i x : Fin (n + 1)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc

pp: case inr
n : ℕ
i : Fin (n + 1)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } (Fin.last (n + 1)) = i.succ.castSucc.succAbove (Fin.last (n + 1))

Tactic:
·

Goal state after:
case inl
n : ℕ
i x : Fin (n + 1)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc

pp: case neg
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc

Tactic:
·

Goal state after:
case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.left
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ x ≤ i.predAbove x.succ

pp: case pos.right
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ ∀ i_1 < x.succ, i.predAbove i_1 < x

Tactic:
·

Goal state after:
case pos.left
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ x ≤ i.predAbove x.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.right
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ ∀ i_1 < x.succ, i.predAbove i_1 < x

Tactic:
·

Goal state after:
case pos.right
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ ∀ i_1 < x.succ, i.predAbove i_1 < x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.I
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)

pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.II
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)

Tactic:
·

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.I
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.II
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)

Tactic:
·

Goal state after:
case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.II
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : i.castSucc < j
⊢ i.predAbove j < x

pp: case neg
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : j ≤ i.castSucc
⊢ i.predAbove j < x

Tactic:
·

Goal state after:
case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : i.castSucc < j
⊢ i.predAbove j < x
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : j ≤ i.castSucc
⊢ i.predAbove j < x

Tactic:
·

Goal state after:
case neg
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : j ≤ i.castSucc
⊢ i.predAbove j < x