-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
/-- Alternative formulation of `contravariant_sequence_exact₂` -/
lemma contravariant_sequence_exact₂' (n : ℕ) :
    (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y (zero_add n)))
      (AddCommGrp.ofHom ((mk₀ S.f).precomp Y (zero_add n))) (by
        ext
        dsimp
        simp only [mk₀_comp_mk₀_assoc, ShortComplex.zero, mk₀_zero, zero_comp])).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 : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  (ShortComplex.mk
      (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n).map
        ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
      (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n).map
        ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂)
      ⋯).Exact
⊢ (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).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 : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
            (((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)).shift ↑n).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
            (((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 ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).g)

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

Tactic:
simp only [mk₀_comp_mk₀_assoc, ShortComplex.zero, mk₀_zero, zero_comp]

Result:
no goals

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 : ℕ
⊢ AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯) ≫ AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯) = 0

Tactic:
ext

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

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 : ℕ
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).Exact

Tactic:
have := (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequence_exact₂ _
  (op_distinguished _ hS.singleTriangle_distinguished) n

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  (ShortComplex.mk
      (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n).map
        ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁)
      (((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n).map
        ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂)
      ⋯).Exact
⊢ (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).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 : ℕ
⊢ (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).Exact

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).Exact