mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h.left
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C := ⋯
i : Y ⟶ F := ⋯
e : F ⟶ Y := ⋯
j : J
⊢ (i ≫ e).app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = (𝟙 Y).app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)

Tactic:
dsimp

Goal state after:
case h.left
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C :=
  { obj := fun j ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j'} φ ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯, map_comp := ⋯ }
i : Y ⟶ F := { app := fun j ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
e : F ⟶ Y := { app := fun j ↦ equalizer.lift (p.app j) ⋯, naturality := ⋯ }
j : J
⊢ (i.app j ≫ e.app j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑(i, j).2 • X.δ (i, j).2) ≫ ((-1) ^ ↑(i, j).1 • X.δ (i, j).1) =
    -((-1) ^ ↑(φ (i, j) hij).2 • X.δ (φ (i, j) hij).2) ≫ ((-1) ^ ↑(φ (i, j) hij).1 • X.δ (φ (i, j) hij).1)

Tactic:
dsimp

Goal state after:
case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑j • X.δ j) ≫ ((-1) ^ ↑i • X.δ i) =
    -((-1) ^ ↑(φ (i, j) hij).2 • X.δ (φ (i, j) hij).2) ≫ ((-1) ^ ↑(φ (i, j) hij).1 • X.δ (φ (i, j) hij).1)
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
⊢ autoParam
    (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
      ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
        eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

pp: case h_obj.h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
⊢ ∀ (X_1 : J),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj X_1 =
      (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj X_1

Tactic:
· intro j j' φ
      ext
      simp

Goal state after:
case h_obj.h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
⊢ ∀ (X_1 : J),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj X_1 =
      (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj X_1
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 (((alternatingFaceMapComplex C).map x✝²).f x✝)

Tactic:
dsimp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f =
    P.p.app (op ⦋n + 1⦌) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f =
    P.p.app (op ⦋n + 1⦌) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).d 1 0 ≫ X.hom.app (op ⦋0⦌) = 0

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ ((alternatingFaceMapComplex C).obj X.left).d 1 0 ≫ X.hom.app (op ⦋0⦌) = 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

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

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
n : SimplexCategoryᵒᵖ
⊢ η.app (A.left.obj n) ≫ Y✝.map (A.hom.app n) ≫ 𝟙 (Y✝.obj A.right) =
    (X✝.map (A.hom.app n) ≫ 𝟙 (X✝.obj A.right)) ≫ η.app A.right
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ ((𝟭 (SimplicialObject C)).obj X).map g ≫ X.map (⦋0⦌.const (unop j) 0).op ≫ f =
    (X.map (⦋0⦌.const (unop i) 0).op ≫ f) ≫ ((const C).obj X₀).map g

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g ≫ X.map (⦋0⦌.const (unop j) 0).op ≫ f = (X.map (⦋0⦌.const (unop i) 0).op ≫ f) ≫ 𝟙 X₀
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inl ⟨1, ?_⟩
    ext i : 3
    match i with
    | 0 => exact e0
    | 1 => exact e1

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_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategory
⊢ ((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).app
      n✝ =
    ({ 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)).app
      n✝

Tactic:
dsimp

Goal state after:
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✝
n✝ : SimplexCategory
⊢ F.map η.left ≫ 𝟙 (F.obj Y✝.left) ≫ F.map (Y✝.hom.app n✝) =
    (𝟙 (F.obj X✝.left) ≫ F.map (X✝.hom.app n✝)) ≫ F.map (η.right.app n✝)
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
n : SimplexCategory
⊢ ((const D).map (η.app (point.obj A)) ≫ ((whiskeringObj C D Y✝).obj A).hom).app n =
    (((whiskeringObj C D X✝).obj A).hom ≫ (𝟭 (CosimplicialObject D)).map (whiskerLeft (drop.obj A) η)).app n

Tactic:
dsimp

Goal state after:
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
n : SimplexCategory
⊢ η.app A.left ≫ 𝟙 (Y✝.obj A.left) ≫ Y✝.map (A.hom.app n) =
    (𝟙 (X✝.obj A.left) ≫ X✝.map (A.hom.app n)) ≫ η.app (A.right.obj n)
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₂
i j : SimplexCategory
g : i ⟶ j
⊢ ((const C).obj X₀).map g ≫ f ≫ X.map (⦋0⦌.const j 0) =
    (f ≫ X.map (⦋0⦌.const i 0)) ≫ ((𝟭 (CosimplicialObject C)).obj X).map g

Tactic:
dsimp

Goal state after:
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₂
i j : SimplexCategory
g : i ⟶ j
⊢ 𝟙 X₀ ≫ f ≫ X.map (⦋0⦌.const j 0) = (f ≫ X.map (⦋0⦌.const i 0)) ≫ X.map g
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✝
x : SimplexCategory
⊢ ((CosimplicialObject.const Cᵒᵖ).map f.unop.right.op ≫ (unop Y✝).rightOp.hom).app x =
    ((unop X✝).rightOp.hom ≫ (𝟭 (CosimplicialObject Cᵒᵖ)).map (NatTrans.rightOp f.unop.left)).app x

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ f.unop.right.op ≫ ((unop Y✝).hom.app (op x)).op = ((unop X✝).hom.app (op x)).op ≫ (f.unop.left.app (op x)).op
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✝
x : SimplexCategoryᵒᵖ
⊢ ((𝟭 (SimplicialObject C)).map (NatTrans.leftOp f.right) ≫ X✝.leftOp.hom).app x =
    (Y✝.leftOp.hom ≫ (SimplicialObject.const C).map f.left.unop).app x

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ (f.right.app (unop x)).unop ≫ (X✝.hom.app (unop x)).unop = (Y✝.hom.app (unop x)).unop ≫ f.left.unop
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:
dsimp

Goal state after:
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 := ⋯ }
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ ↑⟨↑k + (i + 1), ⋯⟩ = ↑⟨↑(Fin.succAbove 0 k) + i, ⋯⟩

Tactic:
dsimp

Goal state after:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ ↑k + (i + 1) = ↑k + 1 + i
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:
dsimp

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).toFun

Tactic:
dsimp

Goal state after:
x y : SimplexCategory
f : x ⟶ y
inst✝ : Epi f
⊢ Function.Surjective ⇑(Hom.toOrderHom f)
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
  simp [δ₀Iter]

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:
simp [δ₀Iter, SimplexCategory.δ₀Iter_succ _ h, δ_def]

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)
⊢ ↑(⟨↑k + (i + 1), ⋯⟩.pred ⋯) = ↑⟨↑k + i, ⋯⟩

Tactic:
dsimp

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

Goal state before:
pp: case pos
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
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ (Hom.toOrderHom θ) i.succ = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) i)

