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

Goal state before:
pp: case left
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : ⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ f)) = ⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ g))
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (x.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j)))

Tactic:
simpa using

Goal state after:
case left
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : ⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ f)) = ⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ g))
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (x.len + 1)
⊢ ↑((SimplexCategory.Hom.toOrderHom f) ((SimplexCategory.Hom.toOrderHom (inl' x y)) j)) =
    ↑((SimplexCategory.Hom.toOrderHom g) ((SimplexCategory.Hom.toOrderHom (inl' x y)) j))
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
t✝ : J
⊢ t✝ ∈ (𝟙 X✝ ≫ f).I ↔ t✝ ∈ f.I

Tactic:
simpa using

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
t✝ : J
⊢ t✝ = X✝.as → t✝ ∈ f.I
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
t✝ : J
⊢ t✝ ∈ (f ≫ 𝟙 Y✝).I ↔ t✝ ∈ f.I

Tactic:
simpa using

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
t✝ : J
⊢ t✝ = Y✝.as → t✝ ∈ f.I
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case right
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : ⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ f)) = ⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ g))
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (y.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j)))

Tactic:
simpa using

Goal state after:
case right
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : ⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ f)) = ⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ g))
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (y.len + 1)
⊢ ↑((SimplexCategory.Hom.toOrderHom f) ((SimplexCategory.Hom.toOrderHom (inr' x y)) j)) =
    ↑((SimplexCategory.Hom.toOrderHom g) ((SimplexCategory.Hom.toOrderHom (inr' x y)) j))
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:
simpa using

Goal state after:
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
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₂ : inr (WithInitial.of x) WithInitial.star ≫ f = inr (WithInitial.of x) WithInitial.star ≫ g
h₁ : 𝟙 (WithInitial.of x ⊗ WithInitial.star) ≫ f = 𝟙 (WithInitial.of x ⊗ WithInitial.star) ≫ g
⊢ f = g

Tactic:
simpa using

Goal state after:
x✝ y z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y ⟶ z✝
x z : SimplexCategory
f g : WithInitial.of x ⊗ WithInitial.star ⟶ WithInitial.of z
h₂ : inr (WithInitial.of x) WithInitial.star ≫ f = inr (WithInitial.of x) WithInitial.star ≫ g
h₁ : 𝟙 (WithInitial.of x ⊗ WithInitial.star) ≫ f = 𝟙 (WithInitial.of x ⊗ WithInitial.star) ≫ g
⊢ f = g
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₂ : 𝟙 (WithInitial.star ⊗ WithInitial.of y) ≫ f = 𝟙 (WithInitial.star ⊗ WithInitial.of y) ≫ g
⊢ f = g

Tactic:
simpa using

Goal state after:
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₂ : 𝟙 (WithInitial.star ⊗ WithInitial.of y) ≫ f = 𝟙 (WithInitial.star ⊗ WithInitial.of y) ≫ g
⊢ f = g
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:
simpa using

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

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

Goal state after:
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⦌)
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⦌)
h : ofSimplex { dim := n, simplex := s }.toN.simplex ≤ A
⊢ ofSimplex s ≤ A

Tactic:
simpa using

Goal state after:
X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
h : ofSimplex { dim := n, simplex := s }.toN.simplex ≤ A
⊢ s ∈ A.obj (Opposite.op ⦋n⦌)
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:
simpa using

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) (_root_.cast ⋯ y.simplex) = _root_.cast ⋯ x.simplex
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:
simpa using

Goal state after:
case pos.inl.left.inr
n : ℕ
x : Fin (n + 1)
hx : x.castSucc ≤ x.castSucc
⊢ x.castSucc ≤ x.succ
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

Tactic:
simpa using

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
⊢ j ≤ x
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:
simpa using

Goal state after:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) y = x
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 }
i : Fin (d + 2)
hi : (ConcreteCategory.hom (SimplicialObject.δ X.op i.rev)) (opObjEquiv.symm y) = opObjEquiv.symm x
⊢ i.rev = (hxy.index ⋯).rev

Tactic:
simpa using

Goal state after:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
i : Fin (d + 2)
hi : (ConcreteCategory.hom (SimplicialObject.δ X.op i.rev)) (opObjEquiv.symm y) = opObjEquiv.symm x
⊢ (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x
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:
simpa using

Goal state after:
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
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

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

Tactic:
simpa using

Goal state after:
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ i ≤ x
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:
simpa using

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
x y : ↑P.II
hxy : P.AncestralRel x y
⊢ (↑x).dim ≤ (↑y).dim
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
⊢ i.predAbove j < x

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
⊢ i.predAbove j < x

Tactic:
· rw [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
          exact hj.trans x.castSucc_lt_succ

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
⊢ i.predAbove j < x
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) }
f : ℕ → ↑(P.ofIso e hA).II
hf : ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ P.AncestralRel ((fun n ↦ ⟨(N.orderIsoOfIso e hA) ↑(f n), ⋯⟩) (n + 1)) ((fun n ↦ ⟨(N.orderIsoOfIso e hA) ↑(f n), ⋯⟩) n)

Tactic:
simpa using

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) }
f : ℕ → ↑(P.ofIso e hA).II
hf : ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ (P.ofIso e hA).AncestralRel (f (n + 1)) (f n)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

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

Tactic:
by
  intro x y hxy
  exact Finset.min'_subset _ (fun z hz ↦ by
    obtain ⟨z, rfl⟩ | rfl := z.eq_castSucc_or_eq_last
    · simp only [castSucc_mem_finset_iff] at hz ⊢
      exact hxy.trans hz
    · simp)

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
d : ℕ
a : A.N
hb✝ : (N.orderIsoOfIso e hA).symm a ∈ (P.ofIso e hA).II
hd : (↑⟨(N.orderIsoOfIso e hA).symm a, hb✝⟩).dim = d
hb : a ∈ P.II
⊢ ⋯.index hd ≠ 0

Tactic:
simpa using

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.IsProper
inst✝ : P.IsInner
d : ℕ
a : A.N
hb✝ : (N.orderIsoOfIso e hA).symm a ∈ (P.ofIso e hA).II
hd : (↑⟨(N.orderIsoOfIso e hA).symm a, hb✝⟩).dim = d
hb : a ∈ P.II
⊢ ⋯.index hd ≠ 0
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
d : ℕ
a : A.N
hb✝ : (N.orderIsoOfIso e hA).symm a ∈ (P.ofIso e hA).II
hd : (↑⟨(N.orderIsoOfIso e hA).symm a, hb✝⟩).dim = d
hb : a ∈ P.II
⊢ ⋯.index hd ≠ Fin.last (d + 1)

Tactic:
simpa using

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.IsProper
inst✝ : P.IsInner
d : ℕ
a : A.N
hb✝ : (N.orderIsoOfIso e hA).symm a ∈ (P.ofIso e hA).II
hd : (↑⟨(N.orderIsoOfIso e hA).symm a, hb✝⟩).dim = d
hb : a ∈ P.II
⊢ ⋯.index hd ≠ Fin.last (d + 1)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case h₁
x y : AugmentedSimplexCategory
⊢ x.inl y ≫ (𝟙 x ⊗ₘ 𝟙 y) = x.inl y ≫ 𝟙 (x ⊗ y)

Tactic:
simpa using

Goal state after:
case h₁
x y : AugmentedSimplexCategory
⊢ tensorHom (𝟙 x) (WithInitial.starInitial.to y) ≫ tensorHom (𝟙 x) (𝟙 y) =
    tensorHom (𝟙 x) (WithInitial.starInitial.to y)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case h₂
x y : AugmentedSimplexCategory
⊢ x.inr y ≫ (𝟙 x ⊗ₘ 𝟙 y) = x.inr y ≫ 𝟙 (x ⊗ y)

Tactic:
simpa using

Goal state after:
case h₂
x y : AugmentedSimplexCategory
⊢ tensorHom (WithInitial.starInitial.to x) (𝟙 y) ≫ tensorHom (𝟙 x) (𝟙 y) =
    tensorHom (WithInitial.starInitial.to x) (𝟙 y)
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:
simpa using

Goal state after:
p q n : ℕ
x : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
m : ℕ
hm : p + q = m
⊢ ↑x ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
y : ↑h.pairing.II
x : h.ι
hxy : h.pairing.AncestralRel (h.equivII x) y
⊢ f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm y)

Tactic:
obtain ⟨y, rfl⟩ := h.equivII.surjective y

Goal state after:
X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
x y : h.ι
hxy : h.pairing.AncestralRel (h.equivII x) (h.equivII y)
⊢ f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm (h.equivII y))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
x y : h.ι
hxy : h.AncestralRel x y
⊢ f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm (h.equivII y))

Tactic:
simpa using

Goal state after:
X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
x y : h.ι
hxy : h.AncestralRel x y
⊢ f.rank x < f.rank y
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
y : ↑h.pairing.II
x : h.ι
hxy : h.pairing.AncestralRel (h.equivII x) y
⊢ (↑(h.equivII x)).dim = (↑y).dim → f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm y)

Tactic:
obtain ⟨y, rfl⟩ := h.equivII.surjective y

Goal state after:
X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
x y : h.ι
hxy : h.pairing.AncestralRel (h.equivII x) (h.equivII y)
⊢ (↑(h.equivII x)).dim = (↑(h.equivII y)).dim →
    f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm (h.equivII y))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
x y : h.ι
hxy : h.AncestralRel x y
⊢ (↑(h.equivII x)).dim = (↑(h.equivII y)).dim →
    f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm (h.equivII y))

Tactic:
simpa using

Goal state after:
X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
x y : h.ι
hxy : h.AncestralRel x y
⊢ h.dim x = h.dim y → f.rank x < f.rank y
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: case refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
t : T
f : ⦋(↑↑t).dim⦌ ⟶ ⦋(↑(P.p y)).dim⦌
w✝ : CategoryTheory.Mono f
hf : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex = (↑↑t).simplex
⊢ (↑↑t).dim < (↑(P.p y)).dim

Tactic:
simpa using

Goal state after:
case refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
t : T
f : ⦋(↑↑t).dim⦌ ⟶ ⦋(↑(P.p y)).dim⦌
w✝ : CategoryTheory.Mono f
hf : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex = (↑↑t).simplex
⊢ (↑↑t).dim < (↑(P.p y)).dim
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : h.ι
⊢ h.type₁ x = ↑(h.pairing.p (h.equivII x))

Tactic:
simp +instances

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
s : h.ι
⊢ (↑(h.equivII s)).IsUniquelyCodimOneFace (↑(h.pairing.p (h.equivII s))).toS

Tactic:
simpa using

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
s : h.ι
⊢ (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝ : h.pairing.IsProper
s : h.ι
⊢ (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS

Tactic:
simpa using

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝ : h.pairing.IsProper
s : h.ι
⊢ (h.type₂ s).IsUniquelyCodimOneFace (↑(h.pairing.p (h.equivII s))).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ⋯.index ⋯ ≠ 0

Tactic:
simpa using

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ¬h.index s = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ⋯.index ⋯ ≠ Fin.last ((↑(h.equivII s)).dim + 1)

Tactic:
simpa using

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ¬h.index s = Fin.last (h.dim s + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
this : IsEmpty { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
x✝ : { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
f : ℕ → ↑h.pairing.II
hf : ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.AncestralRel ((fun n ↦ h.equivII.symm (f n)) (n + 1)) ((fun n ↦ h.equivII.symm (f n)) n)

Tactic:
simpa using

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
this : IsEmpty { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
x✝ : { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
f : ℕ → ↑h.pairing.II
hf : ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.pairing.AncestralRel (f (n + 1)) (f n)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝¹ : h.pairing.IsRegular
this✝ : h.IsProper
this : IsEmpty { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
x✝ : { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
f : ℕ → h.ι
hf : ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.pairing.AncestralRel ((fun n ↦ h.equivII (f n)) (n + 1)) ((fun n ↦ h.equivII (f n)) n)

Tactic:
simpa using

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝¹ : h.pairing.IsRegular
this✝ : h.IsProper
this : IsEmpty { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
x✝ : { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
f : ℕ → h.ι
hf : ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.pairing.AncestralRel (h.equivII (f (n + 1))) (h.equivII (f n))
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: case refine_2
ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
i : ι
⊢ Subcomplex.range (Sigma.ι X i ≫ f) ≤ ⨆ j, Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f)

Tactic:
exact le_trans (by rfl) (le_iSup _ ⟨i⟩)

Goal state after: