-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
/-- Alternative formulation of `contravariant_sequence_exact₃` -/
lemma contravariant_sequence_exact₃' :
    (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y h))
      (AddCommGrp.ofHom (((mk₀ S.g).precomp Y (zero_add n₁)))) (by
        ext
        dsimp
        simp only [ShortComplex.ShortExact.comp_extClass_assoc])).Exact

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
            ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
            ⋯).g)
⊢ Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y h)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y h)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) ⋯).g)

Tactic:
apply Function.Exact.of_ladder_addEquiv_of_exact' (e₁ := Ext.homAddEquiv)
  (e₂ := Ext.homAddEquiv) (e₃ := Ext.homAddEquiv) (H := this)

Result:
case comm₁₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
            ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
            ⋯).g)
⊢ (ConcreteCategory.hom
          (ShortComplex.mk
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
              (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
              ⋯).f).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y h)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) ⋯).f)

case comm₂₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
            ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
            ⋯).g)
⊢ (ConcreteCategory.hom
          (ShortComplex.mk
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
              (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
              ⋯).g).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y h)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) ⋯).g)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  (ShortComplex.mk
      ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
        ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
      (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
        ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
      ⋯).Exact
⊢ (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y h)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) ⋯).Exact

Tactic:
rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
            ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
            ⋯).g)
⊢ Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y h)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y h)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) ⋯).g)