-- Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean
lemma quasiIso_descShortComplex : QuasiIso (descShortComplex S) where
  quasiIsoAt n

Proof state:
case h₃
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ Mono ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app S.X₂)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
⊢ ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast.map' 2 3 ⋯ ⋯ ≫
      (homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁ =
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n) ≫
      (composableArrows₅ hS n (n + 1) ⋯).δlast.map' 2 3 ⋯ ⋯

Tactic:
dsimp

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
⊢ (homologyFunctor C (up ℤ) 0).homologySequenceδ
        (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
          ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁))
        n (n + 1) ⋯ ≫
      (homologyFunctorFactors C (up ℤ) (n + 1)).hom.app S.X₁ =
    ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n) ≫
      hS.δ n (n + 1) ⋯

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
⊢ QuasiIsoAt (descShortComplex S) n

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
⊢ IsIso (HomologicalComplex.homologyMap (descShortComplex S) n)

Proof state:
case h₀
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ Epi (app' φ 0 ⋯)

case h₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ IsIso (app' φ 1 ⋯)

case h₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ IsIso (app' φ 3 ⋯)

case h₃
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ Mono (app' φ 4 ⋯)

Tactic:
all_goals dsimp [φ]; infer_instance

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
⊢ (homologyFunctor C (up ℤ) 0).homologySequenceδ
        (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
          ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁))
        n (n + 1) ⋯ ≫
      (homologyFunctorFactors C (up ℤ) (n + 1)).hom.app S.X₁ =
    ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n) ≫
      hS.δ n (n + 1) ⋯

Tactic:
erw [homologySequenceδ_triangleh hS]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
⊢ ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n ≫
          hS.δ n (n + 1) ⋯ ≫ (homologyFunctorFactors C (up ℤ) (n + 1)).inv.app S.X₁) ≫
      (homologyFunctorFactors C (up ℤ) (n + 1)).hom.app S.X₁ =
    ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n) ≫
      hS.δ n (n + 1) ⋯

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
this :
  IsIso
    ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
⊢ IsIso (HomologicalComplex.homologyMap (descShortComplex S) n)

Tactic:
apply IsIso.of_isIso_comp_left ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f))

Result:
no goals