awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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₁Γ₀
⊢ 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
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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₁Γ₀
h :
  whiskerLeft (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (preimage
        {
          obj := fun (G : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) ↦
            toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ G,
          map :=
            fun {X Y : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)}
              (α : X ⟶ Y) ↦
            whiskerLeft (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) α,
          map_id := ⋯, map_comp := ⋯ :
          (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) ⥤
            ChainComplex.{v_1, u_1, 0} C ℕ ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) }
        e.hom) =
    e.hom
⊢ 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 ℕ))
      (preimage
        {
          obj := fun (G : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) ↦
            toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ G,
          map :=
            fun {X Y : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)}
              (α : X ⟶ Y) ↦
            whiskerLeft (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) α,
          map_id := ⋯, map_comp := ⋯ :
          (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) ⥤
            ChainComplex.{v_1, u_1, 0} C ℕ ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) }
        (Iso.hom (N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀))))
    (Iso.hom N₂Γ₂ToKaroubiIso ≫ Iso.hom N₁Γ₀)

Tactic:
h

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Idempotents.toKaroubi
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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₁Γ₀
h :
  whiskerLeft (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (preimage
        {
          obj := fun (G : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) ↦
            toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ G,
          map :=
            fun {X Y : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)}
              (α : X ⟶ Y) ↦
            whiskerLeft (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) α,
          map_id := ⋯, map_comp := ⋯ :
          (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) ⥤
            ChainComplex.{v_1, u_1, 0} C ℕ ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) }
        e.hom) =
    e.hom
⊢ 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 ℕ))
      (preimage
        {
          obj := fun (G : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) ↦
            toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ G,
          map :=
            fun {X Y : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)}
              (α : X ⟶ Y) ↦
            whiskerLeft (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) α,
          map_id := ⋯, map_comp := ⋯ :
          (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) ⥤
            ChainComplex.{v_1, u_1, 0} C ℕ ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ) }
        (Iso.hom (N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀))))
    (Iso.hom N₂Γ₂ToKaroubiIso ≫ Iso.hom N₁Γ₀)

Tactic:
exact h
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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
K : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ Eq (α :=
    obj (Γ₂ ⋙ N₂) (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K) ⟶
      obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K))
    (NatTrans.app (Iso.hom N₂Γ₂) (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K))
    (NatTrans.app (Iso.hom N₂Γ₂ToKaroubiIso) K ≫ NatTrans.app (Iso.hom N₁Γ₀) K)

Tactic:
congr_app whiskerLeft_toKaroubi_N₂Γ₂_hom K

Premises used: AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom, CategoryTheory.congr_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
i j : ℕ
h : j + 1 = i
⊢ c.Rel i j

Tactic:
ComplexShape.down_mk i j h

Premises used: ComplexShape.down_mk
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
j : ℕ
hj : j + 1 = 0
apply : j.succ ≤ 0
⊢ False

Tactic:
apply Nat.not_succ_le_zero j

Premises used: Nat.not_succ_le_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
j : ℕ
hj : j + 1 = 0
rw : j + 1 ≤ 0
rw₁ rw₂ : LE.le (α := ℕ) 0 0
⊢ j.succ ≤ 0

Tactic:
rw [Nat.succ_eq_add_one, hj]

Premises used: Nat.succ_eq_add_one
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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 : ℕ
hnm : c.Rel m n
⊢ X _⦋n + 1⦌ = HomologicalComplex.X K[X] m

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
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, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯) 0
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] m) (hσ' q n m hnm) 0

Tactic:
simp only [hσ', hσ]

Premises used: AlgebraicTopology.DoldKan.hσ, AlgebraicTopology.DoldKan.hσ'
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
split_ifs : Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] m) (0 ≫ eqToHom ⋯) 0
⊢ 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

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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) (0 ≫ eqToHom ⋯) 0

Tactic:
zero_comp

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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) (0 ≫ eqToHom ⋯) 0

Tactic:
exact zero_comp

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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 m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ X _⦋n + 1⦌ = HomologicalComplex.X K[X] m

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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 m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] m) (hσ' q n m hnm)
    ((HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯)

Tactic:
simp [hσ', hσ, ha]

Premises used: AlgebraicTopology.DoldKan.hσ, AlgebraicTopology.DoldKan.hσ'
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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))
rw₂ rw₃ :
  HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (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))

Tactic:
rw [hσ'_eq ha rfl, eqToHom_refl, comp_id]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.hσ'_eq, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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 : ℕ
rw : Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (hσ' q 0 1 ⋯ ≫ HomologicalComplex.d K[X] 1 0) 0
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) 0) 0

Tactic:
rw [nullHomotopicMap'_f_of_not_rel_left (c_mk 1 0 rfl) cs_down_0_not_rel_left]

Premises used: AlgebraicTopology.DoldKan.cs_down_0_not_rel_left, AlgebraicTopology.DoldKan.c_mk, Homotopy.nullHomotopicMap'_f_of_not_rel_left, OfNat.ofNat, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
succ :
  ∀ (q : ℕ),
    Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
      (hσ' (q + 1) 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

Tactic:
rcases q with (_ | q)
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
⊢ 0 = HAdd.hAdd (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
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, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))) ≫
        eqToHom ⋯) ≫
      HomologicalComplex.d K[X] 1 0)
    0
⊢ Eq (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (hσ' 0 0 1 ⋯ ≫ HomologicalComplex.d K[X] 1 0) 0

Tactic:
rw [hσ'_eq (show 0 = 0 + 0 by rfl) (c_mk 1 0 rfl)]

Premises used: AlgebraicTopology.DoldKan.c_mk, AlgebraicTopology.DoldKan.hσ'_eq, OfNat.ofNat, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
this : HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋0⦌) (X.σ 0 ≫ X.δ 0) (-X.σ 0 ≫ X.δ 1) = 0
⊢ 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

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
zero : HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋0⦌) (X.σ 0 ≫ X.δ 0) (-X.σ 0 ≫ X.δ 1) = 0
⊢ 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

Tactic:
suffices X.σ 0 ≫ X.δ 0 + -X.σ 0 ≫ X.δ 1 = 0 by simpa
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
zero : HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋0⦌) (𝟙 (X _⦋0⦌)) (-𝟙 (X _⦋0⦌)) = 0
⊢ HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋0⦌) (X.σ 0 ≫ X.δ 0) (-X.σ 0 ≫ X.δ 1) = 0

Tactic:
rw [← Fin.succ_zero_eq_one, δ_comp_σ_succ, δ_comp_σ_self' X (Fin.castSucc_zero.symm)]

Premises used: CategoryTheory.SimplicialObject.δ_comp_σ_self', Fin.succ_zero_eq_one, Fin.castSucc_zero, CategoryTheory.SimplicialObject.δ_comp_σ_succ, Eq.symm
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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⦌)) = 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
succ₁ succ₂ : Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) 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

Tactic:
rw [hσ'_eq_zero (Nat.succ_pos q) (c_mk 1 0 rfl), zero_comp]

Premises used: AlgebraicTopology.DoldKan.c_mk, AlgebraicTopology.DoldKan.hσ'_eq_zero, Nat.succ_pos, CategoryTheory.Limits.zero_comp, OfNat.ofNat, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
⊢ n + 1 = m

Tactic:
hnm
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
obtain :
  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⦌))
⊢ 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⦌))

Tactic:
obtain rfl : n + 1 = m := hnm

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
simp :
  (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⦌)
⊢ 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⦌))

Tactic:
simp only [AlternatingFaceMapComplex.obj_X, hσ', hσ, Int.reduceNeg, eqToHom_refl, comp_id]

Premises used: AlgebraicTopology.DoldKan.hσ, Int.reduceNeg, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.hσ', AlgebraicTopology.AlternatingFaceMapComplex.obj_X
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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⦌))
neg :
  ¬n < q →
    f.app (op ⦋n⦌) ≫ (HPow.hPow (α := ℤ) (-1) (n - q) • Y.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) =
      (HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫ 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⦌)

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
pos₁ pos₂ : Eq.{v_1 + 1} (α := X _⦋n⦌ ⟶ Y _⦋n + 1⦌) 0 0
⊢ Eq (α := X _⦋n⦌ ⟶ Y _⦋n + 1⦌) (f.app (op ⦋n⦌) ≫ 0) (0 ≫ f.app (op ⦋n + 1⦌))

Tactic:
rw [zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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
⊢ f.app (op ⦋n⦌) ≫ (HPow.hPow (α := ℤ) (-1) (n - q) • Y.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) =
    (HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫ f.app (op ⦋n + 1⦌)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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 : ℕ
x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
rw :
  Eq.{v_1 + 1} (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (nullHomotopicMap' fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
      HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) i ≫ hσ' q i j hij)
    (nullHomotopicMap' fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
      hσ' q i j hij ≫ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) j)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ nullHomotopicMap' (hσ' q))
    (nullHomotopicMap' (hσ' q) ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)

Tactic:
rw [nullHomotopicMap'_comp, comp_nullHomotopicMap']

Premises used: Homotopy.nullHomotopicMap'_comp, Homotopy.comp_nullHomotopicMap'
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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 : ℕ
x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
e_h :
  Eq.{v_1 + 1} (α :=
    (i j : ℕ) →
      (ComplexShape.down ℕ).Rel j i →
        (HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x) i ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x_1) j))
    (fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
      HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) i ≫ hσ' q i j hij)
    fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
    hσ' q i j hij ≫ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) j
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (nullHomotopicMap' fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
      HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) i ≫ hσ' q i j hij)
    (nullHomotopicMap' fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
      hσ' q i j hij ≫ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) j)

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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 : ℕ
x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
e_h :
  ∀ (n m : ℕ) (hnm : (ComplexShape.down ℕ).Rel m n),
    Eq (α :=
      HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x) n ⟶
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x_1) m)
      (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) n ≫ hσ' q n m hnm)
      (hσ' q n m hnm ≫ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) m)
⊢ Eq.{v_1 + 1} (α :=
    (i j : ℕ) →
      (ComplexShape.down ℕ).Rel j i →
        (HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x) i ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x_1) j))
    (fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
      HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) i ≫ hσ' q i j hij)
    fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
    hσ' q i j hij ≫ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) j

Tactic:
ext n m hnm
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
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 : ℕ
x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
n m : ℕ
hnm : (ComplexShape.down ℕ).Rel m n
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x) n ⟶
      HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x_1) m)
    (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) n ≫ hσ' q n m hnm)
    (hσ' q n m hnm ≫ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) m)

Tactic:
simp only [alternatingFaceMapComplex_map_f, hσ'_naturality]

Premises used: AlgebraicTopology.alternatingFaceMapComplex_map_f, AlgebraicTopology.DoldKan.hσ'_naturality