awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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
refine_2 :
  (aux :
      ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
        (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
            Fork.ι (KernelFork.ofι f ⋯) =
          Fork.ι s) →
    IsLimit (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
⊢ IsLimit (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
have refine_1 : ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
  (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
      Fork.ι (KernelFork.ofι f sorry) =
    Fork.ι s
Tactic: have aux (s : KernelFork (cokernel.π f)) :
            (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
            Fork.ι (KernelFork.ofι _ (cokernel.condition f)) = Fork.ι s := ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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
aux :
  ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
    (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
⊢ IsLimit (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
have refine_2 : ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f))
  (m_1 : s.pt ⟶ Cone.pt (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f sorry)),
  m_1 ≫ Fork.ι (KernelFork.ofι f sorry) = Fork.ι s →
    m_1 =
      (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
          limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
        s
Tactic: refine isLimitAux _ (fun A => limit.lift _ _ ≫ inv (imageMonoFactorisation f).e) aux ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
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
aux :
  ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
    (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (Y := cokernel f) (cokernel.π f)
g : A.pt ⟶ Cone.pt (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
hg : g ≫ Fork.ι (KernelFork.ofι f ⋯) = Fork.ι A
⊢ g =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
        limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
      A
have hg₁ : g ≫ f = Fork.ι A
Tactic: rw [KernelFork.ι_ofι] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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
aux :
  ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
    (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (Y := cokernel f) (cokernel.π f)
g : A.pt ⟶ Cone.pt (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
hg : g ≫ f = Fork.ι A
⊢ g =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
        limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
      A
have refine_2 : g ≫ f =
  (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
        limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
      A ≫
    f
Tactic: rw [← cancel_mono f, hg, ← aux, KernelFork.ι_ofι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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
aux :
  ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
    (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (Y := cokernel f) (cokernel.π f)
g : A.pt ⟶ Cone.pt (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
hg : g ≫ f = Fork.ι A
refine_2 :
  g ≫ f =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
          limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
        A ≫
      f
⊢ g =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
        limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
      A
have refine_2₁ : Fork.ι A =
  (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
        limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
      A ≫
    f
Tactic: rw [← cancel_mono f, hg, ← aux, KernelFork.ι_ofι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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
aux :
  ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
    (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (Y := cokernel f) (cokernel.π f)
g : A.pt ⟶ Cone.pt (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
hg : g ≫ f = Fork.ι A
refine_2 :
  g ≫ f =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
          limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
        A ≫
      f
refine_2₁ :
  Fork.ι A =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
          limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
        A ≫
      f
⊢ g =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
        limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
      A
have refine_2₂ : (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) ≫
    Fork.ι (KernelFork.ofι f sorry) =
  (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
        limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
      A ≫
    f
Tactic: rw [← cancel_mono f, hg, ← aux, KernelFork.ι_ofι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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
aux :
  ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
    (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (Y := cokernel f) (cokernel.π f)
g : A.pt ⟶ Cone.pt (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
hg : g ≫ f = Fork.ι A
refine_2 :
  g ≫ f =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
          limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
        A ≫
      f
refine_2₁ :
  Fork.ι A =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
          limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
        A ≫
      f
refine_2₂ :
  (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) ≫
      Fork.ι (KernelFork.ofι f ⋯) =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
          limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
        A ≫
      f
⊢ g =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
        limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
      A
have refine_2₃ : (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) ≫ f =
  (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
        limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
      A ≫
    f
Tactic: rw [← cancel_mono f, hg, ← aux, KernelFork.ι_ofι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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)
⊢ (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
      Fork.ι (KernelFork.ofι f ⋯) =
    Fork.ι s
have refine_1 : limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e ≫ f = Fork.ι s
Tactic: simp only [KernelFork.ι_ofι, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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)
⊢ limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e ≫ f = Fork.ι s
have 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
Tactic: convert! limit.lift_π s WalkingParallelPair.zero using 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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
⊢ inv (imageMonoFactorisation f).e ≫ f =
    limit.π (parallelPair (Y := cokernel f) (cokernel.π f) 0) WalkingParallelPair.zero
have h : (imageMonoFactorisation f).e ≫ limit.π (parallelPair (Y := cokernel f) (cokernel.π f) 0) WalkingParallelPair.zero = f
Tactic: rw [IsIso.inv_comp_eq, eq_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
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
⊢ IsColimit (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯)
have this : HasImages.{v, u} C
Tactic: haveI : Limits.HasImages C := hasImages
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
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
⊢ IsColimit (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯)
have this₁ : HasEqualizers.{v, u} C
Tactic: haveI : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
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
⊢ IsColimit (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯)
have this₁ : HasZeroObject.{v, u} C
Tactic: haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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
⊢ IsColimit (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯)
have refine_2 : (aux :
    ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f)),
      Cofork.π (CokernelCofork.ofπ f sorry) ≫
          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 sorry)
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 := ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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 ⋯)
⊢ IsColimit (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯)
have refine_1 : ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f)),
  Cofork.π (CokernelCofork.ofπ f sorry) ≫
      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: 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 := ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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
⊢ IsColimit (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯)
have refine_2 : ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f))
  (m_1 : Cocone.pt (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f sorry) ⟶ s.pt),
  Cofork.π (CokernelCofork.ofπ f sorry) ≫ 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
Tactic: refine isColimitAux _ (fun A => inv (imageMonoFactorisation f).m ≫
                  inv (Abelian.coimageImageComparison f) ≫ colimit.desc _ _) aux ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
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
⊢ 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
have hg₁ : f ≫ g = Cofork.π A
Tactic: rw [CokernelCofork.π_ofπ] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [← cancel_epi f, hg, ← aux, CokernelCofork.π_ofπ]