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_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₁ :
  HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (S.X₁.shiftFunctorObjXIso 1 n₀ n₁ ⋯).hom)
        (n₁ + 1) ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₁ n₁ ≫
        𝟙 (Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) 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₀ ≫
        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₁)

Tactic:
rw [HomologicalComplex.homologyπ_naturality_assoc,
    HomologicalComplex.liftCycles_comp_cyclesMap_assoc,
    S.X₁.liftCycles_shift_homologyπ_assoc _ _ _ _ n₁ (by lia) (n₁ + 1) (by simp),
    Iso.inv_hom_id_app]

Premises used: CategoryTheory.ShortComplex.X₁, HomologicalComplex.homologyπ_naturality_assoc, HomologicalComplex.liftCycles_comp_cyclesMap_assoc, HAdd.hAdd, CategoryTheory.Iso.inv_hom_id_app, OfNat.ofNat, CochainComplex.liftCycles_shift_homologyπ_assoc
-- 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₁ :
  HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (HomologicalComplex.XIsoOfEq S.X₁ ⋯).hom)
        (n₁ + 1) ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₁ n₁ ≫ 𝟙 (HomologicalComplex.homology S.X₁ n₁) =
    S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁
⊢ HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (S.X₁.shiftFunctorObjXIso 1 n₀ n₁ ⋯).hom)
        (n₁ + 1) ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₁ n₁ ≫
        𝟙 (Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁) =
    S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁

Tactic:
dsimp [homologyFunctor_shift]

Premises used: CochainComplex.homologyFunctor_shift
-- 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₀)
⊢ HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (HomologicalComplex.XIsoOfEq S.X₁ ⋯).hom)
        (n₁ + 1) ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₁ n₁ ≫ 𝟙 (HomologicalComplex.homology S.X₁ n₁) =
    S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁

Tactic:
simp only [hab, add_comp, assoc, inl_v_triangle_mor₃_f_assoc,
    shiftFunctorObjXIso, neg_comp, Iso.inv_hom_id, comp_neg, comp_id,
    inr_f_triangle_mor₃_f_assoc, zero_comp, comp_zero, add_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Limits.comp_zero, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.neg_comp, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, CategoryTheory.Limits.zero_comp, add_zero
-- 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 : ℤ
rw :
  IsIso (X := HomologicalComplex.homology (mappingCone S.f) n) (Y := HomologicalComplex.homology S.X₃ n)
    (HomologicalComplex.homologyMap (descShortComplex S) n)
⊢ QuasiIsoAt (descShortComplex S) n

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap]

Premises used: quasiIsoAt_iff_isIso_homologyMap
-- 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 : ℤ
erw :
  Eq (α :=
    (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast.obj
        (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 4 1)) ⟶
      (composableArrows₅ hS n (n + 1) ⋯).δlast.obj' 2 _proof_363✝)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂ ≫
      CategoryTheory.Functor.map (HomologicalComplex.homologyFunctor C (up ℤ) n) (triangle S.f).mor₂ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂ ≫
      (composableArrows₅ hS n (n + 1) ⋯).δlast.map' 1 2 _proof_246✝ _proof_363✝)
⊢ (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast.map' 1 2
        _proof_246✝ _proof_363✝ ≫
      NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n =
    NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂ ≫
      (composableArrows₅ hS n (n + 1) ⋯).δlast.map' 1 2 _proof_246✝ _proof_363✝

Tactic:
erw [(homologyFunctorFactors C (up ℤ) n).hom.naturality_assoc]

Premises used: HomotopyCategory.homologyFunctorFactors, Int, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.naturality_assoc, ComplexShape.up
-- 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 : ℤ
dsimp :
  Eq (α :=
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂) ⟶ S.X₃.homology n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₂ ≫
      CategoryStruct.comp (Y := HomologicalComplex.homology (mappingCone S.f) n)
        (HomologicalComplex.homologyMap (inr S.f) n) (HomologicalComplex.homologyMap (descShortComplex S) n))
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₂ ≫ HomologicalComplex.homologyMap S.g n)
⊢ Eq (α :=
    (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast.obj
        (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 4 1)) ⟶
      (composableArrows₅ hS n (n + 1) ⋯).δlast.obj' 2 _proof_363✝)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂ ≫
      CategoryTheory.Functor.map (HomologicalComplex.homologyFunctor C (up ℤ) n) (triangle S.f).mor₂ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂ ≫
      (composableArrows₅ hS n (n + 1) ⋯).δlast.map' 1 2 _proof_246✝ _proof_363✝)

Tactic:
dsimp [-Fin.reduceFinMk]

Premises used: Fin.reduceFinMk
-- 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 : ℤ
rw :
  Eq (α :=
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂) ⟶ S.X₃.homology n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₂ ≫
      HomologicalComplex.homologyMap (inr S.f ≫ descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₂ ≫ HomologicalComplex.homologyMap S.g n)
rw₁ rw₂ :
  Eq (α :=
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂) ⟶ S.X₃.homology n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₂ ≫ HomologicalComplex.homologyMap S.g n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₂ ≫ HomologicalComplex.homologyMap S.g n)
⊢ Eq (α :=
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂) ⟶ S.X₃.homology n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₂ ≫
      CategoryStruct.comp (Y := HomologicalComplex.homology (mappingCone S.f) n)
        (HomologicalComplex.homologyMap (inr S.f) n) (HomologicalComplex.homologyMap (descShortComplex S) n))
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₂ ≫ HomologicalComplex.homologyMap S.g n)

Tactic:
rw [← HomologicalComplex.homologyMap_comp, inr_descShortComplex]

Premises used: HomologicalComplex.homologyMap_comp, CochainComplex.mappingCone.inr_descShortComplex
-- 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 : ℤ
dsimp :
  Eq (α :=
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
      S.X₁.homology (n + 1))
    (CategoryStruct.comp (Y :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1)) (Functor.obj (quotient C (up ℤ)) S.X₁))
        (Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
          (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
          n (n + 1) ⋯)
        (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₁) :
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
        S.X₁.homology (n + 1))
    ((NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (mappingCone S.f) ≫
          HomologicalComplex.homologyMap (descShortComplex S) n) ≫
        hS.δ n (n + 1) ⋯ :
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
        S.X₁.homology (n + 1))
⊢ (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast.map' 2 3
        _proof_299✝ _proof_364✝ ≫
      NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁ =
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n) ≫
      (composableArrows₅ hS n (n + 1) ⋯).δlast.map' 2 3 _proof_299✝ _proof_364✝

Tactic:
dsimp [-Fin.reduceFinMk]

Premises used: Fin.reduceFinMk
-- 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 : ℤ
erw :
  Eq (α :=
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
      S.X₁.homology (n + 1))
    (CategoryStruct.comp (Y :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1)) (Functor.obj (quotient C (up ℤ)) S.X₁))
        (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (mappingCone S.f) ≫
          HomologicalComplex.homologyMap (descShortComplex S) n ≫
            hS.δ n (n + 1) ⋯ ≫ NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₁)
        (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₁) :
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
        S.X₁.homology (n + 1))
    ((NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (mappingCone S.f) ≫
          HomologicalComplex.homologyMap (descShortComplex S) n) ≫
        hS.δ n (n + 1) ⋯ :
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
        S.X₁.homology (n + 1))
⊢ Eq (α :=
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
      S.X₁.homology (n + 1))
    (CategoryStruct.comp (Y :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1)) (Functor.obj (quotient C (up ℤ)) S.X₁))
        (Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
          (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
          n (n + 1) ⋯)
        (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₁) :
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
        S.X₁.homology (n + 1))
    ((NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (mappingCone S.f) ≫
          HomologicalComplex.homologyMap (descShortComplex S) n) ≫
        hS.δ n (n + 1) ⋯ :
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
        S.X₁.homology (n + 1))

Tactic:
erw [homologySequenceδ_triangleh hS]

Premises used: CochainComplex.mappingCone.homologySequenceδ_triangleh
-- 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 : ℤ
⊢ Eq (α :=
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
      S.X₁.homology (n + 1))
    (CategoryStruct.comp (Y :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1)) (Functor.obj (quotient C (up ℤ)) S.X₁))
        (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (mappingCone S.f) ≫
          HomologicalComplex.homologyMap (descShortComplex S) n ≫
            hS.δ n (n + 1) ⋯ ≫ NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₁)
        (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₁) :
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
        S.X₁.homology (n + 1))
    ((NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (mappingCone S.f) ≫
          HomologicalComplex.homologyMap (descShortComplex S) n) ≫
        hS.δ n (n + 1) ⋯ :
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
        S.X₁.homology (n + 1))

Tactic:
simp only [Functor.comp_obj, HomologicalComplex.homologyFunctor_obj, assoc,
            Iso.inv_hom_id_app, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_app, 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 : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
h₀ : Epi (app' φ 0 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)
h₁ : IsIso (app' φ 1 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4)
h₃ : IsIso (app' φ 3 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6)
h₄ : Mono (app' φ 4 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7)
⊢ IsIso (X := Functor.obj (quotient C (up ℤ) ⋙ homologyFunctor C (up ℤ) n) (mappingCone S.f)) (Y :=
    HomologicalComplex.homology S.X₃ n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (mappingCone S.f) ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)

Tactic:
apply Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
        ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅_exact _
          (mappingCone_triangleh_distinguished S.f) n _ rfl).δlast
        (composableArrows₅_exact hS n _ rfl).δlast φ

Premises used: HomotopyCategory.mappingCone_triangleh_distinguished, Int, CategoryTheory.Functor.homologySequenceComposableArrows₅_exact, CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono, HomologicalComplex.HomologySequence.composableArrows₅_exact, CategoryTheory.ShortComplex.f, HomotopyCategory.homologyFunctor, CategoryTheory.ComposableArrows.Exact.δlast, OfNat.ofNat, rfl, ComplexShape.up
-- 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 : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
h₀ :
  Epi (X := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₁))
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₁)
⊢ Epi (app' φ 0 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)

Tactic:
dsimp [φ]
-- 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 : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ Epi (X := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₁))
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₁)

Tactic:
infer_instance
-- 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 : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
h₁ :
  IsIso (X := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂))
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₂)
⊢ IsIso (app' φ 1 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4)

Tactic:
dsimp [φ]
-- 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 : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ IsIso (X := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂))
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) S.X₂)

Tactic:
infer_instance