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
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
h₄ : k ≫ 0 ≫ 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₅ : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (k ≫ 0) 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
h₄ : k ≫ 0 ≫ l = 0
h₅ : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (k ≫ 0) 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.{v₂ + 1} (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) 0 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:
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Mono f
⊢ Mono (L.map f)
have apply : ShortComplex.Exact (ShortComplex.mk (X₁ := L.obj 0) 0 (L.map f) sorry)
Tactic: apply ((Abelian.tfae_mono (L.map f) (L.obj 0)).out 2 0).mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Mono f
⊢ ShortComplex.Exact (ShortComplex.mk (X₁ := L.obj 0) 0 (L.map f) ⋯)
have refine : Iso (C := ShortComplex.{v₂, u₂} B) (ShortComplex.map (ShortComplex.mk (X₁ := 0) 0 f sorry) L)
  (ShortComplex.mk (X₁ := L.obj 0) 0 (L.map f) sorry)
Tactic: refine ShortComplex.exact_of_iso ?_ (hL _ (((tfae_mono f 0).out 0 2).mp hf))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Epi f
⊢ Epi (L.map f)
have apply : ShortComplex.Exact (ShortComplex.mk (X₃ := L.obj 0) (L.map f) 0 sorry)
Tactic: apply ((Abelian.tfae_epi (L.map f) (L.obj 0)).out 2 0).mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Epi f
⊢ ShortComplex.Exact (ShortComplex.mk (X₃ := L.obj 0) (L.map f) 0 ⋯)
have refine : Iso (C := ShortComplex.{v₂, u₂} B) (ShortComplex.map (ShortComplex.mk (X₃ := 0) f 0 sorry) L)
  (ShortComplex.mk (X₃ := L.obj 0) (L.map f) 0 sorry)
Tactic: refine ShortComplex.exact_of_iso ?_ (hL _ (((tfae_epi f 0).out 0 2).mp hf))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
⊢ PreservesLimit (parallelPair f 0) L
have this : L.PreservesMonomorphisms
Tactic: have := preservesMonomorphisms_of_map_exact _ hL
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ PreservesLimit (parallelPair f 0) L
have apply : IsLimit (F := parallelPair f 0 ⋙ L) (L.mapCone (Fork.ofι (P := Limits.kernel f) (kernel.ι f) sorry))
Tactic: apply preservesLimit_of_preserves_limit_cone (kernelIsKernel f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ IsLimit (F := parallelPair f 0 ⋙ L) (L.mapCone (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯))
have apply : IsLimit (F := parallelPair (L.map f) 0) (KernelFork.map (Fork.ofι (P := Limits.kernel f) (kernel.ι f) sorry) L)
Tactic: apply (KernelFork.isLimitMapConeEquiv _ L).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ Mono (X := ShortComplex.X₁ (ShortComplex.map (ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f ⋯) L))
    (ShortComplex.f (ShortComplex.map (ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f ⋯) L))
have dsimp : Mono (X := L.obj (Limits.kernel f)) (L.map (kernel.ι f))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ IsLimit (F := parallelPair (L.map f) 0) (KernelFork.map (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯) L)
have this₁ : Mono (X := ShortComplex.X₁ (ShortComplex.map (ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f sorry) L))
  (ShortComplex.f (ShortComplex.map (ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f sorry) L))
Tactic: have : Mono ((ShortComplex.mk _ _ (kernel.condition f)).map L).f := by
      dsimp
      infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) L
have this : L.PreservesEpimorphisms
Tactic: have := preservesEpimorphisms_of_map_exact _ hL
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ PreservesColimit (parallelPair f 0) L
have apply : IsColimit (F := parallelPair f 0 ⋙ L) (L.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) sorry))
Tactic: apply preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ IsColimit (F := parallelPair f 0 ⋙ L) (L.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯))
have apply : IsColimit (F := parallelPair (L.map f) 0) (CokernelCofork.map (Cofork.ofπ (P := cokernel f) (cokernel.π f) sorry) L)
Tactic: apply (CokernelCofork.isColimitMapCoconeEquiv _ L).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ Epi (X := ShortComplex.X₂ (ShortComplex.map (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯) L))
    (ShortComplex.g (ShortComplex.map (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯) L))
