awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (HPow.hPow (α := ℤ) (-1) (↑(i, j).2 : ℕ) • X.δ (i, j).2) ≫ (HPow.hPow (α := ℤ) (-1) (↑(i, j).1 : ℕ) • X.δ (i, j).1) =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ) • X.δ (φ (i, j) hij).2) ≫
        (HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) • X.δ (φ (i, j) hij).1)
have h : (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) =
  -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ) • X.δ (φ (i, j) hij).2) ≫
      (HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) • X.δ (φ (i, j) hij).1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ) • X.δ (φ (i, j) hij).2) ≫
        (HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) • X.δ (φ (i, j) hij).1)
have h : (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ)) • X.δ j ≫ X.δ i =
  -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ)) •
    X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1
Tactic: simp only [zsmul_comp, comp_zsmul, smul_smul, ← neg_smul]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ)) • X.δ j ≫ X.δ i =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ)) •
      X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1
have h : HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ) =
  -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
h :
  HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ) =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ))
⊢ (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ)) • X.δ j ≫ X.δ i =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ)) •
      X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1
have h₁ : X.δ j ≫ X.δ i = X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ) =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ))
have h : HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ) =
  HPow.hPow (α := ℤ) (-1) (↑(j.castLT sorry) : ℕ) * HPow.hPow (α := ℤ) (-1) (↑i : ℕ)
Tactic: simp only [φ, Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ X.δ j ≫ X.δ i = X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1
have h : (i, j).2 ≤ (i, j).1.castSucc
Tactic: rw [CategoryTheory.SimplicialObject.δ_comp_δ'']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
⊢ Eq (α := HomologicalComplex.X (obj X) (n + 1) ⟶ HomologicalComplex.X (obj Y) n)
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (n + 1))
      ((fun (n : ℕ) ↦ (f.app (op ⦋n⦌) : X _⦋n⦌ ⟶ Y _⦋n⦌)) (n + 1)) (HomologicalComplex.d (obj Y) (n + 1) n))
    (HomologicalComplex.d (obj X) (n + 1) n ≫ (fun (n : ℕ) ↦ (f.app (op ⦋n⦌) : X _⦋n⦌ ⟶ Y _⦋n⦌)) n)
have simp : Eq (α := X _⦋n + 1⦌ ⟶ Y _⦋n⦌) (f.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • Y.δ i)
  ((∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫ f.app (op ⦋n⦌))
Tactic: simp only [obj, ChainComplex.of_d, objD, Int.reduceNeg]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
⊢ Eq (α := X _⦋n + 1⦌ ⟶ Y _⦋n⦌) (f.app (op ⦋n + 1⦌) ≫ ∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • Y.δ i)
    ((∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫ f.app (op ⦋n⦌))
have rw : Eq.{v_1 + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n⦌)
  (∑ j : Fin (n + 2), f.app (op ⦋n + 1⦌) ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • Y.δ j))
  (∑ j : Fin (n + 2), (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ f.app (op ⦋n⦌))
Tactic: rw [comp_sum, sum_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
⊢ Eq.{v_1 + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n⦌)
    (∑ j : Fin (n + 2), f.app (op ⦋n + 1⦌) ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • Y.δ j))
    (∑ j : Fin (n + 2), (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ f.app (op ⦋n⦌))
have refine : ∀ (x : Fin (n + 2)),
  Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x →
    f.app (op ⦋n + 1⦌) ≫ (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • Y.δ x) =
      (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x) ≫ f.app (op ⦋n⦌)
Tactic: refine Finset.sum_congr rfl fun _ _ => ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
h : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x
⊢ f.app (op ⦋n + 1⦌) ≫ (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • Y.δ x) =
    (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x) ≫ f.app (op ⦋n⦌)
have rw : HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • f.app (op ⦋n + 1⦌) ≫ Y.δ x =
  HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x ≫ f.app (op ⦋n⦌)
Tactic: rw [comp_zsmul, zsmul_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
h : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x
⊢ HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • f.app (op ⦋n + 1⦌) ≫ Y.δ x =
    HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x ≫ f.app (op ⦋n⦌)
have e_a : f.app (op ⦋n + 1⦌) ≫ Y.δ x = X.δ x ≫ f.app (op ⦋n⦌)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
h : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x
⊢ f.app (op ⦋n + 1⦌) ≫ Y.δ x = X.δ x ≫ f.app (op ⦋n⦌)
have e_a : X.δ x ≫ f.app (op ⦋n⦌) = f.app (op ⦋n + 1⦌) ≫ Y.δ x
Tactic: symm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ Eq (α := SimplicialObject.{v_1, u_1} C ⥤ HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
    (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
      (F.mapHomologicalComplex (ComplexShape.down ℕ)))
    (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D)
have h_map : autoParam
  (∀ (X Y : SimplicialObject.{v_1, u_1} C) (f : X ⟶ Y),
    Eq (α :=
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
        (Functor.obj
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          X)
        (Functor.obj
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          Y))
      (CategoryTheory.Functor.map
        (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
          (F.mapHomologicalComplex (ComplexShape.down ℕ)))
        f)
      (CategoryStruct.comp (Y :=
        Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) (eqToHom sorry)
        (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) f ≫
          eqToHom sorry)))
  Functor.ext._auto_1
Tactic: apply CategoryTheory.Functor.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
h_map :
  autoParam
    (∀ (X Y : SimplicialObject.{v_1, u_1} C) (f : X ⟶ Y),
      Eq (α :=
        Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
          (Functor.obj
            (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
              (F.mapHomologicalComplex (ComplexShape.down ℕ)))
            X)
          (Functor.obj
            (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
              (F.mapHomologicalComplex (ComplexShape.down ℕ)))
            Y))
        (CategoryTheory.Functor.map
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          f)
        (CategoryStruct.comp (Y :=
          Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) (eqToHom ⋯)
          (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D)
              f ≫
            eqToHom ⋯)))
    Functor.ext._auto_1
⊢ Eq (α := SimplicialObject.{v_1, u_1} C ⥤ HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
    (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
      (F.mapHomologicalComplex (ComplexShape.down ℕ)))
    (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D)
have h_obj : ∀ (X : SimplicialObject.{v_1, u_1} C),
  Eq (α := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
    (Functor.obj
      (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
        (F.mapHomologicalComplex (ComplexShape.down ℕ)))
      X)
    (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X)
Tactic: apply CategoryTheory.Functor.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
      (Functor.obj
        (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
          (F.mapHomologicalComplex (ComplexShape.down ℕ)))
        X)
      (Functor.obj
        (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
          (F.mapHomologicalComplex (ComplexShape.down ℕ)))
        Y))
    (CategoryTheory.Functor.map
      (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
        (F.mapHomologicalComplex (ComplexShape.down ℕ)))
      f)
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) (eqToHom ⋯)
      (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) f ≫
        eqToHom ⋯))
have h_map : ∀ (n : ℕ),
  Eq (α :=
    HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          X)
        n ⟶
      HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          Y)
        n)
    (HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map
        (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
          (F.mapHomologicalComplex (ComplexShape.down ℕ)))
        f)
      n)
    (HomologicalComplex.Hom.f
      (CategoryStruct.comp (Y :=
        Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) (eqToHom sorry)
        (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) f ≫
          eqToHom sorry))
      n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X : SimplicialObject.{v_1, u_1} C
⊢ Eq (α := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
    (Functor.obj
      (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
        (F.mapHomologicalComplex (ComplexShape.down ℕ)))
      X)
    (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X)
have h_obj : ∀ (i j : ℕ),
  (ComplexShape.down ℕ).Rel i j →
    Eq (α :=
      HomologicalComplex.X
          (Functor.obj
            (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
              (F.mapHomologicalComplex (ComplexShape.down ℕ)))
            X)
          i ⟶
        HomologicalComplex.X
          (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) j)
      (HomologicalComplex.d
          (Functor.obj
            (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
              (F.mapHomologicalComplex (ComplexShape.down ℕ)))
            X)
          i j ≫
        eqToHom sorry)
      (eqToHom sorry ≫
        HomologicalComplex.d
          (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) i j)
Tactic: apply HomologicalComplex.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X : SimplicialObject.{v_1, u_1} C
h_obj :
  ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      Eq (α :=
        HomologicalComplex.X
            (Functor.obj
              (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
                (F.mapHomologicalComplex (ComplexShape.down ℕ)))
              X)
            i ⟶
          HomologicalComplex.X
            (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) j)
        (HomologicalComplex.d
            (Functor.obj
              (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
                (F.mapHomologicalComplex (ComplexShape.down ℕ)))
              X)
            i j ≫
          eqToHom ⋯)
        (eqToHom ⋯ ≫
          HomologicalComplex.d
            (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) i j)
⊢ Eq (α := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
    (Functor.obj
      (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
        (F.mapHomologicalComplex (ComplexShape.down ℕ)))
      X)
    (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X)
have h_obj₁ : HomologicalComplex.X
    (Functor.obj
      (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
        (F.mapHomologicalComplex (ComplexShape.down ℕ)))
      X) =
  HomologicalComplex.X (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X)
Tactic: apply HomologicalComplex.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X : SimplicialObject.{v_1, u_1} C
j : ℕ
⊢ Eq (α :=
    HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          X)
        (j + 1) ⟶
      HomologicalComplex.X
        (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) j)
    (HomologicalComplex.d
        (Functor.obj
          (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
            (F.mapHomologicalComplex (ComplexShape.down ℕ)))
          X)
        (j + 1) j ≫
      eqToHom ⋯)
    (eqToHom ⋯ ≫
      HomologicalComplex.d
        (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X) (j + 1) j)
have h_obj : Eq (α :=
  HomologicalComplex.X
      (Functor.obj (C := ChainComplex.{v_1, u_1, 0} C ℕ) (F.mapHomologicalComplex (ComplexShape.down ℕ))
        (Functor.obj (alternatingFaceMapComplex C) X))
      (j + 1) ⟶
    HomologicalComplex.X
      (Functor.obj (alternatingFaceMapComplex D) ((Functor.obj (SimplicialObject.whiskering C D) F).obj X)) j)
  (HomologicalComplex.d
      (Functor.obj (C := ChainComplex.{v_1, u_1, 0} C ℕ) (F.mapHomologicalComplex (ComplexShape.down ℕ))
        (Functor.obj (alternatingFaceMapComplex C) X))
      (j + 1) j ≫
    eqToHom sorry)
  (eqToHom sorry ≫
    HomologicalComplex.d
      (Functor.obj (alternatingFaceMapComplex D) ((Functor.obj (SimplicialObject.whiskering C D) F).obj X)) (j + 1) j)
Tactic: dsimp only [Functor.comp_obj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X : SimplicialObject.{v_1, u_1} C
j : ℕ
⊢ Eq (α :=
    HomologicalComplex.X
        (Functor.obj (C := ChainComplex.{v_1, u_1, 0} C ℕ) (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (Functor.obj (alternatingFaceMapComplex C) X))
        (j + 1) ⟶
      HomologicalComplex.X
        (Functor.obj (alternatingFaceMapComplex D) ((Functor.obj (SimplicialObject.whiskering C D) F).obj X)) j)
    (HomologicalComplex.d
        (Functor.obj (C := ChainComplex.{v_1, u_1, 0} C ℕ) (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (Functor.obj (alternatingFaceMapComplex C) X))
        (j + 1) j ≫
      eqToHom ⋯)
    (eqToHom ⋯ ≫
      HomologicalComplex.d
        (Functor.obj (alternatingFaceMapComplex D) ((Functor.obj (SimplicialObject.whiskering C D) F).obj X)) (j + 1) j)
have h_obj : Eq.{v_2 + 1} (α :=
  HomologicalComplex.X
      (Functor.obj (C := ChainComplex.{v_1, u_1, 0} C ℕ) (F.mapHomologicalComplex (ComplexShape.down ℕ))
        (Functor.obj (alternatingFaceMapComplex C) X))
      (j + 1) ⟶
    HomologicalComplex.X
      (Functor.obj (alternatingFaceMapComplex D) ((Functor.obj (SimplicialObject.whiskering C D) F).obj X)) j)
  (∑ x : Fin (j + 2), HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • F.map (X.δ x))
  (∑ i : Fin (j + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • ((Functor.obj (SimplicialObject.whiskering C D) F).obj X).δ i)
Tactic: simp only [Functor.mapHomologicalComplex_obj_d, alternatingFaceMapComplex_obj_d,
        eqToHom_refl, id_comp, comp_id, AlternatingFaceMapComplex.objD, Functor.map_sum,
        Functor.map_zsmul]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X : SimplicialObject.{v_1, u_1} C
⊢ HomologicalComplex.X
      (Functor.obj
        (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
          (F.mapHomologicalComplex (ComplexShape.down ℕ)))
        X) =
    HomologicalComplex.X (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X)
have h_obj : ∀ (n : ℕ),
  HomologicalComplex.X
      (Functor.obj
        (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
          (F.mapHomologicalComplex (ComplexShape.down ℕ)))
        X)
      n =
    HomologicalComplex.X (Functor.obj (Functor.obj (SimplicialObject.whiskering C D) F ⋙ alternatingFaceMapComplex D) X)
      n
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasPullbacks.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
x : X ⟶ Y
h : Mono x
x_1 : ℕ
⊢ Mono (X := HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) x_1)
    (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) x) x_1)
have dsimp : Mono (X := X _⦋x_1⦌) (x.app (op ⦋x_1⦌))
Tactic: dsimp