mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ j < x

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
⊢ j < x
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))
⊢ Fin.cast ⋯ (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))

Tactic:
]

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))
⊢ Fin.cast ⋯ (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x
⊢ ∃! i,
    (ConcreteCategory.hom (SimplicialObject.δ Y i))
        ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y }.dim⦌)))
          { dim := d + 1, simplex := y }.simplex) =
      (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x }.dim⦌)))
        { dim := d, simplex := x }.simplex

Tactic:
]

Goal state after:
X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x
⊢ ∃! i,
    (ConcreteCategory.hom (SimplicialObject.δ Y i))
        ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y }.dim⦌)))
          { dim := d + 1, simplex := y }.simplex) =
      (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x }.dim⦌)))
        { dim := d, simplex := x }.simplex
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

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

Tactic:
]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.I
y : ↑P.II
hy : P.p y = ⟨x, h⟩
⊢ x = ↑⟨x, h⟩

Tactic:
]

Goal state after:
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
⊢ j < x.succ

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
⊢ j < x.succ
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
⊢ j < x.castSucc

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
⊢ j < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x.castSucc ≤ ({ toFun := i.predAbove, monotone' := ⋯ } x.castSucc).castSucc ∧
    ∀ i_1 < x.castSucc, ({ toFun := i.predAbove, monotone' := ⋯ } i_1).castSucc < x.castSucc

Tactic:
]

Goal state after:
case neg
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x.castSucc ≤ ({ toFun := i.predAbove, monotone' := ⋯ } x.castSucc).castSucc ∧
    ∀ i_1 < x.castSucc, ({ toFun := i.predAbove, monotone' := ⋯ } i_1).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i = Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)))) =
    Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)

Tactic:
]

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i = Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)))) =
    Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
⊢ IsEmpty { f // ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n) }

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
⊢ IsEmpty { f // ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n) }
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case neg
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : j ≤ i.castSucc
⊢ j < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
d : ℕ
hd : (↑x).dim = d
inst✝ : P.IsProper
⊢ ⋯.index hd = ⋯.index hd

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
d : ℕ
hd : (↑x).dim = d
inst✝ : P.IsProper
⊢ ⋯.index hd = ⋯.index hd
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: case e_y
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
d : ℕ
hd : (↑x).dim = d
inst✝ : P.IsProper
⊢ (↑⟨(N.orderIsoOfIso e hA).symm ↑(P.p x), ⋯⟩).toS =
    { dim := (↑(P.p x)).dim,
      simplex :=
        (CategoryTheory.ConcreteCategory.hom (e.symm.hom.app (Opposite.op { len := (↑(P.p x)).dim })))
          (↑(P.p x)).simplex }

Tactic:
]

Goal state after:
case e_y
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
d : ℕ
hd : (↑x).dim = d
inst✝ : P.IsProper
⊢ (↑⟨(N.orderIsoOfIso e hA).symm ↑(P.p x), ⋯⟩).toS =
    { dim := (↑(P.p x)).dim,
      simplex :=
        (CategoryTheory.ConcreteCategory.hom (e.symm.hom.app (Opposite.op { len := (↑(P.p x)).dim })))
          (↑(P.p x)).simplex }
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))
e₄ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))

Tactic:
]

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))
e₄ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ Function.Injective (ULift.down ∘ ((ConcreteCategory.hom ((isoNerve p q).hom.app (Opposite.op ⦋n⦌))) z).obj) ↔
    Function.Injective ⇑(objEquiv z)

Tactic:
]

Goal state after:
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ Function.Injective (ULift.down ∘ ((ConcreteCategory.hom ((isoNerve p q).hom.app (Opposite.op ⦋n⦌))) z).obj) ↔
    Function.Injective ⇑(objEquiv z)
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n ↔ Function.Injective ⇑(objEquiv z)

Tactic:
rw [← nonDegenerate_iff_of_mono (isoNerve p q).hom,
    PartialOrder.mem_nerve_nonDegenerate_iff_injective,
    ← Function.Injective.of_comp_iff ULift.down_injective]
  rfl

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

Goal state before:
pp: p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ StrictMono ((ConcreteCategory.hom ((isoNerve p q).hom.app (Opposite.op ⦋n⦌))) z).obj ↔ StrictMono ⇑(objEquiv z)

Tactic:
]

Goal state after:
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ StrictMono ((ConcreteCategory.hom ((isoNerve p q).hom.app (Opposite.op ⦋n⦌))) z).obj ↔ StrictMono ⇑(objEquiv z)
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
this : (objEquiv x) i ≤ (objEquiv x) j
h₁ : x.1 i ≤ x.1 j
⊢ ↑(x.1 i) + ↑(x.2 i) ≤ ↑(x.1 j) + ↑(x.2 j)

Tactic:
have h₂ : x.2 i ≤ x.2 j := this.2

Goal state after:
p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
this : (objEquiv x) i ≤ (objEquiv x) j
h₁ : x.1 i ≤ x.1 j
h₂ : x.2 i ≤ x.2 j
⊢ ↑(x.1 i) + ↑(x.2 i) ≤ ↑(x.1 j) + ↑(x.2 j)
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
h₁ : a.1 ≤ b.1
h₂ : a.2 ≤ b.2
⊢ a.1 < b.1 ∧ a.2 ≤ b.2 ∨ a.1 ≤ b.1 ∧ a.2 < b.2 ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2

Tactic:
]

Goal state after:
p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
h₁ : a.1 ≤ b.1
h₂ : a.2 ≤ b.2
⊢ a.1 < b.1 ∧ a.2 ≤ b.2 ∨ a.1 ≤ b.1 ∧ a.2 < b.2 ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hx : StrictMono ⇑(orderHomOfSimplex x ⋯)
⊢ False

Tactic:
]

Goal state after:
p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hx : StrictMono ⇑(orderHomOfSimplex x ⋯)
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n
this : Mono (yonedaEquiv.symm x ≫ f)
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n
this : Mono (yonedaEquiv.symm x ≫ f)
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)

Tactic:
]

Goal state after:
X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
⊢ orderHomOfSimplex z hn = OrderHom.id → Function.Injective ⇑(objEquiv z)

Tactic:
]

Goal state after:
case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
⊢ orderHomOfSimplex z hn = OrderHom.id → Function.Injective ⇑(objEquiv z)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i : Fin (n + 2)
this✝ : Mono (yonedaEquiv.symm x)
this :
  (ConcreteCategory.hom (SimplicialObject.δ X i)) x =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i))
⊢ Mono (SimplexCategory.δ i)

Tactic:
]

Goal state after:
X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i : Fin (n + 2)
this✝ : Mono (yonedaEquiv.symm x)
this :
  (ConcreteCategory.hom (SimplicialObject.δ X i)) x =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i))
⊢ Mono (SimplexCategory.δ i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
h : ∀ (x : Fin (n + 1)), ⟨↑(z.1 x) + ↑(z.2 x), ⋯⟩ = x
⊢ ↑⟨↑(z.1 a) + ↑(z.2 a), ⋯⟩ = ↑⟨↑(z.1 b) + ↑(z.2 b), ⋯⟩

Tactic:
]

Goal state after:
case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
h : ∀ (x : Fin (n + 1)), ⟨↑(z.1 x) + ↑(z.2 x), ⋯⟩ = x
⊢ ↑⟨↑(z.1 a) + ↑(z.2 a), ⋯⟩ = ↑⟨↑(z.1 b) + ↑(z.2 b), ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: case snd
p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
i : Fin (n + 1)
h₁ : orderHomOfSimplex ↑z₁ ⋯ = OrderHom.id
h₂ : orderHomOfSimplex ↑z₂ ⋯ = OrderHom.id
⊢ ((objEquiv ↑z₁) i).2 = ((objEquiv ↑z₂) i).2

Tactic:
]

Goal state after:
case snd
p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
i : Fin (n + 1)
h₁ : orderHomOfSimplex ↑z₁ ⋯ = OrderHom.id
h₂ : orderHomOfSimplex ↑z₂ ⋯ = OrderHom.id
⊢ ((objEquiv ↑z₁) i).2 = ((objEquiv ↑z₂) i).2
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
m : SimplexCategory
f g : m ⟶ ⦋n⦌
h : (ConcreteCategory.hom (X.map f.op)) x = (ConcreteCategory.hom (X.map g.op)) x
this : Mono (yonedaEquiv.symm x)
⊢ stdSimplex.map f ≫ yonedaEquiv.symm x = stdSimplex.map g ≫ yonedaEquiv.symm x

Tactic:
]

Goal state after:
X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
m : SimplexCategory
f g : m ⟶ ⦋n⦌
h : (ConcreteCategory.hom (X.map f.op)) x = (ConcreteCategory.hom (X.map g.op)) x
this : Mono (yonedaEquiv.symm x)
⊢ stdSimplex.map f ≫ yonedaEquiv.symm x = stdSimplex.map g ≫ yonedaEquiv.symm x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝¹ : PartialOrder α
inst✝ : WellFoundedLT α
f : P.RankFunction α
⊢ IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝¹ : PartialOrder α
inst✝ : WellFoundedLT α
f : P.RankFunction α
⊢ IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ((↑s).cast ⋯).simplex ∈ X.nonDegenerate (↑s).dim

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ((↑s).cast ⋯).simplex ∈ X.nonDegenerate (↑s).dim
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
⊢ IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
⊢ IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Mono (yonedaEquiv.symm x)

Tactic:
]

Goal state after:
X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Mono (yonedaEquiv.symm x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ((↑s).cast ⋯).simplex ∉ A.obj (Opposite.op ⦋(↑s).dim⦌)

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ((↑s).cast ⋯).simplex ∉ A.obj (Opposite.op ⦋(↑s).dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀)).dim = (↑(g m)).dim
n : ℕ
⊢ f.rank (g (n₀ + n + 1)) < f.rank (g (n₀ + n))

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀)).dim = (↑(g m)).dim
n : ℕ
⊢ f.rank (g (n₀ + n + 1)) < f.rank (g (n₀ + n))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
f₁ f₂ : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
x✝¹ : Mono f₁ ∧ (ConcreteCategory.hom (X.map f₁.op)) y.simplex = x.simplex
x✝ : Mono f₂ ∧ (ConcreteCategory.hom (X.map f₂.op)) y.simplex = x.simplex
left✝¹ : Mono f₁
hf₁ : (ConcreteCategory.hom (X.map f₁.op)) y.simplex = x.simplex
left✝ : Mono f₂
hf₂ : (ConcreteCategory.hom (X.map f₂.op)) y.simplex = x.simplex
⊢ x.simplex = x.simplex

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
x✝ :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim + 1, simplex := ((↑(P.p t)).cast ⋯).simplex }
⊢ ((↑(P.p s)).cast ⋯).toS = ((↑(P.p t)).cast ⋯).toS

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
x✝ :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim + 1, simplex := ((↑(P.p t)).cast ⋯).simplex }
⊢ ((↑(P.p s)).cast ⋯).toS = ((↑(P.p t)).cast ⋯).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h : { dim := (↑s).dim, simplex := ((↑s).cast ⋯).simplex } = { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ s = t

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h : { dim := (↑s).dim, simplex := ((↑s).cast ⋯).simplex } = { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ s = t
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
⊢ yonedaEquiv.symm x.simplex = yonedaEquiv.symm x.simplex

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h : { dim := (↑s).dim, simplex := ((↑s).cast ⋯).simplex } = { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ (↑s).toS = (↑t).toS

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h : { dim := (↑s).dim, simplex := ((↑s).cast ⋯).simplex } = { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ (↑s).toS = (↑t).toS