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

Goal state before:
pp: n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 : (toOrderHom f) 0 = (toOrderHom g) 0
i : Fin (⦋0⦌.len + 1)
⊢ ↑((toOrderHom f) i) = ↑((toOrderHom g) i)

Tactic:
;

Goal state after:
n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 : (toOrderHom f) 0 = (toOrderHom g) 0
i : Fin (⦋0⦌.len + 1)
⊢ ↑((toOrderHom f) i) = ↑((toOrderHom g) i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f : ⦋0⦌ ⟶ n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom f) x) = ↑((Hom.toOrderHom (⦋0⦌.const n ((Hom.toOrderHom f) 0))) x)

Tactic:
;

Goal state after:
n : SimplexCategory
f : ⦋0⦌ ⟶ n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom f) x) = ↑((Hom.toOrderHom (⦋0⦌.const n ((Hom.toOrderHom f) 0))) x)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑i✝ + j = j + ↑i✝

Tactic:
;

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑i✝ + j = j + ↑i✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑i✝ + 1 + j = j + ↑i✝ + 1

Tactic:
;

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑i✝ + 1 + j = j + ↑i✝ + 1
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: Δ : SimplexCategory
f g : Δ ⟶ ⦋0⦌
x✝ : Fin (Δ.len + 1)
⊢ (Hom.toOrderHom f) x✝ = (Hom.toOrderHom g) x✝

Tactic:
;

Goal state after:
Δ : SimplexCategory
f g : Δ ⟶ ⦋0⦌
x✝ : Fin (Δ.len + 1)
⊢ (Hom.toOrderHom f) x✝ = (Hom.toOrderHom g) x✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n
x✝ : SimplexCategoryᵒᵖ
⊢ f.app x✝ = g.app x✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n
x✝ : SimplexCategoryᵒᵖ
⊢ f.app x✝ = g.app x✝
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasPullbacks C
X✝ Y✝ : SimplicialObject C
x✝² : X✝ ⟶ Y✝
x✝¹ : Mono x✝²
x✝ : ℕ
⊢ Mono (x✝².app (op ⦋x✝⦌))

Tactic:
;

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasPullbacks C
X✝ Y✝ : SimplicialObject C
x✝² : X✝ ⟶ Y✝
x✝¹ : Mono x✝²
x✝ : ℕ
⊢ Mono (x✝².app (op ⦋x✝⦌))
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

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

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategoryᵒᵖ
⊢ ((𝟭 (SimplicialObject D)).map (whiskerRight η.left F) ≫
          { left := ((whiskering C D).obj F).obj (drop.obj Y✝), right := F.obj (point.obj Y✝),
              hom := whiskerRight Y✝.hom F ≫ (constComp SimplexCategoryᵒᵖ Y✝.right F).hom }.hom).app
      n✝ =
    ({ left := ((whiskering C D).obj F).obj (drop.obj X✝), right := F.obj (point.obj X✝),
              hom := whiskerRight X✝.hom F ≫ (constComp SimplexCategoryᵒᵖ X✝.right F).hom }.hom ≫
          (const D).map (F.map η.right)).app
      n✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), f.app n = g.app n
x✝ : SimplexCategory
⊢ f.app x✝ = g.app x✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), f.app n = g.app n
x✝ : SimplexCategory
⊢ f.app x✝ = g.app x✝
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)
x✝ : ↑(skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌).toLinOrd
⊢ (LinOrd.Hom.hom
        (InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ }) ≫
            InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 })).hom)
      x✝ =
    (LinOrd.Hom.hom (𝟙 (skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌)).hom) x✝

Tactic:
;

Goal state after:
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)
x✝ : ↑(skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌).toLinOrd
⊢ (LinOrd.Hom.hom
        (InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ }) ≫
            InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 })).hom)
      x✝ =
    (LinOrd.Hom.hom (𝟙 (skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌)).hom) x✝
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)
x✝ : ↑X.toLinOrd
⊢ (LinOrd.Hom.hom
        (InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 }) ≫
            InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ })).hom)
      x✝ =
    (LinOrd.Hom.hom (𝟙 X).hom) x✝

Tactic:
;

Goal state after:
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)
x✝ : ↑X.toLinOrd
⊢ (LinOrd.Hom.hom
        (InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 }) ≫
            InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ })).hom)
      x✝ =
    (LinOrd.Hom.hom (𝟙 X).hom) x✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
;

Goal state after:
x y : SimplexCategory
f : x ⟶ y
inst✝ : Mono f
⊢ Function.Injective ⇑(Hom.toOrderHom f)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
;