have dsimp : Epi (Y := L.obj (cokernel f)) (L.map (cokernel.π f))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
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
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ IsColimit (F := parallelPair (L.map f) 0) (CokernelCofork.map (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯) L)
have this₁ : Epi (X := ShortComplex.X₂ (ShortComplex.map (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry) L))
  (ShortComplex.g (ShortComplex.map (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry) L))
Tactic: have : Epi ((ShortComplex.mk _ _ (cokernel.condition f)).map L).g := by
      dsimp
      infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
⊢ L.PreservesHomology
have hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
Tactic: apply preservesHomology_of_map_exact
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
⊢ 𝟙
        (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.g (S.map L) =
    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) ≫
      L.map (Abelian.factorThruCoimage S.g)
have dsimp : 𝟙 (L.obj S.X₂) ≫ L.map S.g =
  CategoryStruct.comp (Y := L.obj (Abelian.coimage S.g)) (L.map (cokernel.π (kernel.ι S.g)))
    (L.map (Abelian.factorThruCoimage S.g))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
⊢ 𝟙 (L.obj S.X₂) ≫ L.map S.g =
    CategoryStruct.comp (Y := L.obj (Abelian.coimage S.g)) (L.map (cokernel.π (kernel.ι S.g)))
      (L.map (Abelian.factorThruCoimage S.g))
have rw : L.map S.g =
  CategoryStruct.comp (Y := L.obj (Abelian.coimage S.g)) (L.map (cokernel.π (kernel.ι S.g)))
    (L.map (Abelian.factorThruCoimage S.g))
Tactic: rw [Category.id_comp, ← L.map_comp, cokernel.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
rw :
  L.map S.g =
    CategoryStruct.comp (Y := L.obj (Abelian.coimage S.g)) (L.map (cokernel.π (kernel.ι S.g)))
      (L.map (Abelian.factorThruCoimage S.g))
⊢ 𝟙 (L.obj S.X₂) ≫ L.map S.g =
    CategoryStruct.comp (Y := L.obj (Abelian.coimage S.g)) (L.map (cokernel.π (kernel.ι S.g)))
      (L.map (Abelian.factorThruCoimage S.g))
have rw₁ : L.map S.g =
  L.map (CategoryStruct.comp (Y := Abelian.coimage S.g) (cokernel.π (kernel.ι S.g)) (Abelian.factorThruCoimage S.g))
Tactic: rw [Category.id_comp, ← L.map_comp, cokernel.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
rw :
  L.map S.g =
    CategoryStruct.comp (Y := L.obj (Abelian.coimage S.g)) (L.map (cokernel.π (kernel.ι S.g)))
      (L.map (Abelian.factorThruCoimage S.g))
rw₁ :
  L.map S.g =
    L.map (CategoryStruct.comp (Y := Abelian.coimage S.g) (cokernel.π (kernel.ι S.g)) (Abelian.factorThruCoimage S.g))
⊢ 𝟙 (L.obj S.X₂) ≫ L.map S.g =
    CategoryStruct.comp (Y := L.obj (Abelian.coimage S.g)) (L.map (cokernel.π (kernel.ι S.g)))
      (L.map (Abelian.factorThruCoimage S.g))
have rw₂ : L.map S.g = L.map S.g
Tactic: rw [Category.id_comp, ← L.map_comp, cokernel.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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₂₃ := ⋯ }
⊢ ShortComplex.Exact (S.map L)
have hL : ShortComplex.Exact
  ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := sorry :
        ShortComplex.{v₁, u₁} A }.map
    L)
Tactic: apply (ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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₂₃ := ⋯ }
⊢ 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)
have 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 := sorry :
            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 := sorry :
            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 := sorry :
            ShortComplex.{v₁, u₁} A }.map
        L))
    sorry)
Tactic: apply ShortComplex.exact_of_g_is_cokernel
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
⊢ L.PreservesHomology
have hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
Tactic: apply preservesHomology_of_map_exact
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
⊢ 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))
have 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₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
⊢ 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₂)
have 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
Tactic: rw [Category.comp_id, ← L.map_comp, kernel.lift_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
⊢ 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₂)
have rw₁ : L.map (CategoryStruct.comp (Y := Abelian.image S.f) (Abelian.factorThruImage S.f) (kernel.ι (cokernel.π S.f))) =
  L.map S.f
Tactic: rw [Category.comp_id, ← L.map_comp, kernel.lift_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
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
⊢ 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₂)
have rw₂ : L.map S.f = L.map S.f
Tactic: rw [Category.comp_id, ← L.map_comp, kernel.lift_ι]