-- Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
theorem exact_d_f {X Y : C} (f : X ⟶ Y) :
    (ShortComplex.mk (d f) f (by simp)).Exact

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this✝ : Epi α.τ₁
this : IsIso α.τ₂
⊢ (ShortComplex.mk (d f) f ⋯).Exact

Tactic:
have : Mono α.τ₃ := by dsimp; infer_instance

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this✝¹ : Epi α.τ₁
this✝ : IsIso α.τ₂
this : Mono α.τ₃
⊢ (ShortComplex.mk (d f) f ⋯).Exact

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this : Epi α.τ₁
⊢ IsIso α.τ₂

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this✝¹ : Epi α.τ₁
this✝ : IsIso α.τ₂
this : Mono α.τ₃
⊢ (ShortComplex.mk (kernel.ι f) f ⋯).Exact

Tactic:
apply ShortComplex.exact_of_f_is_kernel

Result:
case hS
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this✝¹ : Epi α.τ₁
this✝ : IsIso α.τ₂
this : Mono α.τ₃
⊢ IsLimit (KernelFork.ofι (ShortComplex.mk (kernel.ι f) f ⋯).f ⋯)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
⊢ (ShortComplex.mk (d f) f ⋯).Exact

Tactic:
have : Epi α.τ₁ := by dsimp; infer_instance

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this : Epi α.τ₁
⊢ (ShortComplex.mk (d f) f ⋯).Exact

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ (ShortComplex.mk (d f) f ⋯).Exact

Tactic:
let α : ShortComplex.mk (d f) f (by simp) ⟶ ShortComplex.mk (kernel.ι f) f (by simp) :=
  { τ₁ := Projective.π _
    τ₂ := 𝟙 _
    τ₃ := 𝟙 _ }

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
⊢ (ShortComplex.mk (d f) f ⋯).Exact

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this✝ : Epi α.τ₁
this : IsIso α.τ₂
⊢ Mono α.τ₃

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ kernel.ι f ≫ f = 0

Tactic:
simp

Result:
no goals

Proof state:
case hS
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this✝¹ : Epi α.τ₁
this✝ : IsIso α.τ₂
this : Mono α.τ₃
⊢ IsLimit (KernelFork.ofι (ShortComplex.mk (kernel.ι f) f ⋯).f ⋯)

Tactic:
apply kernelIsKernel

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this : Epi α.τ₁
⊢ (ShortComplex.mk (d f) f ⋯).Exact

Tactic:
have : IsIso α.τ₂ := by dsimp; infer_instance

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this✝ : Epi α.τ₁
this : IsIso α.τ₂
⊢ (ShortComplex.mk (d f) f ⋯).Exact

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ d f ≫ f = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
⊢ Epi α.τ₁

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this✝¹ : Epi α.τ₁
this✝ : IsIso α.τ₂
this : Mono α.τ₃
⊢ (ShortComplex.mk (d f) f ⋯).Exact

Tactic:
rw [ShortComplex.exact_iff_of_epi_of_isIso_of_mono α]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
this✝¹ : Epi α.τ₁
this✝ : IsIso α.τ₂
this : Mono α.τ₃
⊢ (ShortComplex.mk (kernel.ι f) f ⋯).Exact