-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
/-- Alternative formulation of `covariant_sequence_exact₂` -/
lemma covariant_sequence_exact₂' (n : ℕ) :
    (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X (add_zero n)))
      (AddCommGrp.ofHom ((mk₀ S.g).postcomp X (add_zero n))) (by
        ext x
        dsimp
        simp only [comp_assoc_of_third_deg_zero, mk₀_comp_mk₀, ShortComplex.zero, mk₀_zero,
          comp_zero])).Exact

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).g)
⊢ Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).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
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).g)
⊢ (ConcreteCategory.hom
          (ShortComplex.mk
              (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
              (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂)
              ⋯).f).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).f)

case comm₂₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).g)
⊢ (ConcreteCategory.hom
          (ShortComplex.mk
              (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
              (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂)
              ⋯).g).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).g)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
⊢ AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯) ≫ AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯) = 0

Tactic:
ext x

Result:
case hf.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x : ↑(AddCommGrp.of (Ext X S.X₁ n))
⊢ (AddCommGrp.Hom.hom (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯) ≫ AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯))) x =
    (AddCommGrp.Hom.hom 0) x

Proof state:
case hf.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x : ↑(AddCommGrp.of (Ext X S.X₁ n))
⊢ (comp x (mk₀ S.f) ⋯).comp (mk₀ S.g) ⋯ = 0

Tactic:
simp only [comp_assoc_of_third_deg_zero, mk₀_comp_mk₀, ShortComplex.zero, mk₀_zero,
  comp_zero]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  (ShortComplex.mk (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
      (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).Exact
⊢ (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).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
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).g)
⊢ Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).g)

Proof state:
case hf.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x : ↑(AddCommGrp.of (Ext X S.X₁ n))
⊢ (AddCommGrp.Hom.hom (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯) ≫ AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯))) x =
    (AddCommGrp.Hom.hom 0) x

Tactic:
dsimp

Result:
case hf.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x : ↑(AddCommGrp.of (Ext X S.X₁ n))
⊢ (comp x (mk₀ S.f) ⋯).comp (mk₀ S.g) ⋯ = 0