awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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
⊢ (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
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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
⊢ η.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)
have 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)
Tactic: rw [Category.id_comp, Category.id_comp, η.naturality]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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)
⊢ η.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)
have h₁ : η.app A.left ≫ Y.map (A.hom.app n) = X_1.map (A.hom.app n) ≫ η.app (A.right.obj n)
Tactic: rw [Category.id_comp, Category.id_comp, η.naturality]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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)
⊢ η.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)
have h₂ : η.app A.left ≫ Y.map (A.hom.app n) = η.app A.left ≫ Y.map (A.hom.app n)
Tactic: rw [Category.id_comp, Category.id_comp, η.naturality]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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
⊢ (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
have h₁ : CommaMorphism.left
    ((whiskeringObj C D X_1).map f ≫ { left := η.app (obj point x_1), right := whiskerLeft (obj drop x_1) η, w := sorry }) =
  CommaMorphism.left
    ({ left := η.app (obj point x), right := whiskerLeft (obj drop x) η, w := sorry :
        CommaMorphism ((whiskeringObj C D X_1).obj x) ((whiskeringObj C D Y).obj x) } ≫
      (whiskeringObj C D Y).map f)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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)
⊢ (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
have 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 := sorry }))
      n =
    NatTrans.app
      (CommaMorphism.right
        ({ left := η.app (obj point x), right := whiskerLeft (obj drop x) η, w := sorry :
            CommaMorphism ((whiskeringObj C D X_1).obj x) ((whiskeringObj C D Y).obj x) } ≫
          (whiskeringObj C D Y).map f))
      n
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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
⊢ 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
have dsimp : 𝟙 X₀ ≫ f ≫ X.map (⦋0⦌.const j 0) = (f ≫ X.map (⦋0⦌.const i 0)) ≫ X.map g
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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
⊢ 𝟙 X₀ ≫ f ≫ X.map (⦋0⦌.const j 0) = (f ≫ X.map (⦋0⦌.const i 0)) ≫ X.map g
have rw : 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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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
⊢ 𝟙 X₀ ≫ f ≫ X.map (⦋0⦌.const j 0) = (f ≫ X.map (⦋0⦌.const i 0)) ≫ X.map g
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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
⊢ 𝟙 X₀ ≫ f ≫ X.map (⦋0⦌.const j 0) = (f ≫ X.map (⦋0⦌.const i 0)) ≫ X.map g
have rw₂ : f ≫ X.map (⦋0⦌.const j 0) = f ≫ X.map (⦋0⦌.const i 0 ≫ g)
Tactic: rw [Category.id_comp, Category.assoc, ← X.map_comp, w]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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)
⊢ 𝟙 X₀ ≫ f ≫ X.map (⦋0⦌.const j 0) = (f ≫ X.map (⦋0⦌.const i 0)) ≫ X.map g
have rw₃ : f ≫ X.map (⦋0⦌.const i 0 ≫ g) = f ≫ X.map (⦋0⦌.const i 0 ≫ g)
Tactic: rw [Category.id_comp, Category.assoc, ← X.map_comp, w]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
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)
⊢ 𝟙 X₀ ≫ f ≫ X.map (⦋0⦌.const j 0) = (f ≫ X.map (⦋0⦌.const i 0)) ≫ X.map g
have g₂ : ⦋0⦌ ⟶ j
Tactic: rw [Category.id_comp, Category.assoc, ← X.map_comp, w]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
⊢ 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)
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
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
have 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)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
x : SimplexCategory
⊢ 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)))
have 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)))
Tactic: simp_rw [← op_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
x : SimplexCategory
⊢ 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)))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : CosimplicialObject.Augmented.{v, u} Cᵒᵖ
f : X ⟶ Y
⊢ map (𝟭 (SimplicialObject.{v, u} C)) (NatTrans.leftOp f.right) ≫ X.leftOp.hom =
    Y.leftOp.hom ≫ map (SimplicialObject.const C) f.left.unop
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : CosimplicialObject.Augmented.{v, u} Cᵒᵖ
f : X ⟶ Y
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
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : CosimplicialObject.Augmented.{v, u} Cᵒᵖ
f : X ⟶ Y
x : SimplexCategoryᵒᵖ
⊢ 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)
have 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)))
Tactic: simp_rw [← unop_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : CosimplicialObject.Augmented.{v, u} Cᵒᵖ
f : X ⟶ Y
x : SimplexCategoryᵒᵖ
⊢ 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)))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
⊢ 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)
have 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 := sorry }
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
⊢ f ≫ (unop Y).rightOpLeftOpIso.hom.op =
    (unop X).rightOpLeftOpIso.hom.op ≫
      Quiver.Hom.op { left := NatTrans.leftOp (NatTrans.rightOp f.unop.left), right := f.unop.right, w := ⋯ }
have 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 := sorry }
Tactic: rw [← f.op_unop]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
⊢ 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 := ⋯ }
have 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 := sorry :
        CommaMorphism (unop Y).rightOp.leftOp (unop X).rightOp.leftOp } ≫
      (unop X).rightOpLeftOpIso.hom)
Tactic: simp_rw [← op_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SimplicialObject.Augmented.{v, u} C)ᵒᵖ
f : X ⟶ Y
⊢ ((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)
have 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 := sorry :
      CommaMorphism (unop Y).rightOp.leftOp (unop X).rightOp.leftOp } ≫
    (unop X).rightOpLeftOpIso.hom
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (goal)
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 : ℕ
⊢ 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⦌)
have 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
Tactic: rw [← H.h_zero_comp_δ_zero, ← H.h_last_comp_δ_last]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (goal)
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 : ℕ
⊢ 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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (goal)
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 : ℕ
⊢ 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
have simp : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
  HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
      (-∑ x : Fin (n + 1), ∑ x_1 : Fin (n + 2), HPow.hPow (α := ℤ) (-1) ((↑x : ℕ) + (↑x_1 : ℕ)) • X.δ x_1 ≫ H.h x)
      (-∑ x : Fin (n + 1 + 2),
          ∑ x_1 : Fin (n + 1 + 1), HPow.hPow (α := ℤ) (-1) ((↑x : ℕ) + (↑x_1 : ℕ)) • H.h x_1 ≫ Y.δ x) +
    H.h 0 ≫ Y.δ 0
Tactic: simp only [alternatingFaceMapComplex_obj_d, AlternatingFaceMapComplex.objD, hom_eq,
    Preadditive.comp_neg, Preadditive.neg_comp, Preadditive.comp_sum,
    Preadditive.sum_comp, Preadditive.comp_zsmul, Preadditive.zsmul_comp,
    smul_neg, Finset.sum_neg_distrib, ← Finset.sum_zsmul, smul_smul, ← pow_add]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (goal)
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 : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
⊢ α x = -β (x.2.succ, x.1.castSucc)
have dsimp : HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1 =
  -(HPow.hPow (α := ℤ) (-1) ((↑x.2 : ℕ) + 1 + (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ)
Tactic: dsimp [α, β]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (goal)
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 : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
⊢ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1 =
    -(HPow.hPow (α := ℤ) (-1) ((↑x.2 : ℕ) + 1 + (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ)
have simp : (HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ =
  (HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ
Tactic: simp only [← H.h_castSucc_comp_δ_succ_of_lt x.2 x.1 hx,
      pow_add, pow_one, mul_neg, mul_one, neg_mul, neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (goal)
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 : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
⊢ (HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ =
    (HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ
have rw : (HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ =
  (HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ
Tactic: rw [mul_comm]