awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a :
  x ≫
      Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯ ≫
        𝟙 (HomologicalComplex.homology S.X₁ n₁) =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h
⊢ x ≫
      CategoryStruct.comp (Y :=
        Functor.obj (homologyFunctor C (up ℤ) n₀) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
        (NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f))
        (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f) ≫
          CategoryStruct.comp (Y := Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁)
            (Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯ :
              Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₀) (mappingCone S.f) ⟶
                Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁)
            (CategoryStruct.comp (Y :=
                Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₁) (Functor.obj (quotient C (up ℤ)) S.X₁))
                (NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₁)) S.X₁)
                (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₁)) S.X₁) :
              Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁ ⟶
                HomologicalComplex.homology S.X₁ n₁)) =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ 𝟙 (S.X₁.homology n₁)

Tactic:
simp only [Iso.inv_hom_id_app, HomologicalComplex.homologyFunctor_obj, Iso.inv_hom_id_app_assoc,
    comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv_hom_id_app_assoc, HomologicalComplex.homologyFunctor_obj
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a :
  x ≫ Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯ =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h
⊢ x ≫
      Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯ ≫
        𝟙 (HomologicalComplex.homology S.X₁ n₁) =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h

Tactic:
erw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a :
  CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯) =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
⊢ x ≫ Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯ =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h

Tactic:
rw [← cancel_epi π, reassoc_of% hx', reassoc_of% hx',
    HomologicalComplex.homologyπ_naturality_assoc,
    HomologicalComplex.liftCycles_comp_cyclesMap_assoc]

Premises used: HomologicalComplex.homologyπ_naturality_assoc, HomologicalComplex.liftCycles_comp_cyclesMap_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a :
  ∀ (a : A' ⟶ S.X₁.X n₁) (b : A' ⟶ S.X₂.X n₀)
    (hab :
      x' =
        HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
          (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)),
    CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
        (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w)
        (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
          Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯) =
      HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
        HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
⊢ CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯) =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
obtain ⟨a, b, hab⟩ := decomp_to _ x' n₁ h

Premises used: CochainComplex.mappingCone.decomp_to
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
⊢ Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0

Tactic:
rw [hab, ext_to_iff _ n₁ (n₁ + 1) rfl, add_comp, assoc, assoc, inr_f_d, add_comp, assoc,
    assoc, assoc, assoc, inr_f_fst_v, comp_zero, comp_zero, add_zero, zero_comp,
    d_fst_v _ _ _ _ h, comp_neg, inl_v_fst_v_assoc, comp_neg, neg_eq_zero,
    add_comp, assoc, assoc, assoc, assoc, inr_f_snd_v, comp_id, zero_comp,
    d_snd_v _ _ _ h, comp_add, inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, add_zero] at w

Premises used: CategoryTheory.Category.assoc, CochainComplex.mappingCone.inr_f_fst_v, CochainComplex.mappingCone.d_snd_v, CochainComplex.mappingCone.inr_f_d, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Limits.comp_zero, neg_eq_zero, CochainComplex.mappingCone.inr_f_snd_v, CochainComplex.mappingCone.ext_to_iff, CategoryTheory.Category.comp_id, CochainComplex.mappingCone.inl_v_snd_v_assoc, CategoryTheory.Preadditive.add_comp, HAdd.hAdd, CategoryTheory.Preadditive.comp_add, CategoryTheory.Limits.zero_comp, add_zero, OfNat.ofNat, CochainComplex.mappingCone.inl_v_fst_v_assoc, rfl, CochainComplex.mappingCone.d_fst_v
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
w₁ : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
⊢ x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)

Tactic:
rw [hab, ext_to_iff _ n₁ (n₁ + 1) rfl, add_comp, assoc, assoc, inr_f_d, add_comp, assoc,
    assoc, assoc, assoc, inr_f_fst_v, comp_zero, comp_zero, add_zero, zero_comp,
    d_fst_v _ _ _ _ h, comp_neg, inl_v_fst_v_assoc, comp_neg, neg_eq_zero,
    add_comp, assoc, assoc, assoc, assoc, inr_f_snd_v, comp_id, zero_comp,
    d_snd_v _ _ _ h, comp_add, inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, add_zero] at w

Premises used: CategoryTheory.Category.assoc, CochainComplex.mappingCone.inr_f_fst_v, CochainComplex.mappingCone.d_snd_v, CochainComplex.mappingCone.inr_f_d, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Limits.comp_zero, neg_eq_zero, CochainComplex.mappingCone.inr_f_snd_v, CochainComplex.mappingCone.ext_to_iff, CategoryTheory.Category.comp_id, CochainComplex.mappingCone.inl_v_snd_v_assoc, CategoryTheory.Preadditive.add_comp, HAdd.hAdd, CategoryTheory.Preadditive.comp_add, CategoryTheory.Limits.zero_comp, add_zero, OfNat.ofNat, CochainComplex.mappingCone.inl_v_fst_v_assoc, rfl, CochainComplex.mappingCone.d_fst_v
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
simp : HomologicalComplex.liftCycles S.X₃ (b ≫ S.g.f n₀) n₁ ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
| HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
    HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
simp only [hab, add_comp, assoc, inr_f_descShortComplex_f,
    inl_v_descShortComplex_f, comp_zero, zero_add]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, zero_add, CategoryTheory.Preadditive.add_comp, CochainComplex.mappingCone.inl_v_descShortComplex_f, CochainComplex.mappingCone.inr_f_descShortComplex_f
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
a₁ :
  CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯) =
    HomologicalComplex.liftCycles S.X₃ (b ≫ S.g.f n₀) n₁ ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
⊢ CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯) =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
conv_rhs => simp only [hab, add_comp, assoc, inr_f_descShortComplex_f,
    inl_v_descShortComplex_f, comp_zero, zero_add]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, zero_add, CategoryTheory.Preadditive.add_comp, CochainComplex.mappingCone.inl_v_descShortComplex_f, CochainComplex.mappingCone.inr_f_descShortComplex_f
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
⊢ (up ℤ).Rel n₀ n₁

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
⊢ (-a) ≫ S.f.f n₁ = b ≫ S.X₂.d n₀ n₁

Tactic:
simp only [neg_comp, neg_eq_iff_add_eq_zero, w.2]

Premises used: neg_eq_iff_add_eq_zero, And.right, CategoryTheory.Preadditive.neg_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
⊢ (up ℤ).next n₁ = n₁ + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
a₁ :
  Eq (α := A' ⟶ HomologicalComplex.homology S.X₁ n₁)
    (CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯))
    (S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁)
⊢ CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯) =
    HomologicalComplex.liftCycles S.X₃ (b ≫ S.g.f n₀) n₁ ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
rw [hS.δ_eq n₀ n₁ (by simpa using h) (b ≫ S.g.f n₀) _ b rfl (-a)
    (by simp only [neg_comp, neg_eq_iff_add_eq_zero, w.2]) (n₁ + 1) (by simp)]

Premises used: HomologicalComplex.Hom.f, HAdd.hAdd, CategoryTheory.ShortComplex.ShortExact.δ_eq, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, CategoryTheory.ShortComplex.g, Neg.neg, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
a₁ :
  Eq (α := A' ⟶ HomologicalComplex.homology S.X₁ n₁)
    (CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        CategoryStruct.comp (Y :=
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 1)
                S.X₁).homology
            n₀)
          (HomologicalComplex.homologyMap (triangle S.f).mor₃ n₀)
          (NatTrans.app (Iso.hom (Functor.shiftIso (HomologicalComplex.homologyFunctor C (up ℤ) 0) 1 n₀ n₁ ⋯)) S.X₁)))
    (S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁)
⊢ Eq (α := A' ⟶ HomologicalComplex.homology S.X₁ n₁)
    (CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯))
    (S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁)

Tactic:
dsimp [Functor.shiftMap, homologyFunctor_shift]

Premises used: CochainComplex.homologyFunctor_shift, CategoryTheory.Functor.shiftMap
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
⊢ 1 + n₀ = n₁

Tactic:
lia