-- Mathlib/CategoryTheory/Abelian/Ext.lean
/-- If `X : C` is projective and `n : ℕ`, then `Ext^(n + 1) X Y ≅ 0` for any `Y`. -/
lemma isZero_Ext_succ_of_projective (X Y : C) [Projective X] (n : ℕ) :
    IsZero (((Ext R C (n + 1)).obj (Opposite.op X)).obj Y)

Proof state:
case hf.h
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ (ModuleCat.Hom.hom (𝟙 (((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1))))))
      0 =
    (ModuleCat.Hom.hom 0) 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ (HomologicalComplex.sc ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1)).Exact

Tactic:
refine ShortComplex.exact_of_isZero_X₂ _ ?_

Result:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ IsZero (HomologicalComplex.sc ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1)).X₂

Proof state:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ IsZero (((Ext R C (n + 1)).obj (Opposite.op X)).obj Y)

Tactic:
refine IsZero.of_iso ?_ ((ProjectiveResolution.self X).isoExt (n + 1) Y)

Result:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ IsZero (HomologicalComplex.homology ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1))

Proof state:
case hf.h
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
x : Opposite.unop (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1))) ⟶ Y
⊢ (ModuleCat.Hom.hom (𝟙 (((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1))))))
      x =
    (ModuleCat.Hom.hom 0) x

Tactic:
obtain rfl : x = 0 := (HomologicalComplex.isZero_single_obj_X
  (ComplexShape.down ℕ) 0 X (n + 1) (by simp)).eq_of_src _ _

Result:
case hf.h
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ (ModuleCat.Hom.hom (𝟙 (((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1))))))
      0 =
    (ModuleCat.Hom.hom 0) 0

Proof state:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ IsZero (((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1))))

Tactic:
rw [IsZero.iff_id_eq_zero]

Result:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ 𝟙 (((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) = 0

Proof state:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ IsZero (HomologicalComplex.homology ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1))

Tactic:
rw [← HomologicalComplex.exactAt_iff_isZero_homology, HomologicalComplex.exactAt_iff]

Result:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ (HomologicalComplex.sc ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1)).Exact

Proof state:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
x : Opposite.unop (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1))) ⟶ Y
⊢ n + 1 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ IsZero (HomologicalComplex.sc ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1)).X₂

Tactic:
dsimp

Result:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ IsZero (((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1))))

Proof state:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ 𝟙 (((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) = 0

Tactic:
ext (x : _ ⟶ _)

Result:
case hf.h
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
x : Opposite.unop (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1))) ⟶ Y
⊢ (ModuleCat.Hom.hom (𝟙 (((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1))))))
      x =
    (ModuleCat.Hom.hom 0) x