-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
@[simp]
lemma extClass_hom [HasDerivedCategory.{w'} C] : hS.extClass.hom = hS.singleδ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ hS.extClass.hom = hS.singleδ

Tactic:
change SmallShiftedHom.equiv W Q hS.extClass = _

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (SmallShiftedHom.equiv W Q) hS.extClass = hS.singleδ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Q.commShiftIso 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    inv
        (Q.map
          (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
      Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
        (Q.commShiftIso 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁)

Tactic:
rfl

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
inst✝ : HasDerivedCategory C
⊢ ((isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
        Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃) ≫
      (Q.commShiftIso 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    ((singleFunctorsPostcompQIso C).hom.hom 0).app S.X₃ ≫
      (inv
            (Q.map
              (CochainComplex.mappingCone.descShortComplex
                (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
          Q.map
              (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
            (Q.commShiftIso 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁)) ≫
        (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S.X₁)

Tactic:
rw [Category.assoc, Category.assoc, Category.assoc,
  singleFunctorsPostcompQIso_hom_hom, singleFunctorsPostcompQIso_inv_hom]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Q.commShiftIso 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    (𝟙 ((singleFunctors C).functor 0)).app S.X₃ ≫
      inv
          (Q.map
            (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
        Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
          (Q.commShiftIso 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory C) 1).map
              ((𝟙 (((CochainComplex.singleFunctors C).postcomp Q).functor 0)).app S.X₁)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ ((isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
        Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃) ≫
      ((Q.commShiftIso 1).app ((CochainComplex.singleFunctor C 0).obj S.X₁)).hom =
    hS.singleδ

Tactic:
dsimp [singleδ, triangleOfSESδ]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ ((isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
        Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃) ≫
      (Q.commShiftIso 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    ((singleFunctorsPostcompQIso C).hom.hom 0).app S.X₃ ≫
      (inv
            (Q.map
              (CochainComplex.mappingCone.descShortComplex
                (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
          Q.map
              (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
            (Q.commShiftIso 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁)) ≫
        (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S.X₁)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (SmallShiftedHom.equiv W Q) hS.extClass = hS.singleδ

Tactic:
dsimp [extClass, SmallShiftedHom.equiv]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ ((Q.commShiftIso 1).app ((CochainComplex.singleFunctor C 0).obj S.X₁)).homToEquiv
      ((SmallHom.equiv W Q)
        ((SmallHom.mkInv (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0)))
              ⋯).comp
          (SmallHom.mk W (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃))) =
    hS.singleδ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ ((Q.commShiftIso 1).app ((CochainComplex.singleFunctor C 0).obj S.X₁)).homToEquiv
      ((SmallHom.equiv W Q)
        ((SmallHom.mkInv (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0)))
              ⋯).comp
          (SmallHom.mk W (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃))) =
    hS.singleδ

Tactic:
erw [SmallHom.equiv_comp, Iso.homToEquiv_apply]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ ((SmallHom.equiv W Q)
          (SmallHom.mkInv (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯) ≫
        (SmallHom.equiv W Q)
          (SmallHom.mk W (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃)) ≫
      ((Q.commShiftIso 1).app ((CochainComplex.singleFunctor C 0).obj S.X₁)).hom =
    hS.singleδ