Tactic:
refine hi.symm.trans ?_

Goal state after:
case pos
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
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
k : Fin (⦋n + 1⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ₀Iter 1 ⋯)) k) = ↑((ConcreteCategory.hom (σ 0)) k)

Tactic:
dsimp

Goal state after:
n : ℕ
k : Fin (⦋n + 1⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ₀Iter 1 ⋯)) k) = ↑((ConcreteCategory.hom (σ 0)) k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case inl
n : ℕ
⊢ 0 = ↑(Fin.castPred 0 ⋯)

Tactic:
dsimp

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

Goal state before:
pp: n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y

Tactic:
by_cases h : x < y

Goal state after:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : x < y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y

case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ i ≫ σ₀Iter (j + 1) h)) k) = ↑((ConcreteCategory.hom (σ₀Iter j ⋯)) k)

Tactic:
dsimp

Goal state after:
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ i ≫ σ₀Iter (j + 1) h)) k) = ↑((ConcreteCategory.hom (σ₀Iter j ⋯)) k)
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:
dsimp

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

Goal state before:
pp: X Y : SSet
y : Y _⦋0⦌
x✝³ x✝² : SimplexCategoryᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj x✝³
⊢ (ConcreteCategory.hom
          (X.map x✝¹ ≫ ↾fun x ↦ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝²).const ⦋0⦌ 0).op)) y)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((↾fun x ↦ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝³).const ⦋0⦌ 0).op)) y) ≫ Y.map x✝¹)).toFun
      x✝

Tactic:
dsimp

