awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq.{v_1 + 1} (α := Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n :
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n)
        (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
            𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
              Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
          Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
      Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
        HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)))) n)
have h : Eq (α := Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
  (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
      𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
        Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
    Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
  (𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))
Tactic: convert! comp_id _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α := Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
        𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
          Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
      Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))
have h : ∀ (A : Splitting.IndexSet (op ⦋n⦌)),
  Eq (α := Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
        Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
            Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌)))
            (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)))
      (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
          𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
            Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
        Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))
Tactic: apply (Γ₀.splitting X).hom_ext'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ Eq (α := Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
        Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
            Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌)))
            (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)))
      (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
          𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
            Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
        Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))
have h : Eq.{v_1 + 1} (α := Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
  (𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
    Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
  (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))
Tactic: rw [Splitting.ι_desc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ Eq.{v_1 + 1} (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))
have h : Eq.{v_1 + 1} (α := Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
  (𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
    Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
  (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
Tactic: erw [comp_id, id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
h :
  Eq.{v_1 + 1} (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
⊢ Eq.{v_1 + 1} (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))
have h₁ : Eq (α := Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
  (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A) (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
Tactic: erw [comp_id, id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)
n : ℕ
⊢ Eq (α :=
    (obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) X).X.X n ⟶ HomologicalComplex.X (Karoubi.X (obj (Γ₂ ⋙ N₂) X)) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂) X)) n)
    (X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
have dsimp : Eq (α := X.X.X n ⟶ Γ₀.Obj.obj₂ X.X (op ⦋n⦌))
  (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (NatTrans.app
          (preimage
            (obj
              (whiskeringLeft (ChainComplex.{v_1, u_1, 0} C ℕ) (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
              (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
            (Iso.inv N₁Γ₀ ≫ Iso.inv N₂Γ₂ToKaroubiIso))
          X))
      n :
    X.X.X n ⟶ HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ X))) n)
  (X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
Tactic: dsimp [N₂Γ₂]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)
n : ℕ
⊢ Eq (α := X.X.X n ⟶ Γ₀.Obj.obj₂ X.X (op ⦋n⦌))
    (HomologicalComplex.Hom.f
        (Karoubi.Hom.f
          (NatTrans.app
            (preimage
              (obj
                (whiskeringLeft (ChainComplex.{v_1, u_1, 0} C ℕ) (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                  (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
                (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
              (Iso.inv N₁Γ₀ ≫ Iso.inv N₂Γ₂ToKaroubiIso))
            X))
        n :
      X.X.X n ⟶ HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ X))) n)
    (X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
have simp : Eq (α := X.X.X n ⟶ Γ₀.Obj.obj₂ X.X (op ⦋n⦌))
  (HomologicalComplex.Hom.f (Karoubi.Hom.f (map (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) X.decompId_i)) n ≫
      X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
    X.X.X n ⟶ HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ X))) n)
  (X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
    X.X.X n ⟶
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj X.X) (Γ₀.splitting X.X)) (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)))
Tactic: simp only [whiskeringLeft_obj_preimage_app, NatTrans.comp_app, Functor.comp_map,
    Karoubi.comp_f, N₂Γ₂ToKaroubiIso_inv_app, HomologicalComplex.comp_f,
    N₁Γ₀_inv_app_f_f, toKaroubi_obj_X, Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f,
    PInfty_on_Γ₀_splitting_summand_eq_self, N₂_map_f_f, Γ₂_map_f_app, unop_op, Karoubi.decompId_p_f,
    PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Splitting.IndexSet.id_fst, SimplexCategory.len_mk,
    Splitting.ι_desc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
e : Iso (C := ChainComplex.{v_1, u_1, 0} C ℕ ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ Γ₂ ⋙ N₂)
  (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) :=
  N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ Γ₂ ⋙ N₂)
      (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))))
    (whiskerLeft (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.hom N₂Γ₂)) (Iso.hom N₂Γ₂ToKaroubiIso ≫ Iso.hom N₁Γ₀)
