-- Mathlib/CategoryTheory/Triangulated/Yoneda.lean
lemma preadditiveYoneda_homologySequenceδ_apply
    (T : Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {B : C} (x : T.obj₁ ⟶ B⟦n₀⟧) :
    (preadditiveYoneda.obj B).homologySequenceδ
      ((triangleOpEquivalence _).functor.obj (op T)) n₀ n₁ h x =
      T.mor₃ ≫ x⟦(1 : ℤ)⟧' ≫ (shiftFunctorAdd' C n₀ 1 n₁ h).inv.app B

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ ((ShiftedHom.opEquiv 1).symm ((triangleOpEquivalence C).functor.obj (op T)).mor₃ ≫ (shiftFunctor C 1).map x) ≫
      (shiftFunctorAdd' C n₀ 1 n₁ ⋯).inv.app B =
    (T.mor₃ ≫ (shiftFunctor C 1).map x) ≫ (shiftFunctorAdd' C n₀ 1 n₁ h).inv.app B

Tactic:
congr 2

Result:
case e_a.e_a
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ (ShiftedHom.opEquiv 1).symm ((triangleOpEquivalence C).functor.obj (op T)).mor₃ = T.mor₃

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ (ConcreteCategory.hom
        ((preadditiveYoneda.obj B).homologySequenceδ ((triangleOpEquivalence C).functor.obj (op T)) n₀ n₁ h))
      x =
    T.mor₃ ≫ (shiftFunctor C 1).map x ≫ (shiftFunctorAdd' C n₀ 1 n₁ h).inv.app B

Tactic:
simp only [Functor.homologySequenceδ, preadditiveYoneda_shiftMap_apply,
  ShiftedHom.comp, ← Category.assoc]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ ((ShiftedHom.opEquiv 1).symm ((triangleOpEquivalence C).functor.obj (op T)).mor₃ ≫ (shiftFunctor C 1).map x) ≫
      (shiftFunctorAdd' C n₀ 1 n₁ ⋯).inv.app B =
    (T.mor₃ ≫ (shiftFunctor C 1).map x) ≫ (shiftFunctorAdd' C n₀ 1 n₁ h).inv.app B

Proof state:
case e_a.e_a.a
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ ((triangleOpEquivalence C).functor.obj (op T)).mor₃ = (ShiftedHom.opEquiv 1) T.mor₃

Tactic:
rfl

Result:
no goals

Proof state:
case e_a.e_a.a
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ (ShiftedHom.opEquiv 1) ((ShiftedHom.opEquiv 1).symm ((triangleOpEquivalence C).functor.obj (op T)).mor₃) =
    (ShiftedHom.opEquiv 1) T.mor₃

Tactic:
rw [Equiv.apply_symm_apply]

Result:
case e_a.e_a.a
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ ((triangleOpEquivalence C).functor.obj (op T)).mor₃ = (ShiftedHom.opEquiv 1) T.mor₃

Proof state:
case e_a.e_a
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ (ShiftedHom.opEquiv 1).symm ((triangleOpEquivalence C).functor.obj (op T)).mor₃ = T.mor₃

Tactic:
apply (ShiftedHom.opEquiv _).injective

Result:
case e_a.e_a.a
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ (ShiftedHom.opEquiv 1) ((ShiftedHom.opEquiv 1).symm ((triangleOpEquivalence C).functor.obj (op T)).mor₃) =
    (ShiftedHom.opEquiv 1) T.mor₃