[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ Category.{?u.61, max u v} (SimplicialObject C)
[PROOFSTEP]
dsimp only [SimplicialObject]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ Category.{?u.61, max u v} (SimplexCategoryᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplicialObject C)
[PROOFSTEP]
dsimp [SimplicialObject]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplexCategoryᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplicialObject C)
[PROOFSTEP]
dsimp [SimplicialObject]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplexCategoryᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), NatTrans.app f n = NatTrans.app g n
⊢ f.app = g.app
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), NatTrans.app f n = NatTrans.app g n
x✝ : SimplexCategoryᵒᵖ
⊢ NatTrans.app f x✝ = NatTrans.app g x✝
[PROOFSTEP]
apply h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n m : ℕ
h : n = m
⊢ op [n] = op [m]
[PROOFSTEP]
congr
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
h : n = n
⊢ eqToIso X h = Iso.refl (X.obj (op [n]))
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
h : n = n
⊢ (eqToIso X h).hom = (Iso.refl (X.obj (op [n]))).hom
[PROOFSTEP]
simp [eqToIso]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ X (Fin.succ j) ≫ δ X i = δ X (Fin.castSucc i) ≫ δ X j
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.map (SimplexCategory.δ (Fin.succ j)).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (Fin.castSucc i)).op ≫ X.map (SimplexCategory.δ j).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
hj : j = 0
⊢ False
[PROOFSTEP]
simp [hj, Fin.not_lt_zero] at H 
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
⊢ δ X j ≫ δ X i = δ X (Fin.castSucc i) ≫ δ X (Fin.pred j (_ : j = 0 → False))
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
⊢ X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (Fin.castSucc i)).op ≫ X.map (SimplexCategory.δ (Fin.pred j (_ : j = 0 → False))).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ Fin.castSucc j
⊢ δ X (Fin.succ j) ≫ δ X (Fin.castLT i (_ : ↑i < n + 2)) = δ X i ≫ δ X j
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ Fin.castSucc j
⊢ X.map (SimplexCategory.δ (Fin.succ j)).op ≫ X.map (SimplexCategory.δ (Fin.castLT i (_ : ↑i < n + 2))).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.δ j).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ'' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ δ X (Fin.castSucc i) ≫ δ X i = δ X (Fin.succ i) ≫ δ X i
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ (Fin.castSucc i)).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (Fin.succ i)).op ≫ X.map (SimplexCategory.δ i).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 3)
i : Fin (n + 2)
H : j = Fin.castSucc i
⊢ δ X j ≫ δ X i = δ X (Fin.succ i) ≫ δ X i
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ δ X (Fin.castSucc i) ≫ δ X i = δ X (Fin.succ i) ≫ δ X i
[PROOFSTEP]
rw [δ_comp_δ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ Fin.castSucc j
⊢ σ X (Fin.succ j) ≫ δ X (Fin.castSucc i) = δ X i ≫ σ X j
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ Fin.castSucc j
⊢ X.map (SimplexCategory.σ (Fin.succ j)).op ≫ X.map (SimplexCategory.δ (Fin.castSucc i)).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_le H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ σ X i ≫ δ X (Fin.castSucc i) = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ (Fin.castSucc i)).op = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_self, op_id, X.map_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = Fin.castSucc i
⊢ σ X i ≫ δ X j = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ σ X i ≫ δ X (Fin.castSucc i) = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
rw [δ_comp_σ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ σ X i ≫ δ X (Fin.succ i) = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ (Fin.succ i)).op = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_succ, op_id, X.map_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = Fin.succ i
⊢ σ X i ≫ δ X j = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ σ X i ≫ δ X (Fin.succ i) = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
rw [δ_comp_σ_succ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : Fin.castSucc j < i
⊢ σ X (Fin.castSucc j) ≫ δ X (Fin.succ i) = δ X i ≫ σ X j
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : Fin.castSucc j < i
⊢ X.map (SimplexCategory.σ (Fin.castSucc j)).op ≫ X.map (SimplexCategory.δ (Fin.succ i)).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
hi : i = 0
⊢ False
[PROOFSTEP]
simp only [Fin.not_lt_zero, hi] at H 
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ σ X j ≫ δ X i = δ X (Fin.pred i (_ : i = 0 → False)) ≫ σ X (Fin.castLT j (_ : ↑j < n + 1))
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (Fin.pred i (_ : i = 0 → False))).op ≫
      X.map (SimplexCategory.σ (Fin.castLT j (_ : ↑j < n + 1))).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ X j ≫ σ X (Fin.castSucc i) = σ X i ≫ σ X (Fin.succ j)
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.σ (Fin.castSucc i)).op =
    X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.σ (Fin.succ j)).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.σ_comp_σ H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
⊢ Category.{?u.68325, max u v} (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
⊢ Category.{?u.68325, max u v} ((SimplexCategory.Truncated n)ᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J ((SimplexCategory.Truncated n)ᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J ((SimplexCategory.Truncated n)ᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
⊢ Category.{?u.76503, max u v} (Augmented C)
[PROOFSTEP]
dsimp only [Augmented]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
⊢ Category.{?u.76503, max u v} (Comma (𝟭 (SimplicialObject C)) (const C))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (𝟭 C).map (NatTrans.app (drop.map η) (op [0])) ≫
      ((fun X => { left := (drop.obj X).obj (op [0]), right := point.obj X, hom := NatTrans.app X.hom (op [0]) })
          Y✝).hom =
    ((fun X => { left := (drop.obj X).obj (op [0]), right := point.obj X, hom := NatTrans.app X.hom (op [0]) })
          X✝).hom ≫
      (𝟭 C).map (point.map η)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ NatTrans.app η.left (op [0]) ≫ NatTrans.app Y✝.hom (op [0]) = NatTrans.app X✝.hom (op [0]) ≫ η.right
[PROOFSTEP]
rw [← NatTrans.comp_app]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ NatTrans.app (η.left ≫ Y✝.hom) (op [0]) = NatTrans.app X✝.hom (op [0]) ≫ η.right
[PROOFSTEP]
erw [η.w]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ NatTrans.app (X✝.hom ≫ (const C).map η.right) (op [0]) = NatTrans.app X✝.hom (op [0]) ≫ η.right
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ : SimplicialObject C
X Y : Augmented C
f : X ⟶ Y
⊢ NatTrans.app (drop.map f) (op [0]) ≫ NatTrans.app Y.hom (op [0]) = NatTrans.app X.hom (op [0]) ≫ point.map f
[PROOFSTEP]
convert congr_app f.w (op (SimplexCategory.mk 0))
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{?u.105136, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (𝟭 (SimplicialObject D)).map (whiskerRight η.left F) ≫
      ((fun X =>
            { left := ((whiskering C D).obj F).obj (drop.obj X), right := F.obj (point.obj X),
              hom := whiskerRight X.hom F ≫ (Functor.constComp SimplexCategoryᵒᵖ X.right F).hom })
          Y✝).hom =
    ((fun X =>
            { left := ((whiskering C D).obj F).obj (drop.obj X), right := F.obj (point.obj X),
              hom := whiskerRight X.hom F ≫ (Functor.constComp SimplexCategoryᵒᵖ X.right F).hom })
          X✝).hom ≫
      (const D).map (F.map η.right)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{?u.105136, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategoryᵒᵖ
⊢ NatTrans.app
      ((𝟭 (SimplicialObject D)).map (whiskerRight η.left F) ≫
        ((fun X =>
              { left := ((whiskering C D).obj F).obj (drop.obj X), right := F.obj (point.obj X),
                hom := whiskerRight X.hom F ≫ (Functor.constComp SimplexCategoryᵒᵖ X.right F).hom })
            Y✝).hom)
      n✝ =
    NatTrans.app
      (((fun X =>
              { left := ((whiskering C D).obj F).obj (drop.obj X), right := F.obj (point.obj X),
                hom := whiskerRight X.hom F ≫ (Functor.constComp SimplexCategoryᵒᵖ X.right F).hom })
            X✝).hom ≫
        (const D).map (F.map η.right))
      n✝
[PROOFSTEP]
dsimp [whiskerRight]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{?u.105136, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategoryᵒᵖ
⊢ F.map (NatTrans.app η.left n✝) ≫ F.map (NatTrans.app Y✝.hom n✝) ≫ 𝟙 (F.obj Y✝.right) =
    (F.map (NatTrans.app X✝.hom n✝) ≫ 𝟙 (F.obj X✝.right)) ≫ F.map η.right
[PROOFSTEP]
simp only [Category.comp_id, ← F.map_comp, ← NatTrans.comp_app]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{?u.105136, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategoryᵒᵖ
⊢ F.map (NatTrans.app (η.left ≫ Y✝.hom) n✝) = F.map (NatTrans.app X✝.hom n✝ ≫ η.right)
[PROOFSTEP]
erw [η.w]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{?u.105136, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategoryᵒᵖ
⊢ F.map (NatTrans.app (X✝.hom ≫ (const C).map η.right) n✝) = F.map (NatTrans.app X✝.hom n✝ ≫ η.right)
[PROOFSTEP]
rfl
[GOAL]
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
⊢ (𝟭 (SimplicialObject D)).map (whiskerLeft (drop.obj A) η) ≫ ((whiskeringObj C D Y✝).obj A).hom =
    ((whiskeringObj C D X✝).obj A).hom ≫ (const D).map (NatTrans.app η (point.obj A))
[PROOFSTEP]
ext n
[GOAL]
case h
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ᵒᵖ
⊢ NatTrans.app ((𝟭 (SimplicialObject D)).map (whiskerLeft (drop.obj A) η) ≫ ((whiskeringObj C D Y✝).obj A).hom) n =
    NatTrans.app (((whiskeringObj C D X✝).obj A).hom ≫ (const D).map (NatTrans.app η (point.obj A))) n
[PROOFSTEP]
dsimp
[GOAL]
case h
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ᵒᵖ
⊢ NatTrans.app η (A.left.obj n) ≫ Y✝.map (NatTrans.app A.hom n) ≫ 𝟙 (Y✝.obj A.right) =
    (X✝.map (NatTrans.app A.hom n) ≫ 𝟙 (X✝.obj A.right)) ≫ NatTrans.app η A.right
[PROOFSTEP]
rw [Category.comp_id, Category.comp_id, η.naturality]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { obj := whiskeringObj C D,
          map := fun {X Y} η =>
            NatTrans.mk fun A => CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
      (x✝¹ ≫ x✝) =
    { obj := whiskeringObj C D,
            map := fun {X Y} η =>
              NatTrans.mk fun A => CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
        x✝¹ ≫
      { obj := whiskeringObj C D,
            map := fun {X Y} η =>
              NatTrans.mk fun A => CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
        x✝
[PROOFSTEP]
ext
[GOAL]
case w.h.h₁.h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Augmented C
n✝ : SimplexCategoryᵒᵖ
⊢ NatTrans.app
      (NatTrans.app
          ({ obj := whiskeringObj C D,
                map := fun {X Y} η =>
                  NatTrans.mk fun A =>
                    CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
            (x✝² ≫ x✝¹))
          x✝).left
      n✝ =
    NatTrans.app
      (NatTrans.app
          ({ obj := whiskeringObj C D,
                  map := fun {X Y} η =>
                    NatTrans.mk fun A =>
                      CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
              x✝² ≫
            { obj := whiskeringObj C D,
                  map := fun {X Y} η =>
                    NatTrans.mk fun A =>
                      CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
              x✝¹)
          x✝).left
      n✝
[PROOFSTEP]
rfl
[GOAL]
case w.h.h₂
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Augmented C
⊢ (NatTrans.app
        ({ obj := whiskeringObj C D,
              map := fun {X Y} η =>
                NatTrans.mk fun A => CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
          (x✝² ≫ x✝¹))
        x✝).right =
    (NatTrans.app
        ({ obj := whiskeringObj C D,
                map := fun {X Y} η =>
                  NatTrans.mk fun A =>
                    CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
            x✝² ≫
          { obj := whiskeringObj C D,
                map := fun {X Y} η =>
                  NatTrans.mk fun A =>
                    CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
            x✝¹)
        x✝).right
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [0]) ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
⊢ ∀ ⦃X_1 Y : SimplexCategoryᵒᵖ⦄ (f_1 : X_1 ⟶ Y),
    ((𝟭 (SimplicialObject C)).obj X).map f_1 ≫ (fun i => X.map (SimplexCategory.const i.unop 0).op ≫ f) Y =
      (fun i => X.map (SimplexCategory.const i.unop 0).op ≫ f) X_1 ≫ ((const C).obj X₀).map f_1
[PROOFSTEP]
intro i j g
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [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 ≫ (fun i => X.map (SimplexCategory.const i.unop 0).op ≫ f) j =
    (fun i => X.map (SimplexCategory.const i.unop 0).op ≫ f) i ≫ ((const C).obj X₀).map g
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [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 (SimplexCategory.const j.unop 0).op ≫ f = (X.map (SimplexCategory.const i.unop 0).op ≫ f) ≫ 𝟙 X₀
[PROOFSTEP]
rw [← g.op_unop]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [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 (SimplexCategory.const j.unop 0).op ≫ f =
    (X.map (SimplexCategory.const i.unop 0).op ≫ f) ≫ 𝟙 X₀
[PROOFSTEP]
simpa only [← X.map_comp, ← Category.assoc, Category.comp_id, ← op_comp] using w _ _ _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [0]) ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
⊢ NatTrans.app (augment X X₀ f w).hom (op [0]) = f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [0]) ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
⊢ X.map (SimplexCategory.const [0] 0).op ≫ f = f
[PROOFSTEP]
rw [SimplexCategory.hom_zero_zero ([0].const 0), op_id, X.map_id, Category.id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ Category.{?u.208707, max u v} (CosimplicialObject C)
[PROOFSTEP]
dsimp only [CosimplicialObject]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ Category.{?u.208707, max u v} (SimplexCategory ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (CosimplicialObject C)
[PROOFSTEP]
dsimp [CosimplicialObject]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplexCategory ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (CosimplicialObject C)
[PROOFSTEP]
dsimp [CosimplicialObject]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplexCategory ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), NatTrans.app f n = NatTrans.app g n
⊢ f.app = g.app
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), NatTrans.app f n = NatTrans.app g n
x✝ : SimplexCategory
⊢ NatTrans.app f x✝ = NatTrans.app g x✝
[PROOFSTEP]
apply h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n m : ℕ
h : n = m
⊢ [n] = [m]
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
h : n = n
⊢ eqToIso X h = Iso.refl (X.obj [n])
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
h : n = n
⊢ (eqToIso X h).hom = (Iso.refl (X.obj [n])).hom
[PROOFSTEP]
simp [eqToIso]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ X i ≫ δ X (Fin.succ j) = δ X j ≫ δ X (Fin.castSucc i)
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ (Fin.succ j)) =
    X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ (Fin.castSucc i))
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_δ H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
hj : j = 0
⊢ False
[PROOFSTEP]
simp only [hj, Fin.not_lt_zero] at H 
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
⊢ δ X i ≫ δ X j = δ X (Fin.pred j (_ : j = 0 → False)) ≫ δ X (Fin.castSucc i)
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j) =
    X.map (SimplexCategory.δ (Fin.pred j (_ : j = 0 → False))) ≫ X.map (SimplexCategory.δ (Fin.castSucc i))
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ Fin.castSucc j
⊢ δ X (Fin.castLT i (_ : ↑i < n + 2)) ≫ δ X (Fin.succ j) = δ X j ≫ δ X i
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ Fin.castSucc j
⊢ X.map (SimplexCategory.δ (Fin.castLT i (_ : ↑i < n + 2))) ≫ X.map (SimplexCategory.δ (Fin.succ j)) =
    X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i)
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ'' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ δ X i ≫ δ X (Fin.castSucc i) = δ X i ≫ δ X (Fin.succ i)
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ (Fin.castSucc i)) =
    X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ (Fin.succ i))
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_δ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = Fin.castSucc i
⊢ δ X i ≫ δ X j = δ X i ≫ δ X (Fin.succ i)
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ δ X i ≫ δ X (Fin.castSucc i) = δ X i ≫ δ X (Fin.succ i)
[PROOFSTEP]
rw [δ_comp_δ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ Fin.castSucc j
⊢ δ X (Fin.castSucc i) ≫ σ X (Fin.succ j) = σ X j ≫ δ X i
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ Fin.castSucc j
⊢ X.map (SimplexCategory.δ (Fin.castSucc i)) ≫ X.map (SimplexCategory.σ (Fin.succ j)) =
    X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_of_le H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ δ X (Fin.castSucc i) ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.δ (Fin.castSucc i)) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X.obj [n])
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_self, X.map_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = Fin.castSucc i
⊢ δ X j ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ δ X (Fin.castSucc i) ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
rw [δ_comp_σ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ δ X (Fin.succ i) ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.δ (Fin.succ i)) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X.obj [n])
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_succ, X.map_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = Fin.succ i
⊢ δ X j ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ δ X (Fin.succ i) ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
rw [δ_comp_σ_succ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : Fin.castSucc j < i
⊢ δ X (Fin.succ i) ≫ σ X (Fin.castSucc j) = σ X j ≫ δ X i
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : Fin.castSucc j < i
⊢ X.map (SimplexCategory.δ (Fin.succ i)) ≫ X.map (SimplexCategory.σ (Fin.castSucc j)) =
    X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_of_gt H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
hi : i = 0
⊢ False
[PROOFSTEP]
simp only [Fin.not_lt_zero, hi] at H 
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ δ X i ≫ σ X j = σ X (Fin.castLT j (_ : ↑j < n + 1)) ≫ δ X (Fin.pred i (_ : i = 0 → False))
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ (Fin.castLT j (_ : ↑j < n + 1))) ≫
      X.map (SimplexCategory.δ (Fin.pred i (_ : i = 0 → False)))
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ X (Fin.castSucc i) ≫ σ X j = σ X (Fin.succ j) ≫ σ X i
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ (Fin.castSucc i)) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ (Fin.succ j)) ≫ X.map (SimplexCategory.σ i)
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.σ_comp_σ H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
⊢ Category.{?u.295628, max u v} (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
⊢ Category.{?u.295628, max u v} (SimplexCategory.Truncated n ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplexCategory.Truncated n ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplexCategory.Truncated n ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
⊢ Category.{?u.303800, max u v} (Augmented C)
[PROOFSTEP]
dsimp only [Augmented]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
⊢ Category.{?u.303800, max u v} (Comma (const C) (𝟭 (CosimplicialObject C)))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (𝟭 C).map (point.map η) ≫
      ((fun X => { left := point.obj X, right := (drop.obj X).obj [0], hom := NatTrans.app X.hom [0] }) Y✝).hom =
    ((fun X => { left := point.obj X, right := (drop.obj X).obj [0], hom := NatTrans.app X.hom [0] }) X✝).hom ≫
      (𝟭 C).map (NatTrans.app (drop.map η) [0])
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ η.left ≫ NatTrans.app Y✝.hom [0] = NatTrans.app X✝.hom [0] ≫ NatTrans.app η.right [0]
[PROOFSTEP]
rw [← NatTrans.comp_app]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ η.left ≫ NatTrans.app Y✝.hom [0] = NatTrans.app (X✝.hom ≫ η.right) [0]
[PROOFSTEP]
erw [← η.w]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ η.left ≫ NatTrans.app Y✝.hom [0] = NatTrans.app ((const C).map η.left ≫ Y✝.hom) [0]
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{?u.334362, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (const D).map (F.map η.left) ≫
      ((fun X =>
            { left := F.obj (point.obj X), right := ((whiskering C D).obj F).obj (drop.obj X),
              hom := (Functor.constComp SimplexCategory (point.obj X) F).inv ≫ whiskerRight X.hom F })
          Y✝).hom =
    ((fun X =>
            { left := F.obj (point.obj X), right := ((whiskering C D).obj F).obj (drop.obj X),
              hom := (Functor.constComp SimplexCategory (point.obj X) F).inv ≫ whiskerRight X.hom F })
          X✝).hom ≫
      (𝟭 (CosimplicialObject D)).map (whiskerRight η.right F)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{?u.334362, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategory
⊢ NatTrans.app
      ((const D).map (F.map η.left) ≫
        ((fun X =>
              { left := F.obj (point.obj X), right := ((whiskering C D).obj F).obj (drop.obj X),
                hom := (Functor.constComp SimplexCategory (point.obj X) F).inv ≫ whiskerRight X.hom F })
            Y✝).hom)
      n✝ =
    NatTrans.app
      (((fun X =>
              { left := F.obj (point.obj X), right := ((whiskering C D).obj F).obj (drop.obj X),
                hom := (Functor.constComp SimplexCategory (point.obj X) F).inv ≫ whiskerRight X.hom F })
            X✝).hom ≫
        (𝟭 (CosimplicialObject D)).map (whiskerRight η.right F))
      n✝
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{?u.334362, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategory
⊢ F.map η.left ≫ 𝟙 (F.obj Y✝.left) ≫ F.map (NatTrans.app Y✝.hom n✝) =
    (𝟙 (F.obj X✝.left) ≫ F.map (NatTrans.app X✝.hom n✝)) ≫ F.map (NatTrans.app η.right n✝)
[PROOFSTEP]
rw [Category.id_comp, Category.id_comp, ← F.map_comp, ← F.map_comp, ← NatTrans.comp_app]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{?u.334362, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategory
⊢ F.map (η.left ≫ NatTrans.app Y✝.hom n✝) = F.map (NatTrans.app (X✝.hom ≫ η.right) n✝)
[PROOFSTEP]
erw [← η.w]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{?u.334362, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategory
⊢ F.map (η.left ≫ NatTrans.app Y✝.hom n✝) = F.map (NatTrans.app ((const C).map η.left ≫ Y✝.hom) n✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
⊢ (const D).map (NatTrans.app η (point.obj A)) ≫ ((whiskeringObj C D Y✝).obj A).hom =
    ((whiskeringObj C D X✝).obj A).hom ≫ (𝟭 (CosimplicialObject D)).map (whiskerLeft (drop.obj A) η)
[PROOFSTEP]
ext n
[GOAL]
case h
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
⊢ NatTrans.app ((const D).map (NatTrans.app η (point.obj A)) ≫ ((whiskeringObj C D Y✝).obj A).hom) n =
    NatTrans.app (((whiskeringObj C D X✝).obj A).hom ≫ (𝟭 (CosimplicialObject D)).map (whiskerLeft (drop.obj A) η)) n
[PROOFSTEP]
dsimp
[GOAL]
case h
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
⊢ NatTrans.app η A.left ≫ 𝟙 (Y✝.obj A.left) ≫ Y✝.map (NatTrans.app A.hom n) =
    (𝟙 (X✝.obj A.left) ≫ X✝.map (NatTrans.app A.hom n)) ≫ NatTrans.app η (A.right.obj n)
[PROOFSTEP]
rw [Category.id_comp, Category.id_comp, η.naturality]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ (whiskeringObj C D X✝).map f ≫
      (fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝ =
    (fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝¹ ≫
      (whiskeringObj C D Y✝).map f
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ ((whiskeringObj C D X✝).map f ≫
        (fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝).left =
    ((fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝¹ ≫
        (whiskeringObj C D Y✝).map f).left
[PROOFSTEP]
dsimp
[GOAL]
case h₂.h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
n✝ : SimplexCategory
⊢ NatTrans.app
      ((whiskeringObj C D X✝).map f ≫
          (fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝).right
      n✝ =
    NatTrans.app
      ((fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝¹ ≫
          (whiskeringObj C D Y✝).map f).right
      n✝
[PROOFSTEP]
dsimp
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ X✝.map f.left ≫ NatTrans.app η x✝.left = NatTrans.app η x✝¹.left ≫ Y✝.map f.left
[PROOFSTEP]
simp
[GOAL]
case h₂.h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
n✝ : SimplexCategory
⊢ X✝.map (NatTrans.app f.right n✝) ≫ NatTrans.app η (x✝.right.obj n✝) =
    NatTrans.app η (x✝¹.right.obj n✝) ≫ Y✝.map (NatTrans.app f.right n✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [0]
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ ∀ ⦃X_1 Y : SimplexCategory⦄ (f_1 : X_1 ⟶ Y),
    ((const C).obj X₀).map f_1 ≫ (fun i => f ≫ X.map (SimplexCategory.const i 0)) Y =
      (fun i => f ≫ X.map (SimplexCategory.const i 0)) X_1 ≫ ((𝟭 (CosimplicialObject C)).obj X).map f_1
[PROOFSTEP]
intro i j g
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [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 ≫ (fun i => f ≫ X.map (SimplexCategory.const i 0)) j =
    (fun i => f ≫ X.map (SimplexCategory.const i 0)) i ≫ ((𝟭 (CosimplicialObject C)).obj X).map g
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [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 (SimplexCategory.const j 0) = (f ≫ X.map (SimplexCategory.const i 0)) ≫ X.map g
[PROOFSTEP]
simpa [← X.map_comp] using w _ _ _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [0]
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ NatTrans.app (augment X X₀ f w).hom [0] = f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [0]
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ f ≫ X.map (SimplexCategory.const [0] 0) = f
[PROOFSTEP]
rw [SimplexCategory.hom_zero_zero ([0].const 0), X.map_id, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Augmented C
⊢ (CosimplicialObject.Augmented.leftOp (rightOp X)).right = X.right
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Augmented Cᵒᵖ
⊢ (SimplicialObject.Augmented.rightOp (leftOp X)).left = X.left
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (CosimplicialObject.const Cᵒᵖ).map f.unop.right.op ≫ ((fun X => SimplicialObject.Augmented.rightOp X.unop) Y✝).hom =
    ((fun X => SimplicialObject.Augmented.rightOp X.unop) X✝).hom ≫
      (𝟭 (CosimplicialObject Cᵒᵖ)).map (NatTrans.rightOp f.unop.left)
[PROOFSTEP]
ext x
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ NatTrans.app
      ((CosimplicialObject.const Cᵒᵖ).map f.unop.right.op ≫
        ((fun X => SimplicialObject.Augmented.rightOp X.unop) Y✝).hom)
      x =
    NatTrans.app
      (((fun X => SimplicialObject.Augmented.rightOp X.unop) X✝).hom ≫
        (𝟭 (CosimplicialObject Cᵒᵖ)).map (NatTrans.rightOp f.unop.left))
      x
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ f.unop.right.op ≫ (NatTrans.app Y✝.unop.hom (op x)).op =
    (NatTrans.app X✝.unop.hom (op x)).op ≫ (NatTrans.app f.unop.left (op x)).op
[PROOFSTEP]
simp_rw [← op_comp]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ (NatTrans.app Y✝.unop.hom (op x) ≫ f.unop.right).op =
    (NatTrans.app f.unop.left (op x) ≫ NatTrans.app X✝.unop.hom (op x)).op
[PROOFSTEP]
congr 1
[GOAL]
case h.e_f
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ NatTrans.app Y✝.unop.hom (op x) ≫ f.unop.right = NatTrans.app f.unop.left (op x) ≫ NatTrans.app X✝.unop.hom (op x)
[PROOFSTEP]
exact (congr_app f.unop.w (op x)).symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (𝟭 (SimplicialObject C)).map (NatTrans.leftOp f.right) ≫ (CosimplicialObject.Augmented.leftOp X✝).hom =
    (CosimplicialObject.Augmented.leftOp Y✝).hom ≫ (SimplicialObject.const C).map f.left.unop
[PROOFSTEP]
ext x
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ NatTrans.app ((𝟭 (SimplicialObject C)).map (NatTrans.leftOp f.right) ≫ (CosimplicialObject.Augmented.leftOp X✝).hom)
      x =
    NatTrans.app ((CosimplicialObject.Augmented.leftOp Y✝).hom ≫ (SimplicialObject.const C).map f.left.unop) x
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ (NatTrans.app f.right x.unop).unop ≫ (NatTrans.app X✝.hom x.unop).unop =
    (NatTrans.app Y✝.hom x.unop).unop ≫ f.left.unop
[PROOFSTEP]
simp_rw [← unop_comp]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ (NatTrans.app X✝.hom x.unop ≫ NatTrans.app f.right x.unop).unop = (f.left ≫ NatTrans.app Y✝.hom x.unop).unop
[PROOFSTEP]
congr 1
[GOAL]
case h.e_f
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ NatTrans.app X✝.hom x.unop ≫ NatTrans.app f.right x.unop = f.left ≫ NatTrans.app Y✝.hom x.unop
[PROOFSTEP]
exact (congr_app f.w (unop x)).symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (𝟭 (SimplicialObject.Augmented C)ᵒᵖ).map f ≫
      ((fun X => Iso.op (SimplicialObject.Augmented.rightOpLeftOpIso X.unop)) Y✝).hom =
    ((fun X => Iso.op (SimplicialObject.Augmented.rightOpLeftOpIso X.unop)) X✝).hom ≫
      (simplicialToCosimplicialAugmented C ⋙ cosimplicialToSimplicialAugmented C).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ f ≫ (SimplicialObject.Augmented.rightOpLeftOpIso Y✝.unop).hom.op =
    (SimplicialObject.Augmented.rightOpLeftOpIso X✝.unop).hom.op ≫
      (CommaMorphism.mk (NatTrans.leftOp (NatTrans.rightOp f.unop.left)) f.unop.right).op
[PROOFSTEP]
rw [← f.op_unop]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop.op ≫ (SimplicialObject.Augmented.rightOpLeftOpIso Y✝.unop).hom.op =
    (SimplicialObject.Augmented.rightOpLeftOpIso X✝.unop).hom.op ≫
      (CommaMorphism.mk (NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left)) f.unop.op.unop.right).op
[PROOFSTEP]
simp_rw [← op_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((SimplicialObject.Augmented.rightOpLeftOpIso Y✝.unop).hom ≫ f.unop).op =
    (CommaMorphism.mk (NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left)) f.unop.op.unop.right ≫
        (SimplicialObject.Augmented.rightOpLeftOpIso X✝.unop).hom).op
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (SimplicialObject.Augmented.rightOpLeftOpIso Y✝.unop).hom ≫ f.unop =
    CommaMorphism.mk (NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left)) f.unop.op.unop.right ≫
      (SimplicialObject.Augmented.rightOpLeftOpIso X✝.unop).hom
[PROOFSTEP]
aesop_cat
