awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
W' : C
x : W' ⟶ S.X₂
h_1 : x ≫ S.g = 0
x_1 : W' ⟶ Abelian.image S.f
hm : x_1 ≫ Abelian.image.ι S.f = x
rw :
  x_1 ≫ Abelian.image.ι S.f =
    CategoryStruct.comp (Y := Abelian.image S.f)
      ((fun {W' : C} (u : W' ⟶ S.X₂) (hu : u ≫ S.g = 0) ↦
          (kernel.lift (cokernel.π S.f) u ⋯ : W' ⟶ kernel (Y := cokernel S.f) (cokernel.π S.f)))
        x h_1)
      (Abelian.image.ι S.f)
rw₁ :
  x =
    CategoryStruct.comp (Y := Abelian.image S.f)
      ((fun {W' : C} (u : W' ⟶ S.X₂) (hu : u ≫ S.g = 0) ↦
          (kernel.lift (cokernel.π S.f) u ⋯ : W' ⟶ kernel (Y := cokernel S.f) (cokernel.π S.f)))
        x h_1)
      (Abelian.image.ι S.f)
⊢ x_1 =
    (fun {W' : C} (u : W' ⟶ S.X₂) (hu : u ≫ S.g = 0) ↦
        (kernel.lift (cokernel.π S.f) u ⋯ : W' ⟶ kernel (Y := cokernel S.f) (cokernel.π S.f)))
      x h_1
have rw₂ : x = x
Tactic: rw [← cancel_mono (Abelian.image.ι S.f), hm, kernel.lift_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : S.Exact
⊢ IsColimit (CokernelCofork.ofπ (Abelian.coimage.π S.g) ⋯)
have h₁ : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
Tactic: rw [exact_iff_kernel_ι_comp_cokernel_π_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
u : S.X₂ ⟶ Z'
hu : S.f ≫ u = 0
⊢ Eq (α := kernel S.g ⟶ Z') (kernel.ι S.g ≫ u) 0
have rw : Eq (α := kernel S.g ⟶ Z')
  (kernel.ι S.g ≫ CategoryStruct.comp (Y := cokernel S.f) (cokernel.π S.f) (cokernel.desc S.f u hu)) 0
Tactic: rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
u : S.X₂ ⟶ Z'
hu : S.f ≫ u = 0
rw :
  Eq (α := kernel S.g ⟶ Z')
    (kernel.ι S.g ≫ CategoryStruct.comp (Y := cokernel S.f) (cokernel.π S.f) (cokernel.desc S.f u hu)) 0
⊢ Eq (α := kernel S.g ⟶ Z') (kernel.ι S.g ≫ u) 0
have rw₁ : Eq (α := kernel S.g ⟶ Z')
  (CategoryStruct.comp (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) (cokernel.desc S.f u hu)) 0
Tactic: rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
u : S.X₂ ⟶ Z'
hu : S.f ≫ u = 0
rw :
  Eq (α := kernel S.g ⟶ Z')
    (kernel.ι S.g ≫ CategoryStruct.comp (Y := cokernel S.f) (cokernel.π S.f) (cokernel.desc S.f u hu)) 0
rw₁ :
  Eq (α := kernel S.g ⟶ Z')
    (CategoryStruct.comp (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) (cokernel.desc S.f u hu)) 0
⊢ Eq (α := kernel S.g ⟶ Z') (kernel.ι S.g ≫ u) 0
have rw₂ : Eq (α := kernel S.g ⟶ Z') (CategoryStruct.comp (Y := cokernel S.f) 0 (cokernel.desc S.f u hu)) 0
Tactic: rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
u : S.X₂ ⟶ Z'
hu : S.f ≫ u = 0
rw :
  Eq (α := kernel S.g ⟶ Z')
    (kernel.ι S.g ≫ CategoryStruct.comp (Y := cokernel S.f) (cokernel.π S.f) (cokernel.desc S.f u hu)) 0
rw₁ :
  Eq (α := kernel S.g ⟶ Z')
    (CategoryStruct.comp (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) (cokernel.desc S.f u hu)) 0
rw₂ : Eq (α := kernel S.g ⟶ Z') (CategoryStruct.comp (Y := cokernel S.f) 0 (cokernel.desc S.f u hu)) 0
⊢ Eq (α := kernel S.g ⟶ Z') (kernel.ι S.g ≫ u) 0
have rw₃ : Eq.{v₁ + 1} (α := kernel S.g ⟶ Z') 0 0
Tactic: rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
⊢ IsColimit (CokernelCofork.ofπ (Abelian.coimage.π S.g) ⋯)
have refine : ∀ {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 sorry : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
        g' eq'
Tactic: refine CokernelCofork.IsColimit.ofπ _ _
    (fun u hu => cokernel.desc (kernel.ι S.g) u
      (by rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]))
    (by simp) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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'
⊢ 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'
have 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 sorry : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
      g' eq')
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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'
⊢ 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')
have 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 sorry : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
      g' eq')
Tactic: rw [hm, cokernel.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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')
⊢ 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')
have h₂ : g' = g'
Tactic: rw [hm, cokernel.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ 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
have symm : { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := sorry :
      ShortComplex.{v₁, u₁} C }.Exact ↔
  S.Exact
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
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, Eq (α := kernel f ⟶ X) (kernel.ι f) 0, ShortComplex.Exact (ShortComplex.mk (X₁ := Z) 0 f ⋯)].TFAE
have tfae_2_to_1 : ∀ (a : Eq (α := kernel f ⟶ X) (kernel.ι f) 0), Mono f
Tactic: tfae_have 2 → 1 := mono_of_kernel_ι_eq_zero _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
⊢ Eq (α := kernel f ⟶ X) (kernel.ι f) 0
have rw : Eq (α := kernel f ⟶ Y) (kernel.ι f ≫ f) (0 ≫ f)
Tactic: rw [← cancel_mono f, kernel.condition, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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)
⊢ Eq (α := kernel f ⟶ X) (kernel.ι f) 0
have rw₁ : Eq (α := kernel f ⟶ Y) 0 (0 ≫ f)
Tactic: rw [← cancel_mono f, kernel.condition, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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)
⊢ Eq (α := kernel f ⟶ X) (kernel.ι f) 0
have rw₂ : Eq.{v₁ + 1} (α := kernel f ⟶ Y) 0 0
Tactic: rw [← cancel_mono f, kernel.condition, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
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, Eq (α := kernel f ⟶ X) (kernel.ι f) 0, ShortComplex.Exact (ShortComplex.mk (X₁ := Z) 0 f ⋯)].TFAE
have tfae_1_to_2 : ∀ (a : Mono f), Eq (α := kernel f ⟶ X) (kernel.ι f) 0
Tactic: tfae_have 1 → 2
  | _ => by rw [← cancel_mono f, kernel.condition, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
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, Eq (α := kernel f ⟶ X) (kernel.ι f) 0, ShortComplex.Exact (ShortComplex.mk (X₁ := Z) 0 f ⋯)].TFAE
have tfae_3_iff_1 : ShortComplex.Exact (ShortComplex.mk (X₁ := Z) 0 f sorry) ↔ Mono f
Tactic: tfae_have 3 ↔ 1 := ShortComplex.exact_iff_mono _ (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
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, Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0, ShortComplex.Exact (ShortComplex.mk (X₃ := Z) f 0 ⋯)].TFAE
have tfae_2_to_1 : ∀ (a : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), Epi f
Tactic: tfae_have 2 → 1 := epi_of_cokernel_π_eq_zero _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
⊢ Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
have rw : Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) (f ≫ 0)
Tactic: rw [← cancel_epi f, cokernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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)
⊢ Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
have rw₁ : Eq (α := X ⟶ cokernel f) 0 (f ≫ 0)
Tactic: rw [← cancel_epi f, cokernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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)
⊢ Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
have rw₂ : Eq.{v₁ + 1} (α := X ⟶ cokernel f) 0 0
Tactic: rw [← cancel_epi f, cokernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
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, Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0, ShortComplex.Exact (ShortComplex.mk (X₃ := Z) f 0 ⋯)].TFAE
have tfae_1_to_2 : ∀ (a : Epi f), Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
Tactic: tfae_have 1 → 2
  | _ => by rw [← cancel_epi f, cokernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
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, Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0, ShortComplex.Exact (ShortComplex.mk (X₃ := Z) f 0 ⋯)].TFAE
have tfae_3_iff_1 : ShortComplex.Exact (ShortComplex.mk (X₃ := Z) f 0 sorry) ↔ Epi f
Tactic: tfae_have 3 ↔ 1 := ShortComplex.exact_iff_epi _ (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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)
⊢ S.Exact
have 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
Tactic: rw [ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero] at hS ⊢
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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 (α := Limits.kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have h : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0
Tactic: apply F.zero_of_map_zero
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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 (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0
have 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
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])
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
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
have h : ∀ (l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)) (hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)),
  Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0
Tactic: obtain ⟨l, hl⟩ :=
    cokernel.desc' (F.map S.f) (F.map (cokernel.π S.f))
      (by simp only [← F.map_comp, cokernel.condition, CategoryTheory.Functor.map_zero])
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
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)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0
have h : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g) ≫ F.map (cokernel.π S.f)) 0
Tactic: rw [F.map_comp, ← hl, ← hk, Category.assoc, reassoc_of% hS, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
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)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
h : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g) ≫ F.map (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
have h₁ : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g) ≫ cokernel.π (F.map S.f) ≫ l) 0
Tactic: rw [F.map_comp, ← hl, ← hk, Category.assoc, reassoc_of% hS, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
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)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
h : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g) ≫ F.map (cokernel.π S.f)) 0
h₁ : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g) ≫ cokernel.π (F.map S.f) ≫ l) 0
⊢ Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0
have h₂ : (k ≫ kernel.ι (F.map S.g)) ≫ cokernel.π (F.map S.f) ≫ l = 0
Tactic: rw [F.map_comp, ← hl, ← hk, Category.assoc, reassoc_of% hS, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
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)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
h : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g) ≫ F.map (cokernel.π S.f)) 0
h₁ : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g) ≫ cokernel.π (F.map S.f) ≫ l) 0
h₂ : (k ≫ kernel.ι (F.map S.g)) ≫ cokernel.π (F.map S.f) ≫ l = 0
⊢ Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0
have h₃ : k ≫ kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) ≫ l = 0
Tactic: rw [F.map_comp, ← hl, ← hk, Category.assoc, reassoc_of% hS, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
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)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
h : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g) ≫ F.map (cokernel.π S.f)) 0
h₁ : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g) ≫ cokernel.π (F.map S.f) ≫ l) 0
h₂ : (k ≫ kernel.ι (F.map S.g)) ≫ cokernel.π (F.map S.f) ≫ l = 0
h₃ : k ≫ kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) ≫ l = 0
⊢ Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0
have h₄ : k ≫ 0 ≫ l = 0
Tactic: rw [F.map_comp, ← hl, ← hk, Category.assoc, reassoc_of% hS, zero_comp, comp_zero]