awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : SimplexCategory
h :
  F.map η.left ≫ 𝟙 (F.obj Y.left) ≫ F.map (Y.hom.app n) =
    (𝟙 (F.obj X_1.left) ≫ F.map (X_1.hom.app n)) ≫ F.map (η.right.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).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

Tactic:
dsimp
-- 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
n : SimplexCategory
h : F.map (η.left ≫ Y.hom.app n) = F.map (X_1.hom.app n ≫ η.right.app n)
⊢ F.map η.left ≫ 𝟙 (F.obj Y.left) ≫ F.map (Y.hom.app n) =
    (𝟙 (F.obj X_1.left) ≫ F.map (X_1.hom.app n)) ≫ F.map (η.right.app n)

Tactic:
rw [Category.id_comp, Category.id_comp, ← F.map_comp, ← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- 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
n : SimplexCategory
⊢ F.map (η.left ≫ Y.hom.app n) = F.map (X_1.hom.app n ≫ η.right.app n)

Tactic:
simp [w_app, map_comp]

Premises used: CategoryTheory.CosimplicialObject.Augmented.w_app, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
h :
  ∀ (n : SimplexCategory),
    (map (const D) (η.app (obj point A)) ≫ ((whiskeringObj C D Y).obj A).hom).app n =
      (((whiskeringObj C D X_1).obj A).hom ≫ map (𝟭 (CosimplicialObject.{v', u'} D)) (whiskerLeft (obj drop A) η)).app n
⊢ map (const D) (η.app (obj point A)) ≫ ((whiskeringObj C D Y).obj A).hom =
    ((whiskeringObj C D X_1).obj A).hom ≫ map (𝟭 (CosimplicialObject.{v', u'} D)) (whiskerLeft (obj drop A) η)

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
n : SimplexCategory
h :
  η.app A.left ≫ 𝟙 (Y.obj A.left) ≫ Y.map (A.hom.app n) =
    (𝟙 (X_1.obj A.left) ≫ X_1.map (A.hom.app n)) ≫ η.app (A.right.obj n)
⊢ (map (const D) (η.app (obj point A)) ≫ ((whiskeringObj C D Y).obj A).hom).app n =
    (((whiskeringObj C D X_1).obj A).hom ≫ map (𝟭 (CosimplicialObject.{v', u'} D)) (whiskerLeft (obj drop A) η)).app n

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
n : SimplexCategory
h : η.app A.left ≫ Y.map (A.hom.app n) = (𝟙 (X_1.obj A.left) ≫ X_1.map (A.hom.app n)) ≫ η.app (A.right.obj n)
h₁ : η.app A.left ≫ Y.map (A.hom.app n) = X_1.map (A.hom.app n) ≫ η.app (A.right.obj n)
h₂ h₃ : η.app A.left ≫ Y.map (A.hom.app n) = η.app A.left ≫ Y.map (A.hom.app n)
⊢ η.app A.left ≫ 𝟙 (Y.obj A.left) ≫ Y.map (A.hom.app n) =
    (𝟙 (X_1.obj A.left) ≫ X_1.map (A.hom.app n)) ≫ η.app (A.right.obj n)

Tactic:
rw [Category.id_comp, Category.id_comp, η.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
x x_1 : Augmented.{v, u} C
f : x ⟶ x_1
h₁ :
  CommaMorphism.left
      ((whiskeringObj C D X_1).map f ≫
        { left := η.app (obj point x_1), right := whiskerLeft (obj drop x_1) η, w := ⋯ }) =
    CommaMorphism.left
      ({ left := η.app (obj point x), right := whiskerLeft (obj drop x) η, w := ⋯ :
          CommaMorphism ((whiskeringObj C D X_1).obj x) ((whiskeringObj C D Y).obj x) } ≫
        (whiskeringObj C D Y).map f)
h₂ :
  ∀ (n : SimplexCategory),
    NatTrans.app
        (CommaMorphism.right
          ((whiskeringObj C D X_1).map f ≫
            { left := η.app (obj point x_1), right := whiskerLeft (obj drop x_1) η, w := ⋯ }))
        n =
      NatTrans.app
        (CommaMorphism.right
          ({ left := η.app (obj point x), right := whiskerLeft (obj drop x) η, w := ⋯ :
              CommaMorphism ((whiskeringObj C D X_1).obj x) ((whiskeringObj C D Y).obj x) } ≫
            (whiskeringObj C D Y).map f))
        n
⊢ (whiskeringObj C D X_1).map f ≫ { left := η.app (obj point x_1), right := whiskerLeft (obj drop x_1) η, w := ⋯ } =
    { left := η.app (obj point x), right := whiskerLeft (obj drop x) η, w := ⋯ :
        CommaMorphism ((whiskeringObj C D X_1).obj x) ((whiskeringObj C D Y).obj x) } ≫
      (whiskeringObj C D Y).map f

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
x x_1 : Augmented.{v, u} C
f : x ⟶ x_1
⊢ CommaMorphism.left
      ((whiskeringObj C D X_1).map f ≫
        { left := η.app (obj point x_1), right := whiskerLeft (obj drop x_1) η, w := ⋯ }) =
    CommaMorphism.left
      ({ left := η.app (obj point x), right := whiskerLeft (obj drop x) η, w := ⋯ :
          CommaMorphism ((whiskeringObj C D X_1).obj x) ((whiskeringObj C D Y).obj x) } ≫
        (whiskeringObj C D Y).map f)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
x x_1 : Augmented.{v, u} C
f : x ⟶ x_1
n : SimplexCategory
⊢ NatTrans.app
      (CommaMorphism.right
        ((whiskeringObj C D X_1).map f ≫
          { left := η.app (obj point x_1), right := whiskerLeft (obj drop x_1) η, w := ⋯ }))
      n =
    NatTrans.app
      (CommaMorphism.right
        ({ left := η.app (obj point x), right := whiskerLeft (obj drop x) η, w := ⋯ :
            CommaMorphism ((whiskeringObj C D X_1).obj x) ((whiskeringObj C D Y).obj x) } ≫
          (whiskeringObj C D Y).map f))
      n

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X_1 X : CosimplicialObject.{v, u} C
X₀ : C
f : X₀ ⟶ X ^⦋0⦌
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
i j : SimplexCategory
g : i ⟶ j
dsimp : 𝟙 X₀ ≫ f ≫ X.map (⦋0⦌.const j 0) = (f ≫ X.map (⦋0⦌.const i 0)) ≫ X.map g
⊢ map (obj (const C) X₀) g ≫ f ≫ X.map (⦋0⦌.const j 0) =
    (f ≫ X.map (⦋0⦌.const i 0)) ≫ (obj (𝟭 (CosimplicialObject.{v, u} C)) X).map g

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X_1 X : CosimplicialObject.{v, u} C
X₀ : C
f : X₀ ⟶ X ^⦋0⦌
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
i j : SimplexCategory
g : i ⟶ j
rw : f ≫ X.map (⦋0⦌.const j 0) = (f ≫ X.map (⦋0⦌.const i 0)) ≫ X.map g
rw₁ : f ≫ X.map (⦋0⦌.const j 0) = f ≫ X.map (⦋0⦌.const i 0) ≫ X.map g
rw₂ : f ≫ X.map (⦋0⦌.const j 0) = f ≫ X.map (⦋0⦌.const i 0 ≫ g)
rw₃ : f ≫ X.map (⦋0⦌.const i 0 ≫ g) = f ≫ X.map (⦋0⦌.const i 0 ≫ g)
g₂ : ⦋0⦌ ⟶ j
rw₄ : f ≫ X.map (⦋0⦌.const i 0 ≫ g) = f ≫ X.map (⦋0⦌.const i 0 ≫ g)
g₃ : ⦋0⦌ ⟶ j
⊢ 𝟙 X₀ ≫ f ≫ X.map (⦋0⦌.const j 0) = (f ≫ X.map (⦋0⦌.const i 0)) ≫ X.map g

Tactic:
rw [Category.id_comp, Category.assoc, ← X.map_comp, w]

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

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : Augmented.{v, u} C
⊢ X.rightOp.leftOp.right = X.right

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : Augmented.{v, u} Cᵒᵖ
⊢ X.leftOp.rightOp.left = X.left

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
h :
  ∀ (x : SimplexCategory),
    NatTrans.app (map (CosimplicialObject.const Cᵒᵖ) f.unop.right.op ≫ (unop Y).rightOp.hom) x =
      ((unop X).rightOp.hom ≫ map (𝟭 (CosimplicialObject.{v, u} Cᵒᵖ)) (NatTrans.rightOp f.unop.left)).app x
⊢ map (CosimplicialObject.const Cᵒᵖ) f.unop.right.op ≫ (unop Y).rightOp.hom =
    (unop X).rightOp.hom ≫ map (𝟭 (CosimplicialObject.{v, u} Cᵒᵖ)) (NatTrans.rightOp f.unop.left)

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
x : SimplexCategory
h :
  Eq.{v + 1} (α := op (unop X).right ⟶ op ((unop Y).left.obj (op x)))
    (f.unop.right.op ≫ Quiver.Hom.op ((unop Y).hom.app (op x)))
    (Quiver.Hom.op ((unop X).hom.app (op x)) ≫ Quiver.Hom.op (f.unop.left.app (op x)))
⊢ NatTrans.app (map (CosimplicialObject.const Cᵒᵖ) f.unop.right.op ≫ (unop Y).rightOp.hom) x =
    ((unop X).rightOp.hom ≫ map (𝟭 (CosimplicialObject.{v, u} Cᵒᵖ)) (NatTrans.rightOp f.unop.left)).app x

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
x : SimplexCategory
h :
  Eq (α := op (unop X).right ⟶ op ((unop Y).left.obj (op x))) (Quiver.Hom.op ((unop Y).hom.app (op x) ≫ f.unop.right))
    (Quiver.Hom.op (f.unop.left.app (op x) ≫ (unop X).hom.app (op x)))
⊢ Eq.{v + 1} (α := op (unop X).right ⟶ op ((unop Y).left.obj (op x)))
    (f.unop.right.op ≫ Quiver.Hom.op ((unop Y).hom.app (op x)))
    (Quiver.Hom.op ((unop X).hom.app (op x)) ≫ Quiver.Hom.op (f.unop.left.app (op x)))

Tactic:
simp_rw [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
x : SimplexCategory
h :
  Eq (α := (unop Y).left.obj (op x) ⟶ (unop X).right) ((unop Y).hom.app (op x) ≫ f.unop.right)
    (f.unop.left.app (op x) ≫ (unop X).hom.app (op x))
⊢ Eq (α := op (unop X).right ⟶ op ((unop Y).left.obj (op x))) (Quiver.Hom.op ((unop Y).hom.app (op x) ≫ f.unop.right))
    (Quiver.Hom.op (f.unop.left.app (op x) ≫ (unop X).hom.app (op x)))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
x : SimplexCategory
⊢ Eq (α := (unop Y).left.obj (op x) ⟶ (unop X).right) ((unop Y).hom.app (op x) ≫ f.unop.right)
    (f.unop.left.app (op x) ≫ (unop X).hom.app (op x))

Tactic:
(congr_app f.unop.w (op x)).symm

Premises used: Quiver.Hom.unop, CategoryTheory.CommaMorphism.w, Opposite.op, Eq.symm, CategoryTheory.congr_app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
x : SimplexCategory
⊢ Eq (α := (unop Y).left.obj (op x) ⟶ (unop X).right) ((unop Y).hom.app (op x) ≫ f.unop.right)
    (f.unop.left.app (op x) ≫ (unop X).hom.app (op x))

Tactic:
exact (congr_app f.unop.w (op x)).symm

Premises used: Quiver.Hom.unop, CategoryTheory.CommaMorphism.w, Opposite.op, Eq.symm, CategoryTheory.congr_app
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : CosimplicialObject.Augmented.{v, u} Cᵒᵖ
f : X ⟶ Y
h :
  ∀ (x : SimplexCategoryᵒᵖ),
    (map (𝟭 (SimplicialObject.{v, u} C)) (NatTrans.leftOp f.right) ≫ X.leftOp.hom).app x =
      (Y.leftOp.hom ≫ map (SimplicialObject.const C) f.left.unop).app x
⊢ map (𝟭 (SimplicialObject.{v, u} C)) (NatTrans.leftOp f.right) ≫ X.leftOp.hom =
    Y.leftOp.hom ≫ map (SimplicialObject.const C) f.left.unop

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : CosimplicialObject.Augmented.{v, u} Cᵒᵖ
f : X ⟶ Y
x : SimplexCategoryᵒᵖ
h :
  Eq (α := unop (Y.right.obj (unop x)) ⟶ unop X.left)
    (Quiver.Hom.unop (f.right.app (unop x)) ≫ Quiver.Hom.unop (X.hom.app (unop x)))
    (Quiver.Hom.unop (Y.hom.app (unop x)) ≫ f.left.unop)
⊢ (map (𝟭 (SimplicialObject.{v, u} C)) (NatTrans.leftOp f.right) ≫ X.leftOp.hom).app x =
    (Y.leftOp.hom ≫ map (SimplicialObject.const C) f.left.unop).app x

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : CosimplicialObject.Augmented.{v, u} Cᵒᵖ
f : X ⟶ Y
x : SimplexCategoryᵒᵖ
h :
  Eq (α := unop (Y.right.obj (unop x)) ⟶ unop X.left) (Quiver.Hom.unop (X.hom.app (unop x) ≫ f.right.app (unop x)))
    (Quiver.Hom.unop (f.left ≫ Y.hom.app (unop x)))
⊢ Eq (α := unop (Y.right.obj (unop x)) ⟶ unop X.left)
    (Quiver.Hom.unop (f.right.app (unop x)) ≫ Quiver.Hom.unop (X.hom.app (unop x)))
    (Quiver.Hom.unop (Y.hom.app (unop x)) ≫ f.left.unop)

Tactic:
simp_rw [← unop_comp]

Premises used: CategoryTheory.unop_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : CosimplicialObject.Augmented.{v, u} Cᵒᵖ
f : X ⟶ Y
x : SimplexCategoryᵒᵖ
h : Eq (α := X.left ⟶ Y.right.obj (unop x)) (X.hom.app (unop x) ≫ f.right.app (unop x)) (f.left ≫ Y.hom.app (unop x))
⊢ Eq (α := unop (Y.right.obj (unop x)) ⟶ unop X.left) (Quiver.Hom.unop (X.hom.app (unop x) ≫ f.right.app (unop x)))
    (Quiver.Hom.unop (f.left ≫ Y.hom.app (unop x)))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : CosimplicialObject.Augmented.{v, u} Cᵒᵖ
f : X ⟶ Y
x : SimplexCategoryᵒᵖ
⊢ Eq (α := X.left ⟶ Y.right.obj (unop x)) (X.hom.app (unop x) ≫ f.right.app (unop x)) (f.left ≫ Y.hom.app (unop x))

Tactic:
(congr_app f.w (unop x)).symm

Premises used: CategoryTheory.CommaMorphism.w, Eq.symm, CategoryTheory.congr_app, Opposite.unop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : CosimplicialObject.Augmented.{v, u} Cᵒᵖ
f : X ⟶ Y
x : SimplexCategoryᵒᵖ
⊢ Eq (α := X.left ⟶ Y.right.obj (unop x)) (X.hom.app (unop x) ≫ f.right.app (unop x)) (f.left ≫ Y.hom.app (unop x))

Tactic:
exact (congr_app f.w (unop x)).symm

Premises used: CategoryTheory.CommaMorphism.w, Eq.symm, CategoryTheory.congr_app, Opposite.unop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
dsimp :
  f ≫ (unop Y).rightOpLeftOpIso.hom.op =
    (unop X).rightOpLeftOpIso.hom.op ≫
      Quiver.Hom.op { left := NatTrans.leftOp (NatTrans.rightOp f.unop.left), right := f.unop.right, w := ⋯ }
⊢ Eq (α :=
    obj (𝟭 (SimplicialObject.Augmented.{v, u} C)ᵒᵖ) X ⟶
      obj (simplicialToCosimplicialAugmented C ⋙ cosimplicialToSimplicialAugmented C) Y)
    (map (𝟭 (SimplicialObject.Augmented.{v, u} C)ᵒᵖ) f ≫
      Iso.hom ((fun (X : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ) ↦ (unop X).rightOpLeftOpIso.op) Y))
    (Iso.hom ((fun (X : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ) ↦ (unop X).rightOpLeftOpIso.op) X) ≫
      map (simplicialToCosimplicialAugmented C ⋙ cosimplicialToSimplicialAugmented C) f)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
rw :
  f.unop.op ≫ (unop Y).rightOpLeftOpIso.hom.op =
    (unop X).rightOpLeftOpIso.hom.op ≫
      Quiver.Hom.op
        { left := NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left), right := f.unop.op.unop.right, w := ⋯ }
⊢ f ≫ (unop Y).rightOpLeftOpIso.hom.op =
    (unop X).rightOpLeftOpIso.hom.op ≫
      Quiver.Hom.op { left := NatTrans.leftOp (NatTrans.rightOp f.unop.left), right := f.unop.right, w := ⋯ }

Tactic:
rw [← f.op_unop]

Premises used: Quiver.Hom.op_unop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
simp_rw :
  ((unop Y).rightOpLeftOpIso.hom ≫ f.unop).op =
    Quiver.Hom.op
      ({ left := NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left), right := f.unop.op.unop.right, w := ⋯ :
          CommaMorphism (unop Y).rightOp.leftOp (unop X).rightOp.leftOp } ≫
        (unop X).rightOpLeftOpIso.hom)
⊢ f.unop.op ≫ (unop Y).rightOpLeftOpIso.hom.op =
    (unop X).rightOpLeftOpIso.hom.op ≫
      Quiver.Hom.op
        { left := NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left), right := f.unop.op.unop.right, w := ⋯ }

Tactic:
simp_rw [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
e_f :
  (unop Y).rightOpLeftOpIso.hom ≫ f.unop =
    { left := NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left), right := f.unop.op.unop.right, w := ⋯ :
        CommaMorphism (unop Y).rightOp.leftOp (unop X).rightOp.leftOp } ≫
      (unop X).rightOpLeftOpIso.hom
⊢ ((unop Y).rightOpLeftOpIso.hom ≫ f.unop).op =
    Quiver.Hom.op
      ({ left := NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left), right := f.unop.op.unop.right, w := ⋯ :
          CommaMorphism (unop Y).rightOp.leftOp (unop X).rightOp.leftOp } ≫
        (unop X).rightOpLeftOpIso.hom)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
p q : ℕ
h : p + 1 = q
k : Fin (p + 1)
⊢ Y _⦋p + 1⦌ = Y _⦋q⦌

Tactic:
simp [h]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
p : ℕ
⊢ Eq (α := X _⦋p⦌ ⟶ Y _⦋p + 1⦌) (hom H p (p + 1)) (-∑ k : Fin (p + 1), HPow.hPow (α := ℤ) (-1) (↑k : ℕ) • H.h k)

Tactic:
simp [hom]

Premises used: CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
p q : ℕ
hpq : p + 1 ≠ q
⊢ hom H p q = 0

Tactic:
dif_neg hpq

Premises used: CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom, dif_neg
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
⊢ f.app (op ⦋0⦌) =
    HAdd.hAdd (α := X _⦋0⦌ ⟶ Y _⦋0⦌)
      (CategoryStruct.comp (Y := Y _⦋1⦌) (hom H 0 1)
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y) 1 0))
      (g.app (op ⦋0⦌))

Tactic:
simp [← H.h_last_comp_δ_last 0]

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_last_comp_δ_last, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
rw :
  H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (β := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) n ≫ hom H n (n + 1) :
          X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (CategoryStruct.comp (Y := Y _⦋n + 2⦌) (hom H (n + 1) (n + 2))
          (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y) (n + 2) (n + 1))) +
      H.h 0 ≫ Y.δ 0
⊢ f.app (op ⦋n + 1⦌) =
    HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (β := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) n ≫ hom H n (n + 1) :
          X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (CategoryStruct.comp (Y := Y _⦋n + 2⦌) (hom H (n + 1) (n + 2))
          (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y) (n + 2) (n + 1))) +
      g.app (op ⦋n + 1⦌)

Tactic:
rw [← H.h_zero_comp_δ_zero, ← H.h_last_comp_δ_last]

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_last_comp_δ_last, CategoryTheory.SimplicialObject.Homotopy.h_zero_comp_δ_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
dsimp :
  H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (β := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) n ≫ hom H n (n + 1) :
          X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (CategoryStruct.comp (Y := Y _⦋n + 2⦌) (hom H (n + 1) (n + 2))
          (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y) (n + 2) (n + 1))) +
      H.h 0 ≫ Y.δ 0
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (β := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) n ≫ hom H n (n + 1) :
          X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (CategoryStruct.comp (Y := Y _⦋n + 2⦌) (hom H (n + 1) (n + 2))
          (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y) (n + 2) (n + 1))) +
      H.h 0 ≫ Y.δ 0

Tactic:
dsimp