Goal state after:
X Y : SSet
y : Y _⦋0⦌
x✝³ x✝² : SimplexCategoryᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj x✝³
⊢ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝²).const ⦋0⦌ 0).op)) y =
    (ConcreteCategory.hom (Y.map x✝¹)) ((ConcreteCategory.hom (Y.map ((Opposite.unop x✝³).const ⦋0⦌ 0).op)) y)
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 : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ X.left.map f ≫
      WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
        (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop y) i).op ≫ Arrow.Hom.left G) ⋯ =
    WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
        (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ⋯ ≫
      F.augmentedCechNerve.left.map f

Tactic:
dsimp

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 : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ X.left.map f ≫
      WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
        (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop y) i).op ≫ Arrow.Hom.left G) ⋯ =
    WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
        (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ⋯ ≫
      WidePullback.lift (WidePullback.base fun x ↦ F.hom)
        (fun i ↦ WidePullback.π (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X : SSet
A B : X.Subcomplex
d : ℕ
inst✝ : X.HasDimensionLT d
⊢ A ≤ B ↔ ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)

Tactic:
refine ⟨fun h i hi a ⟨ha, _⟩ ↦ h _ ha, fun h ↦ ?_⟩

Goal state after:
X : SSet
A B : X.Subcomplex
d : ℕ
inst✝ : X.HasDimensionLT d
h : ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)
⊢ A ≤ B
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F.augmentedCechConerve ⟶ X
⊢ G.left ≫ (Augmented.toArrow.obj X).hom = F.hom ≫ WidePushout.ι (fun x ↦ F.hom) 0 ≫ G.right.app ⦋0⦌

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F.augmentedCechConerve ⟶ X
⊢ G.left ≫ X.hom.app ⦋0⦌ = F.hom ≫ WidePushout.ι (fun x ↦ F.hom) 0 ≫ G.right.app ⦋0⦌
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ F.augmentedCechConerve.right.map f ≫
      WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ =
    WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app x) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
      X.right.map f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ WidePushout.desc (WidePushout.head fun x ↦ F.hom)
        (fun i ↦ WidePushout.ι (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f) i)) ⋯ ≫
      WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ =
    WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app x) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
      X.right.map f
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₂.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
j : Fin (x.len + 1)
⊢ WidePushout.ι (fun x ↦ F.hom) j ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    WidePushout.ι (fun x ↦ F.hom) j ≫ A.right.app x

Tactic:
dsimp

Goal state after:
case h₂.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
j : Fin (x.len + 1)
⊢ WidePushout.ι (fun x ↦ F.hom) j ≫
      WidePushout.desc (A.left ≫ X.hom.app x)
        (fun i ↦ (WidePushout.ι (fun x ↦ F.hom) 0 ≫ A.right.app ⦋0⦌) ≫ X.right.map (⦋0⦌.const x i)) ⋯ =
    WidePushout.ι (fun x ↦ F.hom) j ≫ A.right.app x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case neg
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)
⊢ ∃ m_1 f_1,
    ∃ (_ : Epi f_1),
      ∃ y,
        (ConcreteCategory.hom (SimplicialObject.σ X i)) ((ConcreteCategory.hom (X.map f.op)) ↑z) =
          (ConcreteCategory.hom (X.map f_1.op)) ↑y

Tactic:
exact ⟨_, SimplexCategory.σ i ≫ f, inferInstance, z, by simp; rfl⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₂.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x ↦ F.hom) ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    (WidePushout.head fun x ↦ F.hom) ≫ A.right.app x

Tactic:
dsimp

Goal state after:
case h₂.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x ↦ F.hom) ≫
      WidePushout.desc (A.left ≫ X.hom.app x)
        (fun i ↦ (WidePushout.ι (fun x ↦ F.hom) 0 ≫ A.right.app ⦋0⦌) ≫ X.right.map (⦋0⦌.const x i)) ⋯ =
    (WidePushout.head fun x ↦ F.hom) ≫ A.right.app x
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.N
h : x ≤ y
⊢ x.dim ≤ y.dim

Tactic:
by
  rw [le_iff_exists_mono] at h
  obtain ⟨f, hf, _⟩ := h
  exact SimplexCategory.len_le_of_mono f

Goal state after: