awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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.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✝)
have 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)
Tactic: dsimp [-Fin.reduceFinMk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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 ℤ)) 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)
have 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)
Tactic: rw [← HomologicalComplex.homologyMap_comp, inr_descShortComplex]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← HomologicalComplex.homologyMap_comp, inr_descShortComplex]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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.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✝
have 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) sorry)
      (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) sorry :
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
      S.X₁.homology (n + 1))
Tactic: dsimp [-Fin.reduceFinMk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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₁))
        (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))
have 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) sorry ≫ 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) sorry :
    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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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 (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)
have h₀ : Epi (app' φ 0 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)
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 φ
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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)
⊢ 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)
have h₁ : IsIso (app' φ 1 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4)
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 φ
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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)
⊢ 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)
have h₃ : IsIso (app' φ 3 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6)
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 φ
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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)
⊢ 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)
have h₄ : Mono (app' φ 4 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7)
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 φ
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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 (app' φ 0 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)
have 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₁)
Tactic: dsimp [φ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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 (app' φ 1 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4)
have 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₂)
Tactic: dsimp [φ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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 (app' φ 3 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6)
have h₃ : IsIso (X :=
  Precomp.obj
    (mk₄ (X₀ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂))
      (X₁ :=
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
      (X₂ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1)) (Functor.obj (quotient C (up ℤ)) S.X₁))
      (X₄ :=
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
        (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
      (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) n)
        (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f)))
      (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) sorry)
      (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
        (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f))
      (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
        (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))))
    (Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₁)) 3)
  (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₁)
Tactic: dsimp [φ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
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₂) ⋯ ⋯ ⋯ ⋯
⊢ Mono (app' φ 4 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7)
have h₄ : Mono (X :=
  Precomp.obj
    (mk₄ (X₀ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂))
      (X₁ :=
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
      (X₂ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1)) (Functor.obj (quotient C (up ℤ)) S.X₁))
      (X₄ :=
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
        (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
      (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) n)
        (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f)))
      (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) sorry)
      (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
        (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f))
      (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
        (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))))
    (Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₁)) 4)
  (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₂)
Tactic: dsimp [φ]