awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y Z : Functor.{v, v', u, u'} C D
x : X_1 ⟶ Y
x_1 : Y ⟶ Z
x_2 : Augmented.{v, u} C
n : SimplexCategoryᵒᵖ
⊢ ({
                app := fun (A : Augmented.{v, u} C) ↦
                  { left := whiskerLeft (obj drop A) (x ≫ x_1), right := (x ≫ x_1).app (obj point A), w := ⋯ :
                    CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Z).obj A) },
                naturality := ⋯ : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Z) }.app
            x_2).left.app
      n =
    NatTrans.app
      (CommaMorphism.left
        (NatTrans.app
          ({
              app := fun (A : Augmented.{v, u} C) ↦
                { left := whiskerLeft (obj drop A) x, right := x.app (obj point A), w := ⋯ :
                  CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Y).obj A) },
              naturality := ⋯ : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Y) } ≫
            {
              app := fun (A : Augmented.{v, u} C) ↦
                { left := whiskerLeft (obj drop A) x_1, right := x_1.app (obj point A), w := ⋯ },
              naturality := ⋯ })
          x_2))
      n

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y Z : Functor.{v, v', u, u'} C D
x : X_1 ⟶ Y
x_1 : Y ⟶ Z
x_2 : Augmented.{v, u} C
⊢ ({
            app := fun (A : Augmented.{v, u} C) ↦
              { left := whiskerLeft (obj drop A) (x ≫ x_1), right := (x ≫ x_1).app (obj point A), w := ⋯ :
                CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Z).obj A) },
            naturality := ⋯ : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Z) }.app
        x_2).right =
    CommaMorphism.right
      (NatTrans.app
        ({
            app := fun (A : Augmented.{v, u} C) ↦
              { left := whiskerLeft (obj drop A) x, right := x.app (obj point A), w := ⋯ :
                CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Y).obj A) },
            naturality := ⋯ : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Y) } ≫
          {
            app := fun (A : Augmented.{v, u} C) ↦
              { left := whiskerLeft (obj drop A) x_1, right := x_1.app (obj point A), w := ⋯ },
            naturality := ⋯ })
        x_2)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X_1 X : SimplicialObject.{v, u} 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
dsimp :
  X.map g ≫ X.map (Quiver.Hom.op (⦋0⦌.const (unop j) 0)) ≫ f = (X.map (Quiver.Hom.op (⦋0⦌.const (unop i) 0)) ≫ f) ≫ 𝟙 X₀
⊢ (obj (𝟭 (SimplicialObject.{v, u} C)) X).map g ≫ X.map (Quiver.Hom.op (⦋0⦌.const (unop j) 0)) ≫ f =
    (X.map (Quiver.Hom.op (⦋0⦌.const (unop i) 0)) ≫ f) ≫ map (obj (const C) X₀) g

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X_1 X : SimplicialObject.{v, u} 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
rw :
  X.map g.unop.op ≫ X.map (Quiver.Hom.op (⦋0⦌.const (unop j) 0)) ≫ f =
    (X.map (Quiver.Hom.op (⦋0⦌.const (unop i) 0)) ≫ f) ≫ 𝟙 X₀
⊢ X.map g ≫ X.map (Quiver.Hom.op (⦋0⦌.const (unop j) 0)) ≫ f = (X.map (Quiver.Hom.op (⦋0⦌.const (unop i) 0)) ≫ f) ≫ 𝟙 X₀

Tactic:
rw [← g.op_unop]

Premises used: Quiver.Hom.op_unop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X_1 X : SimplicialObject.{v, u} 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.unop.op ≫ X.map (Quiver.Hom.op (⦋0⦌.const (unop j) 0)) ≫ f =
    (X.map (Quiver.Hom.op (⦋0⦌.const (unop i) 0)) ≫ f) ≫ 𝟙 X₀

Tactic:
simpa only [← X.map_comp, ← Category.assoc, Category.comp_id, ← op_comp] using w _ _ _

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
⊢ (X.augment X₀ f w).hom.app (op ⦋0⦌) = f

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Category.{v, max u v} (Functor.{0, v, 0, u} SimplexCategory C)

Tactic:
infer_instance
-- 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 (CosimplicialObject.{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 (CosimplicialObject.{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 : CosimplicialObject.{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 : CosimplicialObject.{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 : CosimplicialObject.{v, u} C
n m : ℕ
h : n = m
rw rw₁ : ⦋m⦌ = ⦋m⦌
⊢ ⦋n⦌ = ⦋m⦌

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

Tactic:
simp [eqToIso]

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

Tactic:
dsimp [δ]

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

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

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

Tactic:
dsimp [δ]

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

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

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

Tactic:
dsimp [δ]

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

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

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

Tactic:
dsimp [δ]

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

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

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

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

Tactic:
rw [δ_comp_δ_self]

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

Tactic:
dsimp [δ, σ]

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

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

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

Tactic:
dsimp [δ, σ]

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

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

Premises used: CategoryTheory.Functor.map_id, SimplexCategory.δ_comp_σ_self, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
subst : X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)
⊢ X.δ j ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
subst H
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
rw rw₁ : Eq.{v + 1} (α := X ^⦋n⦌ ⟶ X ^⦋n⦌) (𝟙 (X ^⦋n⦌)) (𝟙 (X ^⦋n⦌))
⊢ X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
rw [δ_comp_σ_self]

Premises used: CategoryTheory.CosimplicialObject.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
dsimp : X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X ^⦋n⦌)
⊢ X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
dsimp [δ, σ]

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

Tactic:
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_succ, X.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, SimplexCategory.δ_comp_σ_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
subst : X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)
⊢ X.δ j ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
subst H
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
rw rw₁ : Eq.{v + 1} (α := X ^⦋n⦌ ⟶ X ^⦋n⦌) (𝟙 (X ^⦋n⦌)) (𝟙 (X ^⦋n⦌))
⊢ X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
rw [δ_comp_σ_succ]

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

Tactic:
dsimp [δ, σ]

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

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

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

Tactic:
dsimp [δ, σ]

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

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

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

Tactic:
dsimp [δ, σ]

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

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

Premises used: CategoryTheory.Functor.map_comp, SimplexCategory.σ_comp_σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X' X : CosimplicialObject.{v, u} C
f : X ⟶ X'
n : ℕ
i : Fin (n + 2)
⊢ X.δ i ≫ f.app ⦋n + 1⦌ = f.app ⦋n⦌ ≫ X'.δ i

Tactic:
f.naturality _

Premises used: CategoryTheory.CosimplicialObject.δ, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X' X : CosimplicialObject.{v, u} C
f : X ⟶ X'
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ f.app ⦋n⦌ = f.app ⦋n + 1⦌ ≫ X'.σ i

Tactic:
f.naturality _

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.CosimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
J : Type v
inst_1 : SmallCategory J
inst_2 : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (Functor.{0, v, 0, u} (SimplexCategory.Truncated n) C)

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

Tactic:
⟨inferInstance⟩

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

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

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 : Augmented.{v, u} C
η : X ⟶ Y
n : SimplexCategory
⊢ η.left ≫ Y.hom.app n = X.hom.app n ≫ η.right.app n

Tactic:
NatTrans.congr_app η.w n

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.NatTrans.congr_app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
X_1 Y : Augmented.{v, u} C
η : X_1 ⟶ Y
⊢ Eq (α :=
    obj.{v, v, u, u} (𝟭 C)
        (Comma.left.{v, v, v, u, u, u} (T := C) (L := 𝟭 C) (R := 𝟭 C)
          { left := obj point X_1, right := obj drop X_1 ^⦋0⦌, hom := X_1.hom.app ⦋0⦌ :
            Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }) ⟶
      obj.{v, v, u, u} (𝟭 C)
        (Comma.right.{v, v, v, u, u, u} (T := C) (L := 𝟭 C) (R := 𝟭 C)
          { left := obj point Y, right := obj drop Y ^⦋0⦌, hom := Y.hom.app ⦋0⦌ :
            Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }))
    (map (𝟭 C) (map point η) ≫
        Comma.hom
          { left := obj point Y, right := obj drop Y ^⦋0⦌, hom := Y.hom.app ⦋0⦌ :
            Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :
      obj.{v, v, u, u} (𝟭 C)
          (Comma.left.{v, v, v, u, u, u} (T := C) (L := 𝟭 C) (R := 𝟭 C)
            { left := obj point X_1, right := obj drop X_1 ^⦋0⦌, hom := X_1.hom.app ⦋0⦌ :
              Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }) ⟶
        obj.{v, v, u, u} (𝟭 C)
          (Comma.right.{v, v, v, u, u, u} (T := C) (L := 𝟭 C) (R := 𝟭 C)
            { left := obj point Y, right := obj drop Y ^⦋0⦌, hom := Y.hom.app ⦋0⦌ :
              Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }))
    (Comma.hom
          { left := obj point X_1, right := obj drop X_1 ^⦋0⦌, hom := X_1.hom.app ⦋0⦌ :
            Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≫
        map (𝟭 C) (NatTrans.app (map drop η) ⦋0⦌) :
      obj.{v, v, u, u} (𝟭 C)
          (Comma.left.{v, v, v, u, u, u} (T := C) (L := 𝟭 C) (R := 𝟭 C)
            { left := obj point X_1, right := obj drop X_1 ^⦋0⦌, hom := X_1.hom.app ⦋0⦌ :
              Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }) ⟶
        obj.{v, v, u, u} (𝟭 C)
          (Comma.right.{v, v, v, u, u, u} (T := C) (L := 𝟭 C) (R := 𝟭 C)
            { left := obj point Y, right := obj drop Y ^⦋0⦌, hom := Y.hom.app ⦋0⦌ :
              Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }))

Tactic:
simp [w_app]

Premises used: CategoryTheory.CosimplicialObject.Augmented.w_app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X_1 Y : Augmented.{v, u} C
η : X_1 ⟶ Y
h :
  ∀ (n : SimplexCategory),
    (map (const D) (F.map η.left) ≫
            { left := F.obj (obj point Y), right := (obj (whiskering C D) F).obj (obj drop Y),
                hom := Iso.inv (constComp SimplexCategory (obj point Y) F) ≫ whiskerRight Y.hom F :
                Comma (const D) (𝟭 (CosimplicialObject.{v_1, u_1} D)) }.hom).app
        n =
      ({ left := F.obj (obj point X_1), right := (obj (whiskering C D) F).obj (obj drop X_1),
                hom := Iso.inv (constComp SimplexCategory (obj point X_1) F) ≫ whiskerRight X_1.hom F :
                Comma (const D) (𝟭 (CosimplicialObject.{v_1, u_1} D)) }.hom ≫
            map (𝟭 (CosimplicialObject.{v_1, u_1} D)) (whiskerRight η.right F)).app
        n
⊢ map (const D) (F.map η.left) ≫
      { left := F.obj (obj point Y), right := (obj (whiskering C D) F).obj (obj drop Y),
          hom := Iso.inv (constComp SimplexCategory (obj point Y) F) ≫ whiskerRight Y.hom F :
          Comma (const D) (𝟭 (CosimplicialObject.{v_1, u_1} D)) }.hom =
    { left := F.obj (obj point X_1), right := (obj (whiskering C D) F).obj (obj drop X_1),
          hom := Iso.inv (constComp SimplexCategory (obj point X_1) F) ≫ whiskerRight X_1.hom F :
          Comma (const D) (𝟭 (CosimplicialObject.{v_1, u_1} D)) }.hom ≫
      map (𝟭 (CosimplicialObject.{v_1, u_1} D)) (whiskerRight η.right F)

Tactic:
ext