awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u
inst : LinearOrder J
⊢ Eq (α := EnrichedFunctor SSet (SimplicialThickening J) (SimplicialThickening J)) (functor OrderHom.id)
    (EnrichedFunctor.id SSet (SimplicialThickening J))

Tactic:
EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_

Premises used: CategoryTheory.EnrichedFunctor.ext, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u
inst : LinearOrder J
refine :
  ∀ (i j : SimplicialThickening J),
    Eq (α :=
      Quiver.Hom (V := SSet) (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j)
        (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _
          (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) i)
          (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) j)))
      (CategoryStruct.comp (Y :=
        @Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ (EnrichedFunctor.obj (functor OrderHom.id) i)
          (EnrichedFunctor.obj (functor OrderHom.id) j))
        (EnrichedFunctor.map (functor OrderHom.id) i j) (eqToHom ⋯))
      (EnrichedFunctor.map (EnrichedFunctor.id SSet (SimplicialThickening J)) i j)
⊢ Eq (α := EnrichedFunctor SSet (SimplicialThickening J) (SimplicialThickening J)) (functor OrderHom.id)
    (EnrichedFunctor.id SSet (SimplicialThickening J))

Tactic:
refine EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_

Premises used: CategoryTheory.EnrichedFunctor.ext, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u
inst : LinearOrder J
i j : SimplicialThickening J
w :
  ∀ (n : SimplexCategoryᵒᵖ) (x : Functor.obj (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j) n),
    Eq (α :=
      Functor.obj
        (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _
          (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) i)
          (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) j))
        n)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (CategoryStruct.comp (Y :=
              @Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ (EnrichedFunctor.obj (functor OrderHom.id) i)
                (EnrichedFunctor.obj (functor OrderHom.id) j))
              (EnrichedFunctor.map (functor OrderHom.id) i j) (eqToHom ⋯))
            n))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (EnrichedFunctor.map (EnrichedFunctor.id SSet (SimplicialThickening J)) i j) n))
        x)
⊢ Eq (α :=
    Quiver.Hom (V := SSet) (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j)
      (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _
        (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) i)
        (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) j)))
    (CategoryStruct.comp (Y :=
      @Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ (EnrichedFunctor.obj (functor OrderHom.id) i)
        (EnrichedFunctor.obj (functor OrderHom.id) j))
      (EnrichedFunctor.map (functor OrderHom.id) i j) (eqToHom ⋯))
    (EnrichedFunctor.map (EnrichedFunctor.id SSet (SimplicialThickening J)) i j)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u
inst : LinearOrder J
i j : SimplicialThickening J
n : SimplexCategoryᵒᵖ
x : Functor.obj (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j) n
⊢ Eq (α :=
    Functor.obj
      (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _
        (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) i)
        (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) j))
      n)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (CategoryStruct.comp (Y :=
            @Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ (EnrichedFunctor.obj (functor OrderHom.id) i)
              (EnrichedFunctor.obj (functor OrderHom.id) j))
            (EnrichedFunctor.map (functor OrderHom.id) i j) (eqToHom ⋯))
          n))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app (EnrichedFunctor.map (EnrichedFunctor.id SSet (SimplicialThickening J)) i j) n))
      x)

Tactic:
exact Functor.ext (by cat_disch)

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K L : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
inst_2 : LinearOrder L
f : J →o K
g : K →o L
⊢ functor (g.comp f) = EnrichedFunctor.comp SSet (functor f) (functor g)

Tactic:
EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_

Premises used: CategoryTheory.EnrichedFunctor.ext, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K L : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
inst_2 : LinearOrder L
f : J →o K
g : K →o L
refine :
  ∀ (i j : SimplicialThickening J),
    (functor (g.comp f)).map i j ≫ eqToHom ⋯ = (EnrichedFunctor.comp SSet (functor f) (functor g)).map i j
⊢ functor (g.comp f) = EnrichedFunctor.comp SSet (functor f) (functor g)

Tactic:
refine EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_

