[GOAL]
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalPreadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasEqualizers C
inst✝³ : HasCokernels C
inst✝² : HasImages C
inst✝¹ : HasImageMaps C
inst✝ : HasProjectiveResolutions C
n : ℕ
X Y : C
f : X ⟶ Y
Z : C
⊢ NatTrans.app ((Tor' C n).map f) Z = (Functor.leftDerived ((tensoringRight C).obj Z) n).map f
[PROOFSTEP]
rfl
  -- porting note: this specific lemma was added because otherwise the internals of
  -- `NatTrans.leftDerived` leaks into the RHS (it was already so in mathlib)
[GOAL]
C : Type u_1
inst✝¹⁰ : Category.{?u.11756, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalPreadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasEqualizers C
inst✝⁴ : HasCokernels C
inst✝³ : HasImages C
inst✝² : HasImageMaps C
inst✝¹ : HasProjectiveResolutions C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ ((Tor' C (n + 1)).obj X).obj Y ≅ 0
[PROOFSTEP]
dsimp only [Tor', Functor.flip]
[GOAL]
C : Type u_1
inst✝¹⁰ : Category.{?u.11756, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalPreadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasEqualizers C
inst✝⁴ : HasCokernels C
inst✝³ : HasImages C
inst✝² : HasImageMaps C
inst✝¹ : HasProjectiveResolutions C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ (Functor.leftDerived ((tensoringRight C).obj Y) (n + 1)).obj X ≅ 0
[PROOFSTEP]
exact ((tensoringRight C).obj Y).leftDerivedObjProjectiveSucc n X
