awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesMonomorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
φ : Quiver.Hom (V := ShortComplex.{v₂, u₂} B)
  ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} A }.map
    L)
  (S.map L) :=
  {
    τ₁ :=
      𝟙
        (ShortComplex.X₁
          ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
                ShortComplex.{v₁, u₁} A }.map
            L)),
    τ₂ :=
      𝟙
        (ShortComplex.X₂
          ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
                ShortComplex.{v₁, u₁} A }.map
            L)),
    τ₃ := L.map (Abelian.factorThruCoimage S.g), comm₁₂ := ⋯, comm₂₃ := ⋯ }
hL :
  IsColimit (F :=
    parallelPair (X :=
      ShortComplex.X₁
        ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      (ShortComplex.f
        ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      0)
    (CokernelCofork.ofπ
      (ShortComplex.g
        ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      ⋯)
⊢ ShortComplex.Exact
    ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
          ShortComplex.{v₁, u₁} A }.map
      L)

Tactic:
apply ShortComplex.exact_of_g_is_cokernel

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesMonomorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
φ : Quiver.Hom (V := ShortComplex.{v₂, u₂} B)
  ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} A }.map
    L)
  (S.map L) :=
  {
    τ₁ :=
      𝟙
        (ShortComplex.X₁
          ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
                ShortComplex.{v₁, u₁} A }.map
            L)),
    τ₂ :=
      𝟙
        (ShortComplex.X₂
          ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
                ShortComplex.{v₁, u₁} A }.map
            L)),
    τ₃ := L.map (Abelian.factorThruCoimage S.g), comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsColimit (F :=
    parallelPair (X :=
      ShortComplex.X₁
        ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      (ShortComplex.f
        ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      0)
    (CokernelCofork.ofπ
      (ShortComplex.g
        ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      ⋯)

Tactic:
exact CokernelCofork.mapIsColimit _ ((S.exact_iff_exact_coimage_π).1 hS).gIsCokernel L

Premises used: CategoryTheory.ShortComplex.Exact.gIsCokernel, Iff.mp, CategoryTheory.ShortComplex.exact_iff_exact_coimage_π, CategoryTheory.Limits.CokernelCofork.mapIsColimit
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesEpimorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
⊢ L.PreservesHomology

Tactic:
apply preservesHomology_of_map_exact

Premises used: CategoryTheory.Functor.preservesHomology_of_map_exact
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesEpimorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
dsimp :
  CategoryStruct.comp (Y := L.obj (Abelian.image S.f)) (L.map (Abelian.factorThruImage S.f))
      (L.map (kernel.ι (cokernel.π S.f))) =
    L.map S.f ≫ 𝟙 (L.obj S.X₂)
⊢ CategoryStruct.comp (Y :=
      ShortComplex.X₁
        ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      (L.map (Abelian.factorThruImage S.f))
      (ShortComplex.f
        ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L)) =
    ShortComplex.f (S.map L) ≫ 𝟙 (ShortComplex.X₂ (S.map L))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesEpimorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
rw :
  CategoryStruct.comp (Y := L.obj (Abelian.image S.f)) (L.map (Abelian.factorThruImage S.f))
      (L.map (kernel.ι (cokernel.π S.f))) =
    L.map S.f
rw₁ :
  L.map (CategoryStruct.comp (Y := Abelian.image S.f) (Abelian.factorThruImage S.f) (kernel.ι (cokernel.π S.f))) =
    L.map S.f
rw₂ rw₃ : L.map S.f = L.map S.f
⊢ CategoryStruct.comp (Y := L.obj (Abelian.image S.f)) (L.map (Abelian.factorThruImage S.f))
      (L.map (kernel.ι (cokernel.π S.f))) =
    L.map S.f ≫ 𝟙 (L.obj S.X₂)

Tactic:
rw [Category.comp_id, ← L.map_comp, kernel.lift_ι]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.kernel.lift_ι
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesEpimorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
φ : Quiver.Hom (V := ShortComplex.{v₂, u₂} B) (S.map L)
  ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} A }.map
    L) :=
  { τ₁ := L.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (ShortComplex.X₂ (S.map L)), τ₃ := 𝟙 (ShortComplex.X₃ (S.map L)),
    comm₁₂ := ⋯, comm₂₃ := ⋯ }
hL :
  ShortComplex.Exact
    ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
          ShortComplex.{v₁, u₁} A }.map
      L)
⊢ ShortComplex.Exact (S.map L)

Tactic:
apply (ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).2

Premises used: Iff.mpr, CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesEpimorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
φ : Quiver.Hom (V := ShortComplex.{v₂, u₂} B) (S.map L)
  ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} A }.map
    L) :=
  { τ₁ := L.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (ShortComplex.X₂ (S.map L)), τ₃ := 𝟙 (ShortComplex.X₃ (S.map L)),
    comm₁₂ := ⋯, comm₂₃ := ⋯ }
hL :
  IsLimit (F :=
    parallelPair (X :=
      ShortComplex.X₂
        ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      (ShortComplex.g
        ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      0)
    (KernelFork.ofι
      (ShortComplex.f
        ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      ⋯)
⊢ ShortComplex.Exact
    ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
          ShortComplex.{v₁, u₁} A }.map
      L)

Tactic:
apply ShortComplex.exact_of_f_is_kernel

Premises used: CategoryTheory.ShortComplex.exact_of_f_is_kernel
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesEpimorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
φ : Quiver.Hom (V := ShortComplex.{v₂, u₂} B) (S.map L)
  ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} A }.map
    L) :=
  { τ₁ := L.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (ShortComplex.X₂ (S.map L)), τ₃ := 𝟙 (ShortComplex.X₃ (S.map L)),
    comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsLimit (F :=
    parallelPair (X :=
      ShortComplex.X₂
        ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      (ShortComplex.g
        ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      0)
    (KernelFork.ofι
      (ShortComplex.f
        ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L))
      ⋯)

Tactic:
exact KernelFork.mapIsLimit _ ((S.exact_iff_exact_image_ι).1 hS).fIsKernel L

Premises used: CategoryTheory.ShortComplex.Exact.fIsKernel, CategoryTheory.ShortComplex.exact_iff_exact_image_ι, CategoryTheory.Limits.KernelFork.mapIsLimit, Iff.mp
-- Module: Mathlib.CategoryTheory.Abelian.Ext
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
⊢ IsZero (C := ModuleCat.{v_1, u_1} R) (Functor.obj (Functor.obj (Ext R C (n + 1)) (Opposite.op X)) Y)

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

Premises used: CategoryTheory.ProjectiveResolution.isoExt, CategoryTheory.ProjectiveResolution.self, CategoryTheory.Limits.IsZero.of_iso, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Ext
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
refine :
  IsZero (C := ModuleCat.{v_1, u_1} R)
    (HomologicalComplex.homology
      (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1))
⊢ IsZero (C := ModuleCat.{v_1, u_1} R) (Functor.obj (Functor.obj (Ext R C (n + 1)) (Opposite.op X)) Y)

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

Premises used: CategoryTheory.ProjectiveResolution.isoExt, CategoryTheory.ProjectiveResolution.self, CategoryTheory.Limits.IsZero.of_iso, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Ext
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
rw :
  ShortComplex.Exact (C := ModuleCat.{v_1, u_1} R)
    (HomologicalComplex.sc
      (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1))
⊢ IsZero (C := ModuleCat.{v_1, u_1} R)
    (HomologicalComplex.homology
      (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1))

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

Premises used: HomologicalComplex.exactAt_iff_isZero_homology, HomologicalComplex.exactAt_iff
-- Module: Mathlib.CategoryTheory.Abelian.Ext
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
⊢ ShortComplex.Exact (C := ModuleCat.{v_1, u_1} R)
    (HomologicalComplex.sc
      (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1))

Tactic:
ShortComplex.exact_of_isZero_X₂ _ ?_

Premises used: CategoryTheory.ShortComplex.exact_of_isZero_X₂
-- Module: Mathlib.CategoryTheory.Abelian.Ext
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
refine :
  IsZero (C := ModuleCat.{v_1, u_1} R)
    (ShortComplex.X₂
      (HomologicalComplex.sc
        (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1)))
⊢ ShortComplex.Exact (C := ModuleCat.{v_1, u_1} R)
    (HomologicalComplex.sc
      (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1))

Tactic:
refine ShortComplex.exact_of_isZero_X₂ _ ?_

Premises used: CategoryTheory.ShortComplex.exact_of_isZero_X₂
-- Module: Mathlib.CategoryTheory.Abelian.Ext
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
dsimp :
  IsZero (C := ModuleCat.{v_1, u_1} R)
    (Functor.obj (Functor.obj (linearYoneda R C) Y)
      (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))
⊢ IsZero (C := ModuleCat.{v_1, u_1} R)
    (ShortComplex.X₂
      (HomologicalComplex.sc
        (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Ext
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
rw :
  Eq.{v_1 + 1} (α :=
    Quiver.Hom (V := ModuleCat.{v_1, u_1} R)
      (Functor.obj (Functor.obj (linearYoneda R C) Y)
        (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))
      (Functor.obj (Functor.obj (linearYoneda R C) Y)
        (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))))
    (𝟙
      (Functor.obj (Functor.obj (linearYoneda R C) Y)
        (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))))
    0
⊢ IsZero (C := ModuleCat.{v_1, u_1} R)
    (Functor.obj (Functor.obj (linearYoneda R C) Y)
      (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Abelian.Ext
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
hf :
  ∀
    (x :
      Opposite.unop
          (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))) ⟶
        Y),
    Eq (α :=
      (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
            (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
        Type v_1))
      ((ModuleCat.Hom.hom
              (𝟙
                (Functor.obj (Functor.obj (linearYoneda R C) Y)
                  (Opposite.op
                    (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))) :
            (a :
                (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) :
                  Type v_1)) →
              (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) : Type v_1))
          x :
        (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
              (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
          Type v_1))
      ((ModuleCat.Hom.hom 0 :
            (a :
                (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) :
                  Type v_1)) →
              (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) : Type v_1))
          x :
        (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
              (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
          Type v_1))
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom (V := ModuleCat.{v_1, u_1} R)
      (Functor.obj (Functor.obj (linearYoneda R C) Y)
        (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))
      (Functor.obj (Functor.obj (linearYoneda R C) Y)
        (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))))
    (𝟙
      (Functor.obj (Functor.obj (linearYoneda R C) Y)
        (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))))
    0

Tactic:
ext (x : _ ⟶ _)
-- Module: Mathlib.CategoryTheory.Abelian.Ext
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
x :
  Opposite.unop (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))) ⟶ Y
⊢ n + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Ext
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
⊢ Eq.{v_1 + 1} (α :=
    (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
          (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
      Type v_1))
    ((ModuleCat.Hom.hom
            (𝟙
              (Functor.obj (Functor.obj (linearYoneda R C) Y)
                (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))) :
          (a :
              (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) :
                Type v_1)) →
            (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) : Type v_1))
        0 :
      (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
            (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
        Type v_1))
    ((ModuleCat.Hom.hom 0 :
          (a :
              (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) :
                Type v_1)) →
            (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) : Type v_1))
        0 :
      (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
            (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
        Type v_1))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ Nonempty (AsSmall C)

Tactic:
⟨0⟩

Premises used: Nonempty.intro, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ Functor.Faithful (C := C) (Equivalence.functor AsSmall.equiv)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ Functor.Faithful (F C)

Tactic:
have : (F C).Faithful := by rw [F]; infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : Functor.Faithful (F C)
⊢ Functor.Faithful (C := AsSmall C) (Functor.rightOp Ind.yoneda)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : Functor.Faithful (F C)
⊢ Functor.Faithful (C := AsSmall C) (G C)

Tactic:
have : (G C).Faithful := by rw [G]; infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : Functor.Faithful (F C)
this : Functor.Faithful (C := AsSmall C) (G C)
⊢ Functor.Faithful (C := (Ind (AsSmall C)ᵒᵖ)ᵒᵖ) (D := ModuleCat (EmbeddingRing.{v, u} C)) (H C)

Tactic:
have : (H C).Faithful := IsGrothendieckAbelian.OppositeModuleEmbedding.faithful_embedding _
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : Functor.Faithful (F C)
this_2 : Functor.Faithful (C := AsSmall C) (G C)
this : Functor.Faithful (C := (Ind (AsSmall C)ᵒᵖ)ᵒᵖ) (D := ModuleCat (EmbeddingRing.{v, u} C)) (H C)
⊢ Functor.Faithful (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ Functor.Full (C := C) (Equivalence.functor AsSmall.equiv)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ Functor.Full (F C)

Tactic:
have : (F C).Full := by rw [F]; infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : Functor.Full (F C)
⊢ Functor.Full (C := AsSmall C) (Functor.rightOp Ind.yoneda)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : Functor.Full (F C)
⊢ Functor.Full (C := AsSmall C) (G C)

Tactic:
have : (G C).Full := by rw [G]; infer_instance