Goal state after:
x y : SimplexCategory
f : x ⟶ y
inst✝ : Epi f
⊢ Function.Surjective ⇑(Hom.toOrderHom f)
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 : ℕ
hi' : n + (i + 1) = m + 1
hj' : ↑0 = ↑j' + (i + 1)
⊢ False

Tactic:
;

Goal state after:
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 : ℕ
hi' : n + (i + 1) = m + 1
hj' : ↑0 = ↑j' + (i + 1)
⊢ False
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 : ℕ
hi' : n + (i + 1) = m + 1
hj' : 0 = ↑j' + (i + 1)
⊢ False

Tactic:
;

Goal state after:
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 : ℕ
hi' : n + (i + 1) = m + 1
hj' : 0 = ↑j' + (i + 1)
⊢ False
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
h' : i.castSucc < 0
⊢ False

Tactic:
;

Goal state after:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
h' : i.castSucc < 0
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

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

Tactic:
;

Goal state after:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ ↑(Fin.castSucc 0) < ↑i'
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

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

Tactic:
;

Goal state after:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ 0 < ↑i'
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X : SSet
n k : ℕ
hk : n ≤ k
⊢ ⊥.toSSet.degenerate k = ⊤

Tactic:
ext ⟨x, hx⟩
    tauto

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
⊢ ∀ {X' X : Augmented C} {Y : Arrow C} (f : X' ⟶ X) (g : X ⟶ augmentedCechNerve.obj Y),
    equivalenceRightToLeft X' Y (f ≫ g) = Augmented.toArrow.map f ≫ equivalenceRightToLeft X Y g

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
⊢ ∀ {X' X : Augmented C} {Y : Arrow C} (f : X' ⟶ X) (g : X ⟶ augmentedCechNerve.obj Y),
    equivalenceRightToLeft X' Y (f ≫ g) = Augmented.toArrow.map f ≫ equivalenceRightToLeft X Y g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
s : X.S
⊢ ∃ (h : s.dim = s.dim), (s.cast h).simplex = s.simplex

Tactic:
;

Goal state after:
X : SSet
s : X.S
⊢ ∃ (h : s.dim = s.dim), (s.cast h).simplex = s.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
s t : X.S
x✝ : ∃ (h : s.dim = t.dim), (s.cast h).simplex = t.simplex
h₁ : s.dim = t.dim
h₂ : (s.cast h₁).simplex = t.simplex
⊢ s = t

Tactic:
obtain ⟨_, _, rfl⟩ := s.mk_surjective
    obtain ⟨_, _, rfl⟩ := t.mk_surjective
    aesop

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ X.S

Tactic:
;

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ X.S
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
i : Fin (n + 1)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
z : ↑(X.nonDegenerate m)
⊢ (ConcreteCategory.hom (SimplicialObject.σ X i)) ((ConcreteCategory.hom (X.map f.op)) ↑z) =
    (ConcreteCategory.hom (X.map (SimplexCategory.σ i).op)) ((ConcreteCategory.hom (X.map f.op)) ↑z)

Tactic:
;

Goal state after:
X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
i : Fin (n + 1)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
z : ↑(X.nonDegenerate m)
⊢ (ConcreteCategory.hom (SimplicialObject.σ X i)) ((ConcreteCategory.hom (X.map f.op)) ↑z) =
    (ConcreteCategory.hom (X.map (SimplexCategory.σ i).op)) ((ConcreteCategory.hom (X.map f.op)) ↑z)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
x✝¹ x✝ : ⊥.toSSet ⟶ Y
n✝ : SimplexCategoryᵒᵖ
val✝ : X.obj n✝
h : val✝ ∈ ⊥.obj n✝
⊢ (ConcreteCategory.hom (x✝¹.app n✝)).toFun ⟨val✝, h⟩ = (ConcreteCategory.hom (x✝.app n✝)).toFun ⟨val✝, h⟩

Tactic:
;

Goal state after:
X Y : SSet
x✝¹ x✝ : ⊥.toSSet ⟶ Y
n✝ : SimplexCategoryᵒᵖ
val✝ : X.obj n✝
h : val✝ ∈ ⊥.obj n✝
⊢ (ConcreteCategory.hom (x✝¹.app n✝)).toFun ⟨val✝, h⟩ = (ConcreteCategory.hom (x✝.app n✝)).toFun ⟨val✝, h⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
val✝ : X.obj x✝²
h : val✝ ∈ ⊥.obj x✝²
⊢ (ConcreteCategory.hom
          (⊥.toSSet.map x✝ ≫
            ↾fun x ↦
              match x with
              | ⟨val, h⟩ => ⋯.elim)).toFun
      ⟨val✝, h⟩ =
    (ConcreteCategory.hom
          ((↾fun x ↦
              match x with
              | ⟨val, h⟩ => ⋯.elim) ≫
            Y.map x✝)).toFun
      ⟨val✝, h⟩

