-- Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
@[simp]
lemma opEquiv'_symm_add {n a : ℤ} (x y : (Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦n⟧))
    (a' : ℤ) (h : n + a = a') :
    (opEquiv' n a a' h).symm (x + y) =
      (opEquiv' n a a' h).symm x + (opEquiv' n a a' h).symm y

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n a : ℤ
x y : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ (opEquiv' n a a' h).symm (x + y) = (opEquiv' n a a' h).symm x + (opEquiv' n a a' h).symm y

Tactic:
dsimp [opEquiv']

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n a : ℤ
x y : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).homToEquiv ((opEquiv n).symm (x + y)) =
    ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).homToEquiv ((opEquiv n).symm x) +
      ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).homToEquiv ((opEquiv n).symm y)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n a : ℤ
x y : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).homToEquiv ((opEquiv n).symm (x + y)) =
    ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).homToEquiv ((opEquiv n).symm x) +
      ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).homToEquiv ((opEquiv n).symm y)

Tactic:
erw [opEquiv_symm_add, Iso.homToEquiv_apply, Iso.homToEquiv_apply, Iso.homToEquiv_apply]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n a : ℤ
x y : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ ((opEquiv n).symm x + (opEquiv n).symm y) ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom =
    (opEquiv n).symm x ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom +
      (opEquiv n).symm y ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n a : ℤ
x y : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ ((opEquiv n).symm x + (opEquiv n).symm y) ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom =
    (opEquiv n).symm x ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom +
      (opEquiv n).symm y ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom

Tactic:
rw [Preadditive.add_comp]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n a : ℤ
x y : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ (opEquiv n).symm x ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom +
      (opEquiv n).symm y ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom =
    (opEquiv n).symm x ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom +
      (opEquiv n).symm y ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n a : ℤ
x y : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ (opEquiv n).symm x ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom +
      (opEquiv n).symm y ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom =
    (opEquiv n).symm x ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom +
      (opEquiv n).symm y ≫ ((shiftFunctorAdd' C a n a' ⋯).symm.app Y).hom

Tactic:
rfl

Result:
no goals