Premises used: CategoryTheory.EnrichedFunctor.ext, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K L : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
inst_2 : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
w :
  ∀ (n : SimplexCategoryᵒᵖ) (x : Functor.obj (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j) n),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ((functor (g.comp f)).map i j ≫ eqToHom ⋯) n)) x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (((EnrichedFunctor.comp SSet (functor f) (functor g)).map i j).app n)).toFun
        x
⊢ (functor (g.comp f)).map i j ≫ eqToHom ⋯ = (EnrichedFunctor.comp SSet (functor f) (functor g)).map i j

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K L : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
inst_2 : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
n : SimplexCategoryᵒᵖ
x : Functor.obj (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j) n
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ((functor (g.comp f)).map i j ≫ eqToHom ⋯) n)) x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((EnrichedFunctor.comp SSet (functor f) (functor g)).map i j).app n)).toFun
      x

Tactic:
exact Functor.ext (by cat_disch)

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
i : SimplexCategoryᵒᵖ
h :
  ∀ (x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾EnrichedFunctor.comp SSet
              (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (Quiver.Hom.unop (𝟙 i))).uliftMap)))
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
        x
⊢ ↾EnrichedFunctor.comp SSet
        (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (Quiver.Hom.unop (𝟙 i))).uliftMap) =
    𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
i : SimplexCategoryᵒᵖ
x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C
h :
  EnrichedFunctor.comp SSet (SimplicialThickening.functor OrderHom.id) x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet
            (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (Quiver.Hom.unop (𝟙 i))).uliftMap)))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x

Tactic:
change EnrichedFunctor.comp SSet (SimplicialThickening.functor OrderHom.id) _ = _

Premises used: OrderHom.id, SSet, CategoryTheory.EnrichedFunctor.comp, CategoryTheory.SimplicialThickening.functor
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
i : SimplexCategoryᵒᵖ
x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C
h :
  EnrichedFunctor.comp SSet
      (EnrichedFunctor.id SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1))))) x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x
⊢ EnrichedFunctor.comp SSet (SimplicialThickening.functor OrderHom.id) x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x

Tactic:
rw [SimplicialThickening.functor_id]

Premises used: CategoryTheory.SimplicialThickening.functor_id
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
i : SimplexCategoryᵒᵖ
x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C
⊢ EnrichedFunctor.comp SSet
      (EnrichedFunctor.id SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1))))) x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
X Y Z : SimplexCategoryᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X).len + 1)))) C),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾EnrichedFunctor.comp SSet
              (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (f ≫ g).unop).uliftMap)))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
            ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)))
        x
⊢ Eq (α :=
    EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X).len + 1)))) C ⟶
      EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop Z).len + 1)))) C)
    (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (f ≫ g).unop).uliftMap))
    (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
      ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
X Y Z : SimplexCategoryᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X).len + 1)))) C
h :
  EnrichedFunctor.comp SSet
      (SimplicialThickening.functor
        ((SimplexCategory.Hom.toOrderHom f.unop).uliftMap.comp (SimplexCategory.Hom.toOrderHom g.unop).uliftMap))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
          ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)))
      x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet
            (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (f ≫ g).unop).uliftMap)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
          ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)))
      x

Tactic:
change EnrichedFunctor.comp SSet (SimplicialThickening.functor
      (f.unop.toOrderHom.uliftMap.comp g.unop.toOrderHom.uliftMap)) _ = _

Premises used: Quiver.Hom.unop, OrderHom.comp, SSet, OrderHom.uliftMap, SimplexCategory.Hom.toOrderHom, CategoryTheory.EnrichedFunctor.comp, CategoryTheory.SimplicialThickening.functor
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
X Y Z : SimplexCategoryᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X).len + 1)))) C
h :
  EnrichedFunctor.comp SSet
      (EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)
        (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
          ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)))
      x
⊢ EnrichedFunctor.comp SSet
      (SimplicialThickening.functor
        ((SimplexCategory.Hom.toOrderHom f.unop).uliftMap.comp (SimplexCategory.Hom.toOrderHom g.unop).uliftMap))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
          ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)))
      x

Tactic:
rw [SimplicialThickening.functor_comp]

Premises used: CategoryTheory.SimplicialThickening.functor_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
X Y Z : SimplexCategoryᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X).len + 1)))) C
⊢ EnrichedFunctor.comp SSet
      (EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)
        (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
          ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)))
      x

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
inst_1 : SmallCategory J
inst_2 : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (Functor.{0, v, 0, u} SimplexCategoryᵒᵖ C)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
⊢ HasLimits (SimplicialObject.{v, u} C)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasLimitsOfSize.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
inst_1 : SmallCategory J
inst_2 : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (Functor.{0, v, 0, u} SimplexCategoryᵒᵖ C)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
⊢ HasColimits (SimplicialObject.{v, u} C)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
h h₁ : ∀ (x : SimplexCategoryᵒᵖ), f.app x = g.app x
⊢ f.app = g.app

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

Tactic:
apply h
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i = X.map (SimplexCategory.δ i).op

Tactic:
rfl

Premises used: CategoryTheory.SimplicialObject.δ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i = X.map (SimplexCategory.σ i).op

Tactic:
rfl

Premises used: rfl, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n m : ℕ
h : n = m
⊢ op ⦋n⦌ = op ⦋m⦌

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
h : n = n
⊢ X.eqToIso h = Iso.refl (X _⦋n⦌)

Tactic:
simp [eqToIso]

Premises used: CategoryTheory.SimplicialObject.eqToIso
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
dsimp :
  X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ j).op
⊢ X.δ j.succ ≫ X.δ i = X.δ i.castSucc ≫ X.δ j

Tactic:
dsimp [δ]

Premises used: CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ j).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ H]

Premises used: CategoryTheory.op_comp, SimplexCategory.δ_comp_δ, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
dsimp :
  X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ (j.pred ⋯)).op
⊢ X.δ j ≫ X.δ i = X.δ i.castSucc ≫ X.δ (j.pred ⋯)

Tactic:
dsimp [δ]

Premises used: CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ (j.pred ⋯)).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]

Premises used: SimplexCategory.δ_comp_δ', CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
dsimp :
  X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ (i.castLT ⋯)).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.δ j).op
⊢ X.δ j.succ ≫ X.δ (i.castLT ⋯) = X.δ i ≫ X.δ j

Tactic:
dsimp [δ]

Premises used: CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ (i.castLT ⋯)).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.δ j).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ'' H]

Premises used: CategoryTheory.op_comp, SimplexCategory.δ_comp_δ'', CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
dsimp :
  X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.succ).op ≫ X.map (SimplexCategory.δ i).op
⊢ X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i

Tactic:
dsimp [δ]

Premises used: CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.succ).op ≫ X.map (SimplexCategory.δ i).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ_self]

Premises used: CategoryTheory.op_comp, SimplexCategory.δ_comp_δ_self, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
j : Fin (n + 3)
i : Fin (n + 2)
H : j = i.castSucc
subst : X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i
⊢ X.δ j ≫ X.δ i = X.δ i.succ ≫ X.δ i

Tactic:
subst H
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
rw rw₁ : X.δ i.succ ≫ X.δ i = X.δ i.succ ≫ X.δ i
⊢ X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i

Tactic:
rw [δ_comp_δ_self]

Premises used: CategoryTheory.SimplicialObject.δ_comp_δ_self
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
dsimp :
  X.map (SimplexCategory.σ j.succ).op ≫ X.map (SimplexCategory.δ i.castSucc).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
⊢ X.σ j.succ ≫ X.δ i.castSucc = X.δ i ≫ X.σ j

Tactic:
dsimp [δ, σ]

Premises used: CategoryTheory.SimplicialObject.δ, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.σ j.succ).op ≫ X.map (SimplexCategory.δ i.castSucc).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_le H]

Premises used: CategoryTheory.op_comp, SimplexCategory.δ_comp_σ_of_le, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
dsimp : X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.castSucc).op = 𝟙 (X _⦋n⦌)
⊢ X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)

Tactic:
dsimp [δ, σ]

Premises used: CategoryTheory.SimplicialObject.δ, CategoryTheory.SimplicialObject.σ