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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (const D).map (F.map η.left) ≫
      { left := F.obj (point.obj Y✝), right := ((whiskering C D).obj F).obj (drop.obj Y✝),
          hom := (constComp SimplexCategory (point.obj Y✝) F).inv ≫ whiskerRight Y✝.hom F }.hom =
    { left := F.obj (point.obj X✝), right := ((whiskering C D).obj F).obj (drop.obj X✝),
          hom := (constComp SimplexCategory (point.obj X✝) F).inv ≫ whiskerRight X✝.hom F }.hom ≫
      (𝟭 (CosimplicialObject D)).map (whiskerRight η.right F)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
⊢ (const D).map (η.app (point.obj A)) ≫ ((whiskeringObj C D Y✝).obj A).hom =
    ((whiskeringObj C D X✝).obj A).hom ≫ (𝟭 (CosimplicialObject D)).map (whiskerLeft (drop.obj A) η)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ (whiskeringObj C D X✝).map f ≫ { left := η.app (point.obj x✝), right := whiskerLeft (drop.obj x✝) η, w := ⋯ } =
    { left := η.app (point.obj x✝¹), right := whiskerLeft (drop.obj x✝¹) η, w := ⋯ } ≫ (whiskeringObj C D Y✝).map f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((alternatingFaceMapComplex A).obj X).d (i + 1) i =
    ((normalizedMooreComplex A).obj X).d (i + 1) i ≫ (NormalizedMooreComplex.objX X i).arrow

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (inclusionOfMooreComplexMap X).f n = (NormalizedMooreComplex.objX X n).arrow

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : 1 ≤ 0
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 0
⊢ ¬1 ≤ 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X ^⦋0⦌
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ ∀ ⦃X_1 Y : SimplexCategory⦄ (f_1 : X_1 ⟶ Y),
    ((const C).obj X₀).map f_1 ≫ f ≫ X.map (⦋0⦌.const Y 0) =
      (f ≫ X.map (⦋0⦌.const X_1 0)) ≫ ((𝟭 (CosimplicialObject C)).obj X).map f_1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X ^⦋0⦌
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ (X.augment X₀ f w).hom.app ⦋0⦌ = f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : CosimplicialObject C
n : ℕ
⊢ objD X n = (AlternatingFaceMapComplex.objD ((cosimplicialSimplicialEquiv C).functor.obj (op X)) n).unop

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : Augmented C
⊢ X.rightOp.leftOp.right = X.right

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : Augmented Cᵒᵖ
⊢ X.leftOp.rightOp.left = X.left

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : 2 ≤ 0
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 0
⊢ ¬2 ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : CosimplicialObject C
n : ℕ
⊢ objD X n ≫ objD X (n + 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : 2 ≤ 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 1
⊢ ¬2 ≤ 1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (CosimplicialObject.const Cᵒᵖ).map f.unop.right.op ≫ (unop Y✝).rightOp.hom =
    (unop X✝).rightOp.hom ≫ (𝟭 (CosimplicialObject Cᵒᵖ)).map (NatTrans.rightOp f.unop.left)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
⊢ X = Y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ X = Y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x✝¹ x✝ : SimplexCategory
f g : x✝¹ ⟶ x✝
h : skeletalFunctor.map f = skeletalFunctor.map g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (𝟭 (SimplicialObject C)).map (NatTrans.leftOp f.right) ≫ X✝.leftOp.hom =
    Y✝.leftOp.hom ≫ (SimplicialObject.const C).map f.left.unop

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ f ≫ (unop Y✝).rightOpLeftOpIso.hom.op =
    (unop X✝).rightOpLeftOpIso.hom.op ≫
      Quiver.Hom.op { left := NatTrans.leftOp (NatTrans.rightOp f.unop.left), right := f.unop.right, w := ⋯ }

Tactic:
rw [← f.op_unop]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop.op ≫ (unop Y✝).rightOpLeftOpIso.hom.op =
    (unop X✝).rightOpLeftOpIso.hom.op ≫
      Quiver.Hom.op
        { left := NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left), right := f.unop.op.unop.right, w := ⋯ }
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
⊢ InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ }) ≫
      InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 }) =
    𝟙 (skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (𝟭 (SimplicialObject.Augmented C)ᵒᵖ).map f ≫ (unop Y✝).rightOpLeftOpIso.op.hom =
    (unop X✝).rightOpLeftOpIso.op.hom ≫
      (simplicialToCosimplicialAugmented C ⋙ cosimplicialToSimplicialAugmented C).map f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
⊢ InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 }) ≫
      InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ }) =
    𝟙 X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
hi : n + i = m
j : Fin (⦋n⦌.len + 1)
⊢ ↑j + i < ⦋m⦌.len + 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
hi : n + i = m
x✝¹ x✝ : Fin (⦋n⦌.len + 1)
⊢ x✝¹ ≤ x✝ → (fun j ↦ ⟨↑j + i, ⋯⟩) x✝¹ ≤ (fun j ↦ ⟨↑j + i, ⋯⟩) x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (n + 1)
hi : autoParam (n + i = m) δ₀Iter_apply._auto_1
⊢ ↑j + i < ⦋m⦌.len + 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ f.app ⦋n⦌ ≫ (obj Y).d n (n + 1) = (obj X).d n (n + 1) ≫ f.app ⦋n + 1⦌

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
h : n + (i + 1) = m
⊢ δ₀Iter (i + 1) h = δ 0 ≫ δ₀Iter i ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X : NonemptyFinLinOrd
⊢ skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌ ≅ X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ Mono f ↔ Function.Injective ⇑(Hom.toOrderHom f)

Tactic:
rw [← Functor.mono_map_iff_mono skeletalEquivalence.functor]

Goal state after:
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalEquivalence.functor.map f) ↔ Function.Injective ⇑(Hom.toOrderHom f)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ Mono f ↔ Function.Injective ⇑(Hom.toOrderHom f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ j ≤ ⟨↑k + i, ⋯⟩.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ Epi f ↔ Function.Surjective ⇑(Hom.toOrderHom f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
f : x ⟶ y
inst✝ : Mono f
⊢ Function.Injective (Hom.toOrderHom f).toFun

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
⊢ δ₀Iter i hi ≫ δ j = δ₀Iter (i + 1) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
f : x ⟶ y
inst✝ : Mono f
⊢ x.len ≤ y.len

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + 0 = m
hi'' : ↑i' = ↑i + 0
⊢ n = m

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
f : x ⟶ y
inst✝ : Epi f
⊢ Function.Surjective (Hom.toOrderHom f).toFun

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
f : x ⟶ y
inst✝ : Epi f
⊢ y.len ≤ x.len

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
n : ℕ
⊢ X.δ₀Iter 0 ⋯ = 𝟙 (X _⦋n⦌)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + i = m
⊢ X.δ₀Iter (i + 1) ⋯ = X.δ 0 ≫ X.δ₀Iter i h

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.δ₀Iter (i + 1) h = X.δ₀Iter i ⋯ ≫ X.δ 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.δ j ≫ X.δ₀Iter i hi = X.δ₀Iter (i + 1) ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : n + j = m
hi'' : ↑i' = ↑i + j
⊢ X.δ i' ≫ X.δ₀Iter j ⋯ = X.δ₀Iter j ⋯ ≫ X.δ i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
i i' : Fin (n + 2)
h : n + 0 = n
hi'' : ↑i' = ↑i + 0
⊢ i = i'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Epi (σ i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m),
    ↑i' = ↑i + j → δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : ↑i' = ↑i + (j + 1)
⊢ 0 ≤ i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m),
    ↑i' = ↑i + j → δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : ↑i' = ↑i + (j + 1)
⊢ ↑i' = ↑i.succ + j

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
⊢ f ≫ Hom.mk { toFun := ⇑(ConcreteCategory.hom (inv ((forget SimplexCategory).map f))), monotone' := ⋯ } = 𝟙 A✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
⊢ Hom.mk { toFun := ⇑(ConcreteCategory.hom (inv ((forget SimplexCategory).map f))), monotone' := ⋯ } ≫ f = 𝟙 B✝

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
⊢ X.σ j ≫ X.δ₀Iter (i + 1) hi = X.δ₀Iter i ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
hf : Mono f
h : n.len = m.len
⊢ n = m

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f : n ⟶ n
hf : Function.Injective ⇑(Hom.toOrderHom f)
h : n.len = n.len
⊢ Function.Surjective (Hom.toOrderHom f).toFun

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
hf : Mono f
⊢ IsIso f ↔ n.len = m.len

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + i = m
hj' : ↑j = ↑j' + i
⊢ X.σ j ≫ X.δ₀Iter i ⋯ = X.δ₀Iter i hi' ≫ X.σ j'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : n + j = m
hi'' : ↑i' = ↑i + j
⊢ δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Mono (δ i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
hf : Epi f
h : n.len = m.len
⊢ n = m

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
n : ℕ
⊢ X.σ₀Iter 0 ⋯ = 𝟙 (X _⦋n⦌)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f : n ⟶ n
hf : Function.Surjective ⇑(Hom.toOrderHom f)
h : n.len = n.len
⊢ Function.Injective (Hom.toOrderHom f).toFun

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
hf : Epi f
⊢ IsIso f ↔ n.len = m.len

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
n : ℕ
⊢ X.σ₀Iter 1 ⋯ = X.σ 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X✝ Y✝ : SimplexCategory
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
e : x ≅ y
i : Fin (x.len + 1)
⊢ (Hom.toOrderHom e.inv) ((Hom.toOrderHom e.hom) i) = i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
e : x ≅ y
i : Fin (y.len + 1)
⊢ (Hom.toOrderHom e.hom) ((Hom.toOrderHom e.inv) i) = i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ j.castSucc < ⟨↑k + (i + 1), ⋯⟩

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.σ₀Iter (i + 1) h = X.σ 0 ≫ X.σ₀Iter i ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x : SimplexCategory
e : x ≅ x
⊢ e = Iso.refl x

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + i = m
⊢ X.σ₀Iter (i + 1) ⋯ = X.σ₀Iter i h ≫ X.σ 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
⊢ δ₀Iter (i + 1) hi ≫ σ j = δ₀Iter i ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
⊢ X.σ₀Iter (j + 1) h ≫ X.δ i = X.σ₀Iter j ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + 0 = m
hj' : ↑j = ↑j' + 0
⊢ n = m

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : m + j = n
hi' : j < ↑i
hi'' : ↑i = ↑i' + j
⊢ X.σ₀Iter j ⋯ ≫ X.δ i = X.δ i' ≫ X.σ₀Iter j ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
j' j : Fin (n + 1)
hi' : n + 0 = n
hj' : ↑j = ↑j' + 0
⊢ j = j'

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.σ₀Iter i hi ≫ X.σ j = X.σ₀Iter (i + 1) ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + i = m
hj : ↑j = ↑j' + i
⊢ X.σ₀Iter i hi ≫ X.σ j = X.σ j' ≫ X.σ₀Iter i ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
hi : n + i = m
⊢ X.σ₀Iter i hi ≫ X.δ₀Iter i hi = 𝟙 (X _⦋n⦌)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
Y : Augmented C
n m i : ℕ
hi : n + i = m
⊢ Y.left.δ₀Iter i hi ≫ Y.hom.app (op ⦋n⦌) = Y.hom.app (op ⦋m⦌)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
Y : Augmented C
n m i : ℕ
hi : n + i = m
⊢ Y.left.σ₀Iter i hi ≫ Y.hom.app (op ⦋m⦌) = Y.hom.app (op ⦋n⦌)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
j : Fin (m + 1 + 1)
hi' : n + (i + 1) = m + 1
hj' : ↑j = ↑j' + (i + 1)
⊢ j ≠ 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n : ℕ
⊢ (X.σ 0 ≫ f.app (op ⦋n + 1⦌)) ≫ Y.δ 0 = f.app (op ⦋n⦌)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n : ℕ
⊢ (X.σ (Fin.last n) ≫ f.app (op ⦋n + 1⦌)) ≫ Y.δ (Fin.last (n + 1)) = f.app (op ⦋n⦌)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hij : i ≤ j.castSucc
⊢ (X.σ j.succ ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y.δ i.castSucc = X.δ i ≫ X.σ j ≫ f.app (op ⦋n✝ + 1⦌)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n✝ : ℕ
j : Fin (n✝ + 1)
⊢ (X.σ j.succ ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ =
    (X.σ j.castSucc ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hji : j.castSucc < i
⊢ (X.σ j.castSucc ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y.δ i.succ = X.δ i ≫ X.σ j ≫ f.app (op ⦋n✝ + 1⦌)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : i.castSucc < x
⊢ x ≠ 0

Tactic:
by

Goal state after: