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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.S
hxy' :
  { dim := x.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex }.IsUniquelyCodimOneFace
    { dim := y.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex }
⊢ x.IsUniquelyCodimOneFace y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ (WithInitial.of x ⊗ WithInitial.of y).inr (WithInitial.of z) ≫
      (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom =
    inr (WithInitial.of y) (WithInitial.of z) ≫ inr (WithInitial.of x) (WithInitial.of y ⊗ WithInitial.of z)

Tactic:
by

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

Goal state before:
pp: n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ i.castSucc < x.succ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ (WithInitial.star ⊗ x✝¹).inr x✝ ≫ (α_ WithInitial.star x✝¹ x✝).hom = x✝¹.inr x✝ ≫ inr WithInitial.star (x✝¹ ⊗ x✝)

Tactic:
by

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
Y : SSet
e : X ≅ Y
d : ℕ
hd : x.dim = d
⊢ ⋯.index hd = hxy.index hd

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ (x✝¹ ⊗ WithInitial.star).inr x✝ ≫ (α_ x✝¹ WithInitial.star x✝).hom =
    inr WithInitial.star x✝ ≫ x✝¹.inr (WithInitial.star ⊗ x✝)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ (x✝¹ ⊗ x✝).inr WithInitial.star ≫ (α_ x✝¹ x✝ WithInitial.star).hom =
    x✝.inr WithInitial.star ≫ x✝¹.inr (x✝ ⊗ WithInitial.star)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
x y : ↑P.II
hxy : P.AncestralRel x y
⊢ (↑x).dim ≤ (↑y).dim

Tactic:
by

Goal state after:
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 = ↑(P.p y)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x : ↑P.I
y : ↑P.II
⊢ ↑x ≠ ↑y

Tactic:
by

Goal state after:
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
⊢ ⇑(N.orderIsoOfIso e hA) ⁻¹' P.I ∩ ⇑(N.orderIsoOfIso e hA) ⁻¹' P.II = ∅

Tactic:
by

Goal state after:
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
⊢ ⇑(N.orderIsoOfIso e hA) ⁻¹' P.I ∪ ⇑(N.orderIsoOfIso e hA) ⁻¹' P.II = Set.univ

Tactic:
by

Goal state after:
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
⊢ ∀ (a : B.N), a ∈ ⇑(N.orderIsoOfIso e hA) ⁻¹' P.II ↔ (N.orderIsoOfIso e hA).toEquiv a ∈ P.II

Tactic:
by

Goal state after:
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
⊢ ∀ (a : A.N), a ∈ P.I ↔ (N.orderIsoOfIso e hA).symm.toEquiv a ∈ ⇑(N.orderIsoOfIso e hA) ⁻¹' P.I

Tactic:
by

Goal state after:
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 ((tensorObjOf y z).len + 1) i)
⊢ x.len + 1 + (y.len + 1) = (tensorObjOf x y).len + 1

Tactic:
by

Goal state after:
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
⊢ (N.orderIsoOfIso e hA).symm ↑x ∈ (P.ofIso e hA).II

Tactic:
by

Goal state after:
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
⊢ (N.orderIsoOfIso e hA).symm ↑(P.p x) ∈ (P.ofIso e hA).I

Tactic:
by

Goal state after:
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
⊢ (P.ofIso e hA).p ⟨(N.orderIsoOfIso e hA).symm ↑x, ⋯⟩ = ⟨(N.orderIsoOfIso e hA).symm ↑(P.p x), ⋯⟩

Tactic:
by

Goal state after:
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 y : ↑P.II
⊢ (N.orderIsoOfIso e hA).symm ↑x ∈ (P.ofIso e hA).II

Tactic:
by

Goal state after:
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 y : ↑P.II
⊢ (N.orderIsoOfIso e hA).symm ↑y ∈ (P.ofIso e hA).II

Tactic:
by

Goal state after:
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 y : ↑P.II
⊢ ⟨(N.orderIsoOfIso e hA).symm ↑x, ⋯⟩ = ⟨(N.orderIsoOfIso e hA).symm ↑y, ⋯⟩ ↔ x = y

Tactic:
by

Goal state after:
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 y : ↑P.II
⊢ ↑⟨(N.orderIsoOfIso e hA).symm ↑x, ⋯⟩ < ↑((P.ofIso e hA).p ⟨(N.orderIsoOfIso e hA).symm ↑y, ⋯⟩) ↔ ↑x < ↑(P.p y)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x.castSucc ≤ i.castSucc

Tactic:
by

Goal state after:
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.IsProper
⊢ ∀ (x : ↑(P.ofIso e hA).II), (↑x).IsUniquelyCodimOneFace (↑((P.ofIso e hA).p x)).toS

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ inl (WithInitial.of x) (WithInitial.of y) ≫
      (WithInitial.of x ⊗ WithInitial.of y).inl (WithInitial.of z) ≫
        (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom =
    inl (WithInitial.of x) (WithInitial.of y ⊗ WithInitial.of z)

Tactic:
by

Goal state after:
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
⊢ WellFounded (P.ofIso e hA).AncestralRel

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ inl WithInitial.star x✝¹ ≫ (WithInitial.star ⊗ x✝¹).inl x✝ ≫ (α_ WithInitial.star x✝¹ x✝).hom =
    inl WithInitial.star (x✝¹ ⊗ x✝)

Tactic:
by

Goal state after:
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
⊢ (N.orderIsoOfIso e hA).symm ↑x ∈ (P.ofIso e hA).II

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ x✝¹.inl WithInitial.star ≫ (x✝¹ ⊗ WithInitial.star).inl x✝ ≫ (α_ x✝¹ WithInitial.star x✝).hom =
    x✝¹.inl (WithInitial.star ⊗ x✝)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ x✝¹.inl x✝ ≫ (x✝¹ ⊗ x✝).inl WithInitial.star ≫ (α_ x✝¹ x✝ WithInitial.star).hom = x✝¹.inl (x✝ ⊗ WithInitial.star)

Tactic:
by

Goal state after:
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)
⊢ x.len + 1 + (y.len + 1) = (tensorObjOf x y).len + 1

Tactic:
by

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 2)
hz : z ∈ finset f y
⊢ z ∈ finset f x

Tactic:
by

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
⊢ Monotone (map' f)

Tactic:
by

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

Goal state before:
pp: n : SimplexCategory
⊢ Quiver.Hom.unop (op (Hom.mk { toFun := II.map' (Hom.toOrderHom (𝟙 n)), monotone' := ⋯ })) = (𝟙 (op ⦋n.len + 1⦌)).unop

Tactic:
by

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

Goal state after:
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)))
⊢ y.len + 1 + (z.len + 1) = (tensorObjOf y z).len + 1

Tactic:
by

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

Goal state before:
pp: m n p : SimplexCategory
f : m ⟶ n
g : n ⟶ p
⊢ Quiver.Hom.unop (op (Hom.mk { toFun := II.map' (Hom.toOrderHom (f ≫ g)), monotone' := ⋯ })) =
    (op (Hom.mk { toFun := II.map' (Hom.toOrderHom f), monotone' := ⋯ }) ≫
        op (Hom.mk { toFun := II.map' (Hom.toOrderHom g), monotone' := ⋯ })).unop

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ (II.δ i).unop = (σ i).op.unop

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (II.σ i).unop = (δ i.succ.castSucc).op.unop

Tactic:
by

Goal state after:
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.IsProper
inst✝ : P.IsInner
⊢ ∀ (x : ↑(P.ofIso e hA).II) {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ 0

Tactic:
by

Goal state after:
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.IsProper
inst✝ : P.IsInner
⊢ ∀ (x : ↑(P.ofIso e hA).II) {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ Fin.last (d + 1)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ inr (WithInitial.of x) (WithInitial.of y) ≫
      (WithInitial.of x ⊗ WithInitial.of y).inl (WithInitial.of z) ≫
        (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom =
    inl (WithInitial.of y) (WithInitial.of z) ≫ inr (WithInitial.of x) (WithInitial.of y ⊗ WithInitial.of z)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ inr WithInitial.star x✝¹ ≫ (WithInitial.star ⊗ x✝¹).inl x✝ ≫ (α_ WithInitial.star x✝¹ x✝).hom =
    x✝¹.inl x✝ ≫ inr WithInitial.star (x✝¹ ⊗ x✝)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ x✝¹.inr WithInitial.star ≫ (x✝¹ ⊗ WithInitial.star).inl x✝ ≫ (α_ x✝¹ WithInitial.star x✝).hom =
    inl WithInitial.star x✝ ≫ x✝¹.inr (WithInitial.star ⊗ x✝)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ x✝¹.inr x✝ ≫ (x✝¹ ⊗ x✝).inl WithInitial.star ≫ (α_ x✝¹ x✝ WithInitial.star).hom =
    x✝.inl WithInitial.star ≫ x✝¹.inr (x✝ ⊗ WithInitial.star)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁ y₁ z₁ x₂ y₂ z₂ : AugmentedSimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
g₁ : y₁ ⟶ z₁
g₂ : y₂ ⟶ z₂
⊢ (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : AugmentedSimplexCategory
⊢ 𝟙 x ⊗ₘ 𝟙 y = 𝟙 (x ⊗ y)

Tactic:
by

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

Goal state before:
pp: p q n : ℕ
x✝ : (Δ[p] ⊗ Δ[q]) _⦋n⦌
x : Δ[p] _⦋n⦌
y : Δ[q] _⦋n⦌
⊢ (fun f ↦
        (stdSimplex.objEquiv.symm (SimplexCategory.Hom.mk (OrderHom.fst.comp f)),
          stdSimplex.objEquiv.symm (SimplexCategory.Hom.mk (OrderHom.snd.comp f))))
      ((fun x ↦
          match x with
          | (x, y) =>
            (SimplexCategory.Hom.toOrderHom (stdSimplex.objEquiv x)).prod
              (SimplexCategory.Hom.toOrderHom (stdSimplex.objEquiv y)))
        (x, y)) =
    (x, y)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: w x y z : AugmentedSimplexCategory
⊢ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) = (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ (fun i ↦ ⟨↑(x.1 i) + ↑(x.2 i), ⋯⟩) i ≤ (fun i ↦ ⟨↑(x.1 i) + ↑(x.2 i), ⋯⟩) j

Tactic:
by

Goal state after:
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)
hab : a ≤ b
⊢ a < b ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2

Tactic:
by

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

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
⊢ StrictMono ⇑(orderHomOfSimplex x hm) ↔ StrictMono ⇑(objEquiv x)

Tactic:
by

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

Goal state before:
pp: p q n : ℕ
x : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
m : ℕ
hm : p + q = m
⊢ StrictMono ⇑(orderHomOfSimplex (↑x) hm)

Tactic:
by

Goal state after:
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
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx⟩)

Tactic:
← nonDegenerate_iff_of_mono f

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.Nonsingular

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
⊢ ∀ {n : ℕ} (x : ↑(X.nonDegenerate n)), Mono (yonedaEquiv.symm ↑x)

Tactic:
by

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

Goal state before:
pp: p q n : ℕ
hn : p + q + 1 ≤ n
⊢ (Δ[p] ⊗ Δ[q]).degenerate n = ⊤

Tactic:
by

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

Goal state before:
pp: p q n : ℕ
x : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
m : ℕ
hm : p + q = m
i : Fin (n + 1)
⊢ ↑i ≤ ↑((orderHomOfSimplex (↑x) hm) i)

Tactic:
by

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

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
⊢ ∀ {n : ℕ} (x : ↑((nerve T).nonDegenerate n)), Mono (yonedaEquiv.symm ↑x)

Tactic:
by

Goal state after:
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)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X i)) x ∈ X.nonDegenerate n

Tactic:
by

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

Goal state before:
pp: p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
⊢ z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n ↔ orderHomOfSimplex z hn = OrderHom.id

Tactic:
by

Goal state after:
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 j : Fin (n + 2)
hij : (ConcreteCategory.hom (SimplicialObject.δ X i)) x = (ConcreteCategory.hom (SimplicialObject.δ X j)) x
⊢ i = j

Tactic:
by

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

Goal state before:
pp: p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
⊢ z₁ = z₂

Tactic:
by

Goal state after:
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 α
⊢ WellFounded P.AncestralRel

Tactic:
by

Goal state after:
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
⊢ f = g

Tactic:
by

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 : ↑P.II
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).simplex ∈ X.nonDegenerate (↑s).dim

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ IsIso (Subcomplex.toOfSimplex x)

Tactic:
by

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 : ↑P.II
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).simplex ∉ A.obj (Opposite.op ⦋(↑s).dim⦌)

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
⊢ ∃ x_1, Mono x_1 ∧ (ConcreteCategory.hom (X.map x_1.op)) y.simplex = x.simplex

Tactic:
by

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 }
⊢ s = t

Tactic:
by

Goal state after:
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
⊢ (ConcreteCategory.hom (X.map f₁.op)) y.simplex = (ConcreteCategory.hom (X.map f₂.op)) y.simplex

Tactic:
by

Goal state after:
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 : ℕ
⊢ n₀ ≤ n₀ + n + 1

Tactic:
by

Goal state after:
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
⊢ f₁ = f₂

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
⊢ stdSimplex.map (monoOfLE h) ≫ yonedaEquiv.symm y.simplex = yonedaEquiv.symm x.simplex

Tactic:
by

Goal state after: