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

Proof state:
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)).shift ↑n₀).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂)
            ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            ⋯).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)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            ⋯).g)
⊢ (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)).homologySequenceδ
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
              ⋯).g).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y h)) ⋯).g)

Tactic:
ext

Result:
case comm₂₃.h
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)).shift ↑n₀).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂)
            ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            ⋯).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)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            ⋯).g)
x✝ : Ext S.X₁ Y n₀
⊢ ((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)).homologySequenceδ
                  ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
                ⋯).g).comp
        ↑homAddEquiv)
      x✝ =
    ((↑homAddEquiv).comp
        (ConcreteCategory.hom
          (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y h))
              ⋯).g))
      x✝

Proof state:
case comm₂₃.h
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)).shift ↑n₀).map
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂)
            ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            ⋯).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)).homologySequenceδ
              ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯)
            ⋯).g)
x✝ : Ext S.X₁ Y n₀
⊢ (ConcreteCategory.hom
        ((preadditiveYonedaObj ((singleFunctor C 0).obj Y) ⋙
              forget₂ (ModuleCat (End ((singleFunctor C 0).obj Y))) AddCommGrp).homologySequenceδ
          (Triangle.mk ((singleFunctor C 0).map S.g).op ((singleFunctor C 0).map S.f).op
            ((opShiftFunctorEquivalence (DerivedCategory C) 1).counitIso.inv.app (op ((singleFunctor C 0).obj S.X₁)) ≫
              (shiftFunctor (DerivedCategory C)ᵒᵖ 1).map hS.singleδ.op))
          ↑n₀ ↑n₁ ⋯))
      x✝.hom =
    (hS.extClass.comp x✝ h).hom

Tactic:
apply preadditiveYoneda_homologySequenceδ_singleTriangle_apply

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₀ n₁ : ℕ
h : 1 + n₀ = n₁
⊢ (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y h)) ⋯).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₀ n₁ : ℕ
h : 1 + n₀ = n₁
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y h)) ⋯).Exact

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