mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ b ∈ finset f x, y.castSucc ≤ b
i : Fin (n + 1)
hi : i < y
this : x ≤ (f i).castSucc
⊢ i.castSucc ∈ 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)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ b ∈ finset f x, y.castSucc ≤ b
i : Fin (n + 1)
hi : i < y
this : x ≤ (f i).castSucc
⊢ y ≤ i

Tactic:
by

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

Goal state before:
pp: x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i j : Fin (x₁.len + 1 + (x₂.len + 1))
h : i ≤ j
⊢ (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      i ≤
    (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      j

Tactic:
by

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

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ (tensorObjOf x y).len + z.len + 1 = x.len + (tensorObjOf y z).len + 1

Tactic:
by

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

Goal state before:
pp: x : AugmentedSimplexCategory
⊢ x ◁ 𝟙 WithInitial.star = 𝟙 (x ⊗ WithInitial.star)

Tactic:
by

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

Goal state before:
pp: x : AugmentedSimplexCategory
⊢ 𝟙 WithInitial.star ▷ x = 𝟙 (WithInitial.star ⊗ 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)
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
this : i < y
⊢ x ≤ (f i).castSucc

Tactic:
by

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

Goal state before:
pp: x y : SimplexCategory
i : Fin (x.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)

Tactic:
by

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

Goal state before:
pp: x y : SimplexCategory
i : Fin (y.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)

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 : Fin (m + 2)
y : Fin (n + 1)
⊢ map' f x = y.castSucc ↔ x ≤ (f y).castSucc ∧ ∀ i < y, (f i).castSucc < 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)
⊢ map' f (Fin.last (m + 1)) = Fin.last (n + 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)
⊢ map' f 0 = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : Fin (n + 2)
⊢ map' OrderHom.id x = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
⊢ l ∈ f.I ∪ g.I → i.as ≤ l

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
⊢ l ∈ f.I ∪ g.I → l ≤ k.as

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : J), t ∈ x.I ↔ t ∈ y.I
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f = f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
⊢ f ≫ 𝟙 Y✝ = f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
x✝³ : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((𝟙_ SSet).map x✝ ≫ ↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝¹).len + 1))).obj (𝟙 x✝³)) =
    (↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝²).len + 1))).obj (𝟙 x✝³)) ≫ (nerve (x✝³ ⟶ x✝³)).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((nerve (i ⟶ j) ⊗ nerve (j ⟶ k)).map x✝ ≫ ↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) =
    (↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) ≫ (nerve (i ⟶ k)).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
⊢ ∀ k ∈ ⇑f '' I.I, { as := f i.as }.as ≤ k

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
⊢ ∀ k ∈ ⇑f '' I.I, k ≤ { as := f j.as }.as

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
⊢ ∀ k ∈ ⇑f '' I.I, k ≤ { as := f j.as }.as

Tactic:
by rintro _ ⟨k, hk, rfl⟩; exact f.monotone (I.le_right k hk)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : (𝟙_ SSet).obj n✝
⊢ ∀ (X : Fin ((Opposite.unop n✝).len + 1)),
    ((ConcreteCategory.hom
                (({ app := fun x ↦ ↾fun x_1 ↦ (Functor.const (Fin ((Opposite.unop x).len + 1))).obj (𝟙 i),
                        naturality := ⋯ } ≫
                      nerveMap (functorMap f i i)).app
                  n✝)).toFun
            x✝).obj
        X =
      ((ConcreteCategory.hom
                (↾fun x ↦ (Functor.const (Fin ((Opposite.unop n✝).len + 1))).obj (𝟙 { as := f i.as }))).toFun
            x✝).obj
        X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i : SimplicialThickening J
⊢ eId SSet i ≫ nerveMap (functorMap f i i) = eId SSet { as := f i.as }

Tactic:
by

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

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : WithInitial.of x ⊗ WithInitial.of y ⟶ WithInitial.of z
h₁ : inl (WithInitial.of x) (WithInitial.of y) ≫ f = inl (WithInitial.of x) (WithInitial.of y) ≫ g
h₂ : inr (WithInitial.of x) (WithInitial.of y) ≫ f = inr (WithInitial.of x) (WithInitial.of y) ≫ g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: 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
⊢ y ≤ f z

Tactic:
by

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

Goal state before:
pp: x✝ y z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y ⟶ z✝
x z : SimplexCategory
f g : WithInitial.of x ⊗ WithInitial.star ⟶ WithInitial.of z
h₁ : inl (WithInitial.of x) WithInitial.star ≫ f = inl (WithInitial.of x) WithInitial.star ≫ g
h₂ : inr (WithInitial.of x) WithInitial.star ≫ f = inr (WithInitial.of x) WithInitial.star ≫ g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j k : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : ((i ⟶[SSet] j) ⊗ j ⟶[SSet] k).obj n✝
⊢ ∀ (X : Fin ((Opposite.unop n✝).len + 1)),
    ((ConcreteCategory.hom
                (({ app := fun x ↦ ↾fun x_1 ↦ Functor.prod' x_1.1 x_1.2 ⋙ i.compFunctor j k, naturality := ⋯ } ≫
                      nerveMap (functorMap f i k)).app
                  n✝)).toFun
            x✝).obj
        X =
      ((ConcreteCategory.hom
                (((nerveMap (functorMap f i j) ⊗ₘ nerveMap (functorMap f j k)) ≫
                      {
                        app := fun x ↦
                          ↾fun x_1 ↦
                            Functor.prod' x_1.1 x_1.2 ⋙ { as := f i.as }.compFunctor { as := f j.as } { as := f k.as },
                        naturality := ⋯ }).app
                  n✝)).toFun
            x✝).obj
        X

Tactic:
by

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

Goal state before:
pp: x y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x ⊗ y✝ ⟶ z✝
y z : SimplexCategory
f g : WithInitial.star ⊗ WithInitial.of y ⟶ WithInitial.of z
h₁ : inl WithInitial.star (WithInitial.of y) ≫ f = inl WithInitial.star (WithInitial.of y) ≫ g
h₂ : inr WithInitial.star (WithInitial.of y) ≫ f = inr WithInitial.star (WithInitial.of y) ≫ g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j k : SimplicialThickening J
⊢ eComp SSet i j k ≫ nerveMap (functorMap f i k) =
    (nerveMap (functorMap f i j) ⊗ₘ nerveMap (functorMap f j k)) ≫
      eComp SSet { as := f i.as } { as := f j.as } { as := f k.as }

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : (i ⟶[SSet] j).obj n✝
⊢ ∀ (X : Fin ((Opposite.unop n✝).len + 1)),
    ((ConcreteCategory.hom (((functor OrderHom.id).map i j ≫ eqToHom ⋯).app n✝)).toFun x✝).obj X =
      ((ConcreteCategory.hom (((EnrichedFunctor.id SSet (SimplicialThickening J)).map i j).app n✝)).toFun x✝).obj X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
⊢ functor OrderHom.id = EnrichedFunctor.id SSet (SimplicialThickening J)

Tactic:
by

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

Goal state before:
pp: 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 : Fin (n + 1)
hi : i < z
⊢ f i < y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : (i ⟶[SSet] j).obj n✝
⊢ ∀ (X : Fin ((Opposite.unop n✝).len + 1)),
    ((ConcreteCategory.hom (((functor (g.comp f)).map i j ≫ eqToHom ⋯).app n✝)).toFun x✝).obj X =
      ((ConcreteCategory.hom (((EnrichedFunctor.comp SSet (functor f) (functor g)).map i j).app n✝)).toFun x✝).obj X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
⊢ functor (g.comp f) = EnrichedFunctor.comp SSet (functor f) (functor g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : SimplicialCategory C
i : SimplexCategoryᵒᵖ
⊢ ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (𝟙 i).unop).uliftMap) =
    𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C)

Tactic:
by

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

Goal state before:
pp: 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 : ∀ (i : Fin (n + 1)), (f i).castSucc < y.castSucc
i : Fin (n + 1)
⊢ f i < y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : SimplicialCategory C
X✝ Y✝ Z✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (f ≫ g).unop).uliftMap) =
    ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
      ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)

Tactic:
by

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

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inl (WithInitial.of x₁) (WithInitial.of x₂) ≫ (f₁ ⊗ₘ f₂) = f₁ ≫ inl (WithInitial.of y₁) (WithInitial.of y₂)

Tactic:
by

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

Goal state before:
pp: x₁ y₁ x₂ y₂ : AugmentedSimplexCategory
f₁✝ : x₁ ⟶ y₁
f₂✝ : x₂ ⟶ y₂
x✝² x✝¹ x✝ : AugmentedSimplexCategory
f₁ : x✝² ⟶ x✝¹
f₂ : WithInitial.star ⟶ x✝
⊢ x✝².inl WithInitial.star ≫ (f₁ ⊗ₘ f₂) = f₁ ≫ x✝¹.inl x✝

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
x y : A.N
⊢ x = y ↔ x.toN = y.toN

Tactic:
by

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

Goal state before:
pp: 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
⊢ s.simplex ∉ A.obj (Opposite.op ⦋s.dim⦌)

Tactic:
by

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

Goal state before:
pp: 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
⊢ motive s

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
x y : A.N
⊢ x = y ↔ { dim := x.dim, simplex := x.simplex } = { dim := y.dim, simplex := y.simplex }

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
x✝¹ x✝ : A.N
⊢ x✝¹.toN = x✝.toN → x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
s : A.N
d : ℕ
hd : s.dim = d
⊢ s.cast hd = s

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
x : A.N
⊢ ((SSet.N.orderIsoOfIso e) x.toN).simplex ∉ B.obj (Opposite.op ⦋((SSet.N.orderIsoOfIso e) x.toN).dim⦌)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
y : B.N
⊢ A.preimage e.inv = B

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
y : B.N
⊢ ((SSet.N.orderIsoOfIso e).symm y.toN).simplex ∉ A.obj (Opposite.op ⦋((SSet.N.orderIsoOfIso e).symm y.toN).dim⦌)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
x✝ : A.N
⊢ (fun y ↦ { toN := (SSet.N.orderIsoOfIso e).symm y.toN, notMem := ⋯ })
      ((fun x ↦ { toN := (SSet.N.orderIsoOfIso e) x.toN, notMem := ⋯ }) x✝) =
    x✝

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
x✝ : B.N
⊢ (fun x ↦ { toN := (SSet.N.orderIsoOfIso e) x.toN, notMem := ⋯ })
      ((fun y ↦ { toN := (SSet.N.orderIsoOfIso e).symm y.toN, notMem := ⋯ }) x✝) =
    x✝

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
⊢ ∃ x f, Epi f ∧ (ConcreteCategory.hom (X.map f.op)) x.simplex = s

Tactic:
by

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

Goal state before:
pp: 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

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
d : ℕ
hd : x.dim = d
⊢ y.dim = d + 1

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
d : ℕ
hd : x.dim = d
⊢ (x.cast hd).IsUniquelyCodimOneFace (y.cast ⋯)

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
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
⊢ y.dim = d + 1

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
d : ℕ
hd : x.dim = d
⊢ ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) (y.cast ⋯).simplex = (x.cast hd).simplex

Tactic:
by

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

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

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
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
⊢ i = hxy.index hd → (ConcreteCategory.hom (SimplicialObject.δ X i)) (y.cast ⋯).simplex = (x.cast hd).simplex

Tactic:
by

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

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inr (WithInitial.of x₁) (WithInitial.of x₂) ≫ (f₁ ⊗ₘ f₂) = f₂ ≫ inr (WithInitial.of y₁) (WithInitial.of y₂)

Tactic:
by

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

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

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
⊢ x ≤ y

Tactic:
by

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

Goal state before:
pp: x₁ y₁ x₂ y₂ : AugmentedSimplexCategory
f₁✝ : x₁ ⟶ y₁
f₂✝ : x₂ ⟶ y₂
x✝² x✝¹ x✝ : AugmentedSimplexCategory
f₁ : WithInitial.star ⟶ x✝²
f₂ : x✝¹ ⟶ x✝
⊢ inr WithInitial.star x✝¹ ≫ (f₁ ⊗ₘ f₂) = f₂ ≫ x✝².inr 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
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
⊢ y.dim = d + 1

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
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) (y.cast ⋯).simplex = (x.cast hd).simplex
⊢ Mono f

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
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) (y.cast ⋯).simplex = (x.cast hd).simplex
⊢ Mono (SimplexCategory.δ (hxy.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 (z.len + 1)
e₁ :
  (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (tensorObjOf x y).len.succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
⊢ y.len + 1 + (z.len + 1) = (tensorObjOf y z).len + 1

Tactic:
by

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

Goal state before:
pp: X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ (fun i ↦ (ConcreteCategory.hom (SimplicialObject.δ X.op i)) (opObjEquiv.symm y) = opObjEquiv.symm x) (hxy.index ⋯).rev

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
⊢ (opEquiv.symm x).IsUniquelyCodimOneFace (opEquiv.symm y)

Tactic:
by

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

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

Tactic:
by

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

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

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
⊢ { 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 }

Tactic:
by

Goal state after: