awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : KernelFork (Y := cokernel f) (cokernel.π f)
h :
  (s.pt ⟶ Y) = (s.pt ⟶ (parallelPair (Y := cokernel f) (cokernel.π f) 0).obj WalkingParallelPair.zero) →
    Y = (parallelPair (Y := cokernel f) (cokernel.π f) 0).obj WalkingParallelPair.zero →
      inv (imageMonoFactorisation f).e ≫ f =
        limit.π (parallelPair (Y := cokernel f) (cokernel.π f) 0) WalkingParallelPair.zero
⊢ limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e ≫ f = Fork.ι s

Tactic:
convert! limit.lift_π s WalkingParallelPair.zero using 2

Premises used: CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.WalkingParallelPair.zero
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : KernelFork (Y := cokernel f) (cokernel.π f)
e_1 : (s.pt ⟶ Y) = (s.pt ⟶ (parallelPair (Y := cokernel f) (cokernel.π f) 0).obj WalkingParallelPair.zero)
e_5 : Y = (parallelPair (Y := cokernel f) (cokernel.π f) 0).obj WalkingParallelPair.zero
h :
  (imageMonoFactorisation f).e ≫ limit.π (parallelPair (Y := cokernel f) (cokernel.π f) 0) WalkingParallelPair.zero = f
⊢ inv (imageMonoFactorisation f).e ≫ f =
    limit.π (parallelPair (Y := cokernel f) (cokernel.π f) 0) WalkingParallelPair.zero

Tactic:
rw [IsIso.inv_comp_eq, eq_comm]

Premises used: CategoryTheory.IsIso.inv_comp_eq, eq_comm
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : KernelFork (Y := cokernel f) (cokernel.π f)
e_1 : (s.pt ⟶ Y) = (s.pt ⟶ (parallelPair (Y := cokernel f) (cokernel.π f) 0).obj WalkingParallelPair.zero)
e_5 : Y = (parallelPair (Y := cokernel f) (cokernel.π f) 0).obj WalkingParallelPair.zero
⊢ (imageMonoFactorisation f).e ≫ limit.π (parallelPair (Y := cokernel f) (cokernel.π f) 0) WalkingParallelPair.zero = f

Tactic:
(imageMonoFactorisation f).fac

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : KernelFork (Y := cokernel f) (cokernel.π f)
e_1 : (s.pt ⟶ Y) = (s.pt ⟶ (parallelPair (Y := cokernel f) (cokernel.π f) 0).obj WalkingParallelPair.zero)
e_5 : Y = (parallelPair (Y := cokernel f) (cokernel.π f) 0).obj WalkingParallelPair.zero
⊢ (imageMonoFactorisation f).e ≫ limit.π (parallelPair (Y := cokernel f) (cokernel.π f) 0) WalkingParallelPair.zero = f

Tactic:
exact (imageMonoFactorisation f).fac

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
⊢ HasImages.{v, u} C

Tactic:
haveI : Limits.HasImages C := hasImages
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this : HasImages.{v, u} C
⊢ HasEqualizers.{v, u} C

Tactic:
haveI : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this : HasEqualizers.{v, u} C
⊢ HasZeroObject.{v, u} C

Tactic:
haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
refine_2 :
  (aux :
      ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f)),
        Cofork.π (CokernelCofork.ofπ f ⋯) ≫
            inv (imageMonoFactorisation f).m ≫
              CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
                (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
          Cofork.π s) →
    IsColimit (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯)
refine_1 :
  ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
      Cofork.π s
⊢ IsColimit (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯)

Tactic:
have aux (s : CokernelCofork (kernel.ι f)) :
            Cofork.π (CokernelCofork.ofπ _ (kernel.condition f)) ≫
              inv (imageMonoFactorisation f).m ≫ inv (Abelian.coimageImageComparison f) ≫
                colimit.desc (parallelPair (kernel.ι f) 0) s = Cofork.π s := ?_
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
aux :
  ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
      Cofork.π s
refine_2 :
  ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f))
    (m_1 : Cocone.pt (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯) ⟶ s.pt),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫ m_1 = Cofork.π s →
      m_1 =
        (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
            inv (imageMonoFactorisation f).m ≫
              CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
                (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
          s
⊢ IsColimit (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯)

Tactic:
refine isColimitAux _ (fun A => inv (imageMonoFactorisation f).m ≫
                  inv (Abelian.coimageImageComparison f) ≫ colimit.desc _ _) aux ?_

Premises used: CategoryTheory.Limits.isColimitAux, CategoryTheory.Limits.colimit.desc, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, OfNat.ofNat, CategoryTheory.Limits.parallelPair, CategoryTheory.Abelian.coimageImageComparison, CategoryTheory.Limits.kernel.ι
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
aux :
  ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
      Cofork.π s
A : CokernelCofork (X := kernel f) (kernel.ι f)
g : Cocone.pt (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯) ⟶ A.pt
hg : Cofork.π (CokernelCofork.ofπ f ⋯) ≫ g = Cofork.π A
⊢ f ≫ g = Cofork.π A

Tactic:
rw [CokernelCofork.π_ofπ] at hg

Premises used: CategoryTheory.Limits.CokernelCofork.π_ofπ
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
aux :
  ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
      Cofork.π s
A : CokernelCofork (X := kernel f) (kernel.ι f)
g : Cocone.pt (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯) ⟶ A.pt
hg : f ≫ g = Cofork.π A
refine_2 :
  f ≫ g =
    f ≫
      (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
          inv (imageMonoFactorisation f).m ≫
            CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
              (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
        A
refine_2₁ :
  Cofork.π A =
    f ≫
      (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
          inv (imageMonoFactorisation f).m ≫
            CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
              (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
        A
refine_2₂ :
  Cofork.π (CokernelCofork.ofπ f ⋯) ≫
      inv (imageMonoFactorisation f).m ≫
        CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
          (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A) =
    f ≫
      (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
          inv (imageMonoFactorisation f).m ≫
            CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
              (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
        A
refine_2₃ refine_2₄ :
  f ≫
      inv (imageMonoFactorisation f).m ≫
        CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
          (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A) =
    f ≫
      (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
          inv (imageMonoFactorisation f).m ≫
            CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
              (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
        A
⊢ g =
    (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
      A

Tactic:
rw [← cancel_epi f, hg, ← aux, CokernelCofork.π_ofπ]

Premises used: CategoryTheory.Limits.CokernelCofork.π_ofπ, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : CokernelCofork (X := kernel f) (kernel.ι f)
refine_1 :
  CategoryStruct.comp (Y := Abelian.coimage f) ((f ≫ inv (imageMonoFactorisation f).m) ≫ inv (coimageImageComparison f))
      (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
    Cofork.π s
⊢ Cofork.π (CokernelCofork.ofπ f ⋯) ≫
      inv (imageMonoFactorisation f).m ≫
        CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
          (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
    Cofork.π s

Tactic:
simp only [CokernelCofork.π_ofπ, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.CokernelCofork.π_ofπ
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : CokernelCofork (X := kernel f) (kernel.ι f)
⊢ CategoryStruct.comp (Y := colimit (parallelPair (X := kernel f) (kernel.ι f) 0))
      (colimit.ι (parallelPair (X := kernel f) (kernel.ι f) 0) WalkingParallelPair.one)
      (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
    s.ι.app WalkingParallelPair.one

Tactic:
colimit.ι_desc s WalkingParallelPair.one

Premises used: CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : CokernelCofork (X := kernel f) (kernel.ι f)
h :
  (X ⟶ s.pt) = ((parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt) →
    X = (parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one →
      Eq (α := X ⟶ Abelian.coimage f) ((f ≫ inv (imageMonoFactorisation f).m) ≫ inv (coimageImageComparison f))
        (colimit.ι (parallelPair (X := kernel f) (kernel.ι f) 0) WalkingParallelPair.one)
⊢ CategoryStruct.comp (Y := Abelian.coimage f) ((f ≫ inv (imageMonoFactorisation f).m) ≫ inv (coimageImageComparison f))
      (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
    Cofork.π s

Tactic:
convert! colimit.ι_desc s WalkingParallelPair.one using 2

Premises used: CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : CokernelCofork (X := kernel f) (kernel.ι f)
e_1 : (X ⟶ s.pt) = ((parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt)
e_3 : X = (parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one
h : (imageMonoFactorisation f).e ≫ (imageMonoFactorisation f).m = f
⊢ Eq (α := X ⟶ Abelian.coimage f) ((f ≫ inv (imageMonoFactorisation f).m) ≫ inv (coimageImageComparison f))
    (colimit.ι (parallelPair (X := kernel f) (kernel.ι f) 0) WalkingParallelPair.one)

Tactic:
rw [IsIso.comp_inv_eq, IsIso.comp_inv_eq, eq_comm, ← imageMonoFactorisation_e']

Premises used: eq_comm, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e', CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : CokernelCofork (X := kernel f) (kernel.ι f)
e_1 : (X ⟶ s.pt) = ((parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt)
e_3 : X = (parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one
⊢ (imageMonoFactorisation f).e ≫ (imageMonoFactorisation f).m = f

Tactic:
(imageMonoFactorisation f).fac

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : CokernelCofork (X := kernel f) (kernel.ι f)
e_1 : (X ⟶ s.pt) = ((parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt)
e_3 : X = (parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one
⊢ (imageMonoFactorisation f).e ≫ (imageMonoFactorisation f).m = f

Tactic:
exact (imageMonoFactorisation f).fac

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasFiniteBiproducts.{v, u} C

Tactic:
Limits.HasFiniteBiproducts.of_hasFiniteProducts

Premises used: CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasBinaryBiproducts.{v, u} C

Tactic:
Limits.hasBinaryBiproducts_of_finite_biproducts _

Premises used: CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasZeroObject.{v, u} C

Tactic:
hasZeroObject_of_hasInitial_object

Premises used: CategoryTheory.Limits.hasZeroObject_of_hasInitial_object
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
⊢ Epi (Y := Abelian.image f) (Abelian.factorThruImage f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : Mono f
⊢ IsIso (Y := Abelian.image f) (Abelian.factorThruImage f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
⊢ Mono (X := Abelian.coimage f) (Abelian.factorThruCoimage f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : Epi f
⊢ IsIso (X := Abelian.coimage f) (Abelian.factorThruCoimage f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
h : Eq (α := kernel f ⟶ P) (kernel.ι f) 0
⊢ Mono f

Tactic:
mono_of_kernel_zero h

Premises used: CategoryTheory.Preadditive.mono_of_kernel_zero
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
h : Eq (α := Q ⟶ cokernel f) (cokernel.π f) 0
⊢ Epi f

Tactic:
epi_of_cokernel_zero h

Premises used: CategoryTheory.Preadditive.epi_of_cokernel_zero
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
R : C
g : Q ⟶ R
h : f ≫ g = 0
⊢ CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (image.ι f ≫ g) = 0

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
R : C
g : Q ⟶ R
h : f ≫ g = 0
⊢ CategoryStruct.comp (Y := Abelian.coimage g) (f ≫ coimage.π g) (Abelian.factorThruCoimage g) = 0

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
⊢ Mono (X := Abelian.image f) (image.ι f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasStrongEpiMonoFactorisations.{v, u} C

Tactic:
HasStrongEpiMonoFactorisations.mk fun f => imageStrongEpiMonoFactorisation f

Premises used: CategoryTheory.Abelian.imageStrongEpiMonoFactorisation, CategoryTheory.Limits.HasStrongEpiMonoFactorisations.mk
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasImages.{v, u} C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasImageMaps.{v, u} C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f : X ⟶ Y
⊢ IsIso
    ((coimageStrongEpiMonoFactorisation f).toMonoIsImage.isoExt (imageStrongEpiMonoFactorisation f).toMonoIsImage).hom

Tactic:
Iso.isIso_hom
      (IsImage.isoExt (coimageStrongEpiMonoFactorisation f).toMonoIsImage
        (imageStrongEpiMonoFactorisation f).toMonoIsImage)

Premises used: CategoryTheory.Abelian.imageStrongEpiMonoFactorisation, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation, CategoryTheory.Limits.IsImage.isoExt, CategoryTheory.Iso.isIso_hom, CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage