awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
Z' : C
_ :
  ∀ (g' : S.X₂ ⟶ Z') (eq' : S.f ≫ g' = 0) (m : Abelian.coimage S.g ⟶ Z'),
    Abelian.coimage.π S.g ≫ m = g' →
      m =
        (fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
            (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
          g' eq'
⊢ ∀ (g' : S.X₂ ⟶ Z') (eq' : S.f ≫ g' = 0) (m : Abelian.coimage S.g ⟶ Z'),
    Abelian.coimage.π S.g ≫ m = g' →
      m =
        (fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
            (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
          g' eq'

Tactic:
_
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
Z' : C
g' : S.X₂ ⟶ Z'
_ :
  ∀ (eq' : S.f ≫ g' = 0) (m : Abelian.coimage S.g ⟶ Z'),
    Abelian.coimage.π S.g ≫ m = g' →
      m =
        (fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
            (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
          g' eq'
⊢ ∀ (eq' : S.f ≫ g' = 0) (m : Abelian.coimage S.g ⟶ Z'),
    Abelian.coimage.π S.g ≫ m = g' →
      m =
        (fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
            (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
          g' eq'

Tactic:
_
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
Z' : C
g' : S.X₂ ⟶ Z'
eq' : S.f ≫ g' = 0
_ :
  ∀ (m : Abelian.coimage S.g ⟶ Z'),
    Abelian.coimage.π S.g ≫ m = g' →
      m =
        (fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
            (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
          g' eq'
⊢ ∀ (m : Abelian.coimage S.g ⟶ Z'),
    Abelian.coimage.π S.g ≫ m = g' →
      m =
        (fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
            (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
          g' eq'

Tactic:
_
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
Z' : C
g' : S.X₂ ⟶ Z'
eq' : S.f ≫ g' = 0
m : Abelian.coimage S.g ⟶ Z'
hm : Abelian.coimage.π S.g ≫ m = g'
h₁ :
  coequalizer.π (kernel.ι S.g) 0 ≫ m =
    CategoryStruct.comp (Y := coequalizer (X := kernel S.g) (kernel.ι S.g) 0) (coequalizer.π (kernel.ι S.g) 0)
      ((fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
          (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
        g' eq')
⊢ m =
    (fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
        (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
      g' eq'

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
Z' : C
g' : S.X₂ ⟶ Z'
eq' : S.f ≫ g' = 0
m : Abelian.coimage S.g ⟶ Z'
hm : Abelian.coimage.π S.g ≫ m = g'
h₁ :
  g' =
    CategoryStruct.comp (Y := coequalizer (X := kernel S.g) (kernel.ι S.g) 0) (coequalizer.π (kernel.ι S.g) 0)
      ((fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
          (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
        g' eq')
h₂ h₃ : g' = g'
⊢ coequalizer.π (kernel.ι S.g) 0 ≫ m =
    CategoryStruct.comp (Y := coequalizer (X := kernel S.g) (kernel.ι S.g) 0) (coequalizer.π (kernel.ι S.g) 0)
      ((fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
          (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
        g' eq')

Tactic:
rw [hm, cokernel.π_desc]

Premises used: CategoryTheory.Limits.cokernel.π_desc
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : S.Exact
⊢ (Cofork.π (CokernelCofork.ofπ (Abelian.coimage.π S.g) ⋯) ≫ Iso.hom (Abelian.coimageIsoImage' S.g)) ≫ image.ι S.g =
    CategoryStruct.comp (Y := image S.g) (factorThruImage S.g) (image.ι S.g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := kernel f ⟶ Y) (kernel.ι f ≫ f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ Exact { X₁ := kernel f, X₂ := X, X₃ := Y, f := kernel.ι f, g := f, zero := ⋯ }

Tactic:
exact_of_f_is_kernel _ (kernelIsKernel f)

Premises used: CategoryTheory.ShortComplex.exact_of_f_is_kernel, CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ Exact { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }

Tactic:
exact_of_g_is_cokernel _ (cokernelIsCokernel f)

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel, CategoryTheory.Limits.cokernelIsCokernel
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ S.Exact ↔
    { X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} C }.Exact

Tactic:
ShortComplex.exact_iff_of_epi_of_isIso_of_mono
    { τ₁ := Abelian.factorThruImage S.f
      τ₂ := 𝟙 _
      τ₃ := 𝟙 _ }

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono, CategoryTheory.Abelian.factorThruImage, CategoryTheory.CategoryStruct.id, CategoryTheory.ShortComplex.Hom.mk, CategoryTheory.ShortComplex.f, CategoryTheory.ShortComplex.X₃, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
symm :
  { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} C }.Exact ↔
    S.Exact
⊢ S.Exact ↔
    { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} C }.Exact

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} C }.Exact ↔
    S.Exact

Tactic:
ShortComplex.exact_iff_of_epi_of_isIso_of_mono
    { τ₁ := 𝟙 _
      τ₂ := 𝟙 _
      τ₃ := Abelian.factorThruCoimage S.g }

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono, CategoryTheory.Abelian.coimage.π, CategoryTheory.ShortComplex.mk, CategoryTheory.ShortComplex.X₁, CategoryTheory.CategoryStruct.id, CategoryTheory.ShortComplex.Hom.mk, CategoryTheory.ShortComplex.zero, CategoryTheory.Abelian.factorThruCoimage, CategoryTheory.ShortComplex.f, CategoryTheory.ShortComplex.g, CategoryTheory.Abelian.comp_coimage_π_eq_zero, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} C }.Exact ↔
    S.Exact

Tactic:
exact ShortComplex.exact_iff_of_epi_of_isIso_of_mono
    { τ₁ := 𝟙 _
      τ₂ := 𝟙 _
      τ₃ := Abelian.factorThruCoimage S.g }

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono, CategoryTheory.ShortComplex.X₁, CategoryTheory.CategoryStruct.id, CategoryTheory.ShortComplex.Hom.mk, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Eq (α := kernel f ⟶ X) (kernel.ι f) 0

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Mono f

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
⊢ ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f

Tactic:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
⊢ ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f

Tactic:
tfae_have 2 → 1 := mono_of_kernel_ι_eq_zero _

Premises used: CategoryTheory.Abelian.mono_of_kernel_ι_eq_zero
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
⊢ Mono f

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
⊢ Eq (α := kernel f ⟶ X) (kernel.ι f) 0

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
⊢ ∀ (a : Mono f), Eq (α := kernel f ⟶ X) (kernel.ι f) 0

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
h : Mono f
rw : Eq (α := kernel f ⟶ Y) (kernel.ι f ≫ f) (0 ≫ f)
rw₁ : Eq (α := kernel f ⟶ Y) 0 (0 ≫ f)
rw₂ rw₃ : Eq.{v₁ + 1} (α := kernel f ⟶ Y) 0 0
⊢ Eq (α := kernel f ⟶ X) (kernel.ι f) 0

Tactic:
rw [← cancel_mono f, kernel.condition, zero_comp]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.kernel.condition, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
⊢ ∀ (a : Mono f), Eq (α := kernel f ⟶ X) (kernel.ι f) 0

Tactic:
tfae_have 1 → 2
  | _ => by rw [← cancel_mono f, kernel.condition, zero_comp]
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
tfae_1_to_2 : ∀ (a : Mono f), Eq (α := kernel f ⟶ X) (kernel.ι f) 0
⊢ ShortComplex.Exact (ShortComplex.mk (X₁ := Z) 0 f ⋯)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
tfae_1_to_2 : ∀ (a : Mono f), Eq (α := kernel f ⟶ X) (kernel.ι f) 0
⊢ Mono f

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
tfae_1_to_2 : ∀ (a : Mono f), Eq (α := kernel f ⟶ X) (kernel.ι f) 0
⊢ ShortComplex.Exact (ShortComplex.mk (X₁ := Z) 0 f ⋯) ↔ Mono f

Tactic:
3 ↔ 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
tfae_1_to_2 : ∀ (a : Mono f), Eq (α := kernel f ⟶ X) (kernel.ι f) 0
⊢ Eq (α := ShortComplex.X₁ (ShortComplex.mk (X₁ := Z) 0 f ⋯) ⟶ ShortComplex.X₂ (ShortComplex.mk (X₁ := Z) 0 f ⋯))
    (ShortComplex.f (ShortComplex.mk (X₁ := Z) 0 f ⋯)) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
tfae_1_to_2 : ∀ (a : Mono f), Eq (α := kernel f ⟶ X) (kernel.ι f) 0
⊢ ShortComplex.Exact (ShortComplex.mk (X₁ := Z) 0 f ⋯) ↔ Mono f

Tactic:
tfae_have 3 ↔ 1 := ShortComplex.exact_iff_mono _ (by simp)

Premises used: CategoryTheory.ShortComplex.exact_iff_mono
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
tfae_1_to_2 : ∀ (a : Mono f), Eq (α := kernel f ⟶ X) (kernel.ι f) 0
tfae_3_iff_1 : ShortComplex.Exact (ShortComplex.mk (X₁ := Z) 0 f ⋯) ↔ Mono f
⊢ [Mono f, Eq (α := kernel f ⟶ X) (kernel.ι f) 0, ShortComplex.Exact (ShortComplex.mk (X₁ := Z) 0 f ⋯)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Epi f

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
⊢ ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f

Tactic:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
⊢ ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f

Tactic:
tfae_have 2 → 1 := epi_of_cokernel_π_eq_zero _

Premises used: CategoryTheory.Abelian.epi_of_cokernel_π_eq_zero
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
⊢ Epi f

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
⊢ Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
⊢ ∀ (a : Epi f), Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
h : Epi f
rw : Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) (f ≫ 0)
rw₁ : Eq (α := X ⟶ cokernel f) 0 (f ≫ 0)
rw₂ rw₃ : Eq.{v₁ + 1} (α := X ⟶ cokernel f) 0 0
⊢ Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0

Tactic:
rw [← cancel_epi f, cokernel.condition, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.cokernel.condition, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
⊢ ∀ (a : Epi f), Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0

Tactic:
tfae_have 1 → 2
  | _ => by rw [← cancel_epi f, cokernel.condition, comp_zero]
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
tfae_1_to_2 : ∀ (a : Epi f), Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
⊢ ShortComplex.Exact (ShortComplex.mk (X₃ := Z) f 0 ⋯)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
tfae_1_to_2 : ∀ (a : Epi f), Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
⊢ Epi f

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
tfae_1_to_2 : ∀ (a : Epi f), Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
⊢ ShortComplex.Exact (ShortComplex.mk (X₃ := Z) f 0 ⋯) ↔ Epi f

Tactic:
3 ↔ 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
tfae_1_to_2 : ∀ (a : Epi f), Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
⊢ Eq (α := ShortComplex.X₂ (ShortComplex.mk (X₃ := Z) f 0 ⋯) ⟶ ShortComplex.X₃ (ShortComplex.mk (X₃ := Z) f 0 ⋯))
    (ShortComplex.g (ShortComplex.mk (X₃ := Z) f 0 ⋯)) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
tfae_1_to_2 : ∀ (a : Epi f), Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
⊢ ShortComplex.Exact (ShortComplex.mk (X₃ := Z) f 0 ⋯) ↔ Epi f

Tactic:
tfae_have 3 ↔ 1 := ShortComplex.exact_iff_epi _ (by simp)

Premises used: CategoryTheory.ShortComplex.exact_iff_epi
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
tfae_1_to_2 : ∀ (a : Epi f), Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
tfae_3_iff_1 : ShortComplex.Exact (ShortComplex.mk (X₃ := Z) f 0 ⋯) ↔ Epi f
⊢ [Epi f, Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0, ShortComplex.Exact (ShortComplex.mk (X₃ := Z) f 0 ⋯)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Faithful
S : ShortComplex.{v₁, u₁} C
hS : ShortComplex.Exact (S.map F)
rw :
  ∀
    (hS :
      Eq (α :=
        Limits.kernel (X := ShortComplex.X₂ (S.map F)) (ShortComplex.g (S.map F)) ⟶
          cokernel (X := ShortComplex.X₁ (S.map F)) (ShortComplex.f (S.map F)))
        (kernel.ι (ShortComplex.g (S.map F)) ≫ cokernel.π (ShortComplex.f (S.map F))) 0),
    Eq (α := Limits.kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
⊢ S.Exact

Tactic:
rw [ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero] at hS ⊢

Premises used: CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Faithful
S : ShortComplex.{v₁, u₁} C
hS : Eq (α := Limits.kernel (F.map S.g) ⟶ cokernel (F.map S.f)) (kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f)) 0
h : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0
⊢ Eq (α := Limits.kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0

Tactic:
apply F.zero_of_map_zero

Premises used: CategoryTheory.Functor.zero_of_map_zero
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Faithful
S : ShortComplex.{v₁, u₁} C
hS : Eq (α := Limits.kernel (F.map S.g) ⟶ cokernel (F.map S.f)) (kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f)) 0
⊢ Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj S.X₃) (F.map (kernel.ι S.g) ≫ F.map S.g) 0

Tactic:
simp only [← F.map_comp, kernel.condition, CategoryTheory.Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.kernel.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Faithful
S : ShortComplex.{v₁, u₁} C
hS : Eq (α := Limits.kernel (F.map S.g) ⟶ cokernel (F.map S.f)) (kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f)) 0
h :
  ∀ (k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)) (hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)),
    Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0
⊢ Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0

Tactic:
obtain ⟨k, hk⟩ :=
    kernel.lift' (F.map S.g) (F.map (kernel.ι S.g))
      (by simp only [← F.map_comp, kernel.condition, CategoryTheory.Functor.map_zero])

Premises used: CategoryTheory.Functor.map, CategoryTheory.ShortComplex.g, CategoryTheory.Limits.kernel.ι, CategoryTheory.Limits.kernel.lift'