Tactic:
;

Goal state after:
X Y : SSet
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
val✝ : X.obj x✝²
h : val✝ ∈ ⊥.obj x✝²
⊢ (ConcreteCategory.hom
          (⊥.toSSet.map x✝ ≫
            ↾fun x ↦
              match x with
              | ⟨val, h⟩ => ⋯.elim)).toFun
      ⟨val✝, h⟩ =
    (ConcreteCategory.hom
          ((↾fun x ↦
              match x with
              | ⟨val, h⟩ => ⋯.elim) ≫
            Y.map x✝)).toFun
      ⟨val✝, h⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ (ofSimplex x).image f = ofSimplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)

Tactic:
apply le_antisymm
  · rw [image_le_iff, ofSimplex_le_iff, preimage_obj, Set.mem_preimage]
    apply mem_ofSimplex_obj
  · rw [ofSimplex_le_iff]
    exact ⟨x, mem_ofSimplex_obj _, rfl⟩

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

Goal state before:
pp: X : SSet
x : X.N
⊢ x.subcomplex = x.subcomplex

Tactic:
;

Goal state after:
X : SSet
x : X.N
⊢ x.subcomplex = x.subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : X.obj x✝
hx : x ∈ A.obj x✝
⊢ (ConcreteCategory.hom (inv (f.app x✝))) ((ConcreteCategory.hom (f.app x✝)) x) ∈ A.obj x✝

Tactic:
;

Goal state after:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : X.obj x✝
hx : x ∈ A.obj x✝
⊢ (ConcreteCategory.hom (inv (f.app x✝))) ((ConcreteCategory.hom (f.app x✝)) x) ∈ A.obj x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x✝¹ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝¹ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝¹ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
hα₂ : Monotone α
x✝ : Fin (⦋m⦌.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (SimplexCategory.Hom.mk { toFun := α, monotone' := hα₂ } ≫ f₁)) x✝ =
    (SimplexCategory.Hom.toOrderHom (𝟙 ⦋m⦌)) x✝

Tactic:
;

Goal state after:
X : SSet
n : ℕ
x✝¹ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝¹ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝¹ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
hα₂ : Monotone α
x✝ : Fin (⦋m⦌.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (SimplexCategory.Hom.mk { toFun := α, monotone' := hα₂ } ≫ f₁)) x✝ =
    (SimplexCategory.Hom.toOrderHom (𝟙 ⦋m⦌)) x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x : X.S
⊢ x.toN.subcomplex = x.subcomplex

Tactic:
;

Goal state after:
X : SSet
x : X.S
⊢ x.toN.subcomplex = x.subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n → (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n

Tactic:
exact fun hx ↦ degenerate_app_apply hx f

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

Goal state before:
pp: X Y : Truncated 2
inst✝ : Subsingleton (X.obj (Opposite.op { obj := ⦋1⦌, property := _proof_2 }))
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
f g : Edge x y
⊢ f.edge = g.edge

Tactic:
;

Goal state after:
X Y : Truncated 2
inst✝ : Subsingleton (X.obj (Opposite.op { obj := ⦋1⦌, property := _proof_2 }))
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
f g : Edge x y
⊢ f.edge = g.edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_1
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op))

Tactic:
;

Goal state after:
case refine_1
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_2
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op))

Tactic:
;

Goal state after:
case refine_2
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_3
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 0 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op))

Tactic:
;

Goal state after:
case refine_3
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 0 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_4
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 0 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op))

Tactic:
;

Goal state after:
case refine_4
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 0 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_5
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op))

Tactic:
;

Goal state after:
case refine_5
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_6
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op))

Tactic:
;

Goal state after:
case refine_6
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ⇑(ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ ((ConcreteCategory.hom (SimplicialObject.σ (nerve C) 0)) (ComposableArrows.mk₀ x)).hom = eqToHom ⋯

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ ((ConcreteCategory.hom (SimplicialObject.σ (nerve C) 0)) (ComposableArrows.mk₀ x)).hom = eqToHom ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) (ComposableArrows.mk₂ f g)) = f

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) (ComposableArrows.mk₂ f g)) = f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) (ComposableArrows.mk₂ f g)) = g

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) (ComposableArrows.mk₂ f g)) = g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) (ComposableArrows.mk₂ f g)) = f ≫ g

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) (ComposableArrows.mk₂ f g)) = f ≫ g