have h : map
    (obj
      (whiskeringLeft (ChainComplex.{v_1, u_1, 0} C ℕ) (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
        (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
      (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
    (preimage
      (obj
        (whiskeringLeft (ChainComplex.{v_1, u_1, 0} C ℕ) (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
          (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
        (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
      e.hom) =
  e.hom
Tactic: have h := ((whiskeringLeft _ _ (Karoubi (ChainComplex C ℕ))).obj
    (toKaroubi (ChainComplex C ℕ))).map_preimage e.hom
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
Goal:
j : ℕ
hj : j + 1 = 0
⊢ False
have apply : j.succ ≤ 0
Tactic: apply Nat.not_succ_le_zero j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
Goal:
j : ℕ
hj : j + 1 = 0
rw : j + 1 ≤ 0
⊢ j.succ ≤ 0
have rw₁ : LE.le (α := ℕ) 0 0
Tactic: rw [Nat.succ_eq_add_one, hj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] m) (hσ' q n m hnm) 0
have simp : Eq (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] m)
  ((if n < q then 0 else HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, sorry⟩ : Fin (n + 1))) ≫ eqToHom sorry) 0
Tactic: simp only [hσ', hσ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] m)
    ((if n < q then 0 else HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯) 0
have split_ifs : Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] m) (0 ≫ eqToHom sorry) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
q n a : ℕ
ha : n = a + q
⊢ hσ' q n (n + 1) ⋯ = HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))
have rw : (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, sorry⟩ : Fin (n + 1))) ≫ eqToHom sorry =
  HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, sorry⟩ : Fin (n + 1))
Tactic: rw [hσ'_eq ha rfl, eqToHom_refl, comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
q n a : ℕ
ha : n = a + q
rw :
  (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯ =
    HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))
⊢ hσ' q n (n + 1) ⋯ = HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))
have rw₁ : (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, sorry⟩ : Fin (n + 1))) ≫ 𝟙 (X _⦋n + 1⦌) =
  HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, sorry⟩ : Fin (n + 1))
Tactic: rw [hσ'_eq ha rfl, eqToHom_refl, comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
q n a : ℕ
ha : n = a + q
rw :
  (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯ =
    HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))
rw₁ :
  (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))) ≫ 𝟙 (X _⦋n + 1⦌) =
    HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))
⊢ hσ' q n (n + 1) ⋯ = HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))
have rw₂ : HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, sorry⟩ : Fin (n + 1)) = HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, sorry⟩ : Fin (n + 1))
Tactic: rw [hσ'_eq ha rfl, eqToHom_refl, comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
q : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) 0) 0
have rw : Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (hσ' q 0 1 sorry ≫ HomologicalComplex.d K[X] 1 0) 0
Tactic: rw [nullHomotopicMap'_f_of_not_rel_left (c_mk 1 0 rfl) cs_down_0_not_rel_left]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
q : ℕ
⊢ Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (hσ' q 0 1 ⋯ ≫ HomologicalComplex.d K[X] 1 0) 0
have zero : Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (hσ' 0 0 1 sorry ≫ HomologicalComplex.d K[X] 1 0) 0
Tactic: rcases q with (_ | q)
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
q : ℕ
zero :
  Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (hσ' 0 0 1 ⋯ ≫ HomologicalComplex.d K[X] 1 0) 0
⊢ Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (hσ' q 0 1 ⋯ ≫ HomologicalComplex.d K[X] 1 0) 0
have succ : ∀ (q : ℕ),
  Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (hσ' (q + 1) 0 1 sorry ≫ HomologicalComplex.d K[X] 1 0) 0
Tactic: rcases q with (_ | q)
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
⊢ Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (hσ' 0 0 1 ⋯ ≫ HomologicalComplex.d K[X] 1 0) 0
have zero : Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
  ((HSMul.hSMul (β := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (HPow.hPow (α := ℤ) (β := ℕ) (-1) 0)
        (X.σ (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))) ≫
      eqToHom sorry) ≫
    HomologicalComplex.d K[X] 1 0)
  0
Tactic: rw [hσ'_eq (show 0 = 0 + 0 by rfl) (c_mk 1 0 rfl)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
⊢ Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    ((HSMul.hSMul (β := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (HPow.hPow (α := ℤ) (β := ℕ) (-1) 0)
          (X.σ (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))) ≫
        eqToHom ⋯) ≫
      HomologicalComplex.d K[X] 1 0)
    0
have zero : HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋0⦌) (X.σ 0 ≫ X.δ 0) (-X.σ 0 ≫ X.δ 1) = 0
Tactic: suffices X.σ 0 ≫ X.δ 0 + -X.σ 0 ≫ X.δ 1 = 0 by simpa
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
⊢ HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋0⦌) (X.σ 0 ≫ X.δ 0) (-X.σ 0 ≫ X.δ 1) = 0
have zero : HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋0⦌) (𝟙 (X _⦋0⦌)) (-𝟙 (X _⦋0⦌)) = 0
Tactic: rw [← Fin.succ_zero_eq_one, δ_comp_σ_succ, δ_comp_σ_self' X (Fin.castSucc_zero.symm)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
q : ℕ
⊢ Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (hσ' (q + 1) 0 1 ⋯ ≫ HomologicalComplex.d K[X] 1 0) 0
have succ : Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
  (CategoryStruct.comp (Y := HomologicalComplex.X K[X] 1) 0 (HomologicalComplex.d K[X] 1 0)) 0
Tactic: rw [hσ'_eq_zero (Nat.succ_pos q) (c_mk 1 0 rfl), zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (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
q : ℕ
succ :
  Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (CategoryStruct.comp (Y := HomologicalComplex.X K[X] 1) 0 (HomologicalComplex.d K[X] 1 0)) 0
⊢ Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (hσ' (q + 1) 0 1 ⋯ ≫ HomologicalComplex.d K[X] 1 0) 0
have succ₁ : Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) 0 0
Tactic: rw [hσ'_eq_zero (Nat.succ_pos q) (c_mk 1 0 rfl), zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n m : ℕ
hnm : c.Rel m n
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[Y] m) (f.app (op ⦋n⦌) ≫ hσ' q n m hnm) (hσ' q n m hnm ≫ f.app (op ⦋m⦌))
have obtain : Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[Y] (n + 1)) (f.app (op ⦋n⦌) ≫ hσ' q n (n + 1) sorry)
  (hσ' q n (n + 1) sorry ≫ f.app (op ⦋n + 1⦌))
Tactic: obtain rfl : n + 1 = m := hnm
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[Y] (n + 1)) (f.app (op ⦋n⦌) ≫ hσ' q n (n + 1) ⋯)
    (hσ' q n (n + 1) ⋯ ≫ f.app (op ⦋n + 1⦌))
have simp : (f.app (op ⦋n⦌) ≫ if n < q then 0 else HPow.hPow (α := ℤ) (-1) (n - q) • Y.σ (⟨n - q, sorry⟩ : Fin (n + 1))) =
  (if n < q then 0 else HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, sorry⟩ : Fin (n + 1))) ≫ f.app (op ⦋n + 1⦌)
Tactic: simp only [AlternatingFaceMapComplex.obj_X, hσ', hσ, Int.reduceNeg, eqToHom_refl, comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ (f.app (op ⦋n⦌) ≫ if n < q then 0 else HPow.hPow (α := ℤ) (-1) (n - q) • Y.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) =
    (if n < q then 0 else HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫ f.app (op ⦋n + 1⦌)
have pos : n < q → Eq (α := X _⦋n⦌ ⟶ Y _⦋n + 1⦌) (f.app (op ⦋n⦌) ≫ 0) (0 ≫ f.app (op ⦋n + 1⦌))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
pos : n < q → Eq (α := X _⦋n⦌ ⟶ Y _⦋n + 1⦌) (f.app (op ⦋n⦌) ≫ 0) (0 ≫ f.app (op ⦋n + 1⦌))
⊢ (f.app (op ⦋n⦌) ≫ if n < q then 0 else HPow.hPow (α := ℤ) (-1) (n - q) • Y.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) =
    (if n < q then 0 else HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫ f.app (op ⦋n + 1⦌)
have neg : ¬n < q →
  f.app (op ⦋n⦌) ≫ (HPow.hPow (α := ℤ) (-1) (n - q) • Y.σ (⟨n - q, sorry⟩ : Fin (n + 1))) =
    (HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, sorry⟩ : Fin (n + 1))) ≫ f.app (op ⦋n + 1⦌)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
h : n < q
⊢ Eq (α := X _⦋n⦌ ⟶ Y _⦋n + 1⦌) (f.app (op ⦋n⦌) ≫ 0) (0 ≫ f.app (op ⦋n + 1⦌))
have pos : Eq (α := X _⦋n⦌ ⟶ Y _⦋n + 1⦌) (f.app (op ⦋n⦌) ≫ 0) 0
Tactic: rw [zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
h : n < q
pos : Eq (α := X _⦋n⦌ ⟶ Y _⦋n + 1⦌) (f.app (op ⦋n⦌) ≫ 0) 0
⊢ Eq (α := X _⦋n⦌ ⟶ Y _⦋n + 1⦌) (f.app (op ⦋n⦌) ≫ 0) (0 ≫ f.app (op ⦋n + 1⦌))
have pos₁ : Eq.{v_1 + 1} (α := X _⦋n⦌ ⟶ Y _⦋n + 1⦌) 0 0
Tactic: rw [zero_comp, comp_zero]