-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
/-- Alternative formulation of `covariant_sequence_exact₁` -/
lemma covariant_sequence_exact₁' :
    (ShortComplex.mk
      (AddCommGrp.ofHom (hS.extClass.postcomp X h))
      (AddCommGrp.ofHom ((mk₀ S.f).postcomp X (add_zero n₁))) (by
        ext x
        dsimp
        simp only [comp_assoc_of_third_deg_zero, ShortComplex.ShortExact.extClass_comp,
          comp_zero])).Exact

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₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : ↑(AddCommGrp.of (Ext X S.X₃ n₀))
⊢ (AddCommGrp.Hom.hom (AddCommGrp.ofHom (hS.extClass.postcomp X h) ≫ AddCommGrp.ofHom ((mk₀ S.f).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₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : ↑(AddCommGrp.of (Ext X S.X₃ n₀))
⊢ (comp x hS.extClass h).comp (mk₀ S.f) ⋯ = 0

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

Tactic:
exact preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply hS x h

Result:
no goals

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₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : ↑(AddCommGrp.of (Ext X S.X₃ n₀))
⊢ (comp x hS.extClass h).comp (mk₀ S.f) ⋯ = 0

Tactic:
simp only [comp_assoc_of_third_deg_zero, ShortComplex.ShortExact.extClass_comp,
  comp_zero]

Result:
no goals

Proof state:
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₀ n₁ : ℕ
h : n₀ + 1 = n₁
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯)
            (((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))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯)
            (((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))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯)
              (((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 (hS.extClass.postcomp X h)) (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) ⋯).g)

Tactic:
ext x

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