awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
X' : C
f : X' ⟶ X
inst_2 : IsIso f
g : X ⟶ Y
inst_3 : HasKernel g
⊢ Iso.hom (kernelSubobjectIsoComp f g) ≫ (kernelSubobject g).arrow = (kernelSubobject (f ≫ g)).arrow ≫ f

Tactic:
simp [kernelSubobjectIsoComp]

Premises used: CategoryTheory.Limits.kernelSubobjectIsoComp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
X' : C
f : X' ⟶ X
inst_2 : IsIso f
g : X ⟶ Y
inst_3 : HasKernel g
⊢ Iso.inv (kernelSubobjectIsoComp f g) ≫ (kernelSubobject (f ≫ g)).arrow = (kernelSubobject g).arrow ≫ inv f

Tactic:
simp [kernelSubobjectIsoComp]

Premises used: CategoryTheory.Limits.kernelSubobjectIsoComp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X ⟶ Y
inst_2 : HasKernel f
Z : C
h : Y ⟶ Z
inst_3 : HasKernel (f ≫ h)
⊢ (kernelSubobject f).arrow ≫ f ≫ h = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X ⟶ Y
inst_2 : HasKernel f
Z : C
h : Y ⟶ Z
inst_3 : Mono h
⊢ ((kernelSubobject (f ≫ h)).arrow ≫ f) ≫ h = 0 ≫ h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z_1 : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X ⟶ Y
inst_2 : HasKernel f_1
f : X ⟶ Y
inst_3 : HasKernel f
Z : C
h : Y ⟶ Z
inst_4 : Mono h
rw :
  IsIso (X := Functor.obj underlying (kernelSubobject f)) (Y := Functor.obj underlying (kernelSubobject (f ≫ h)))
    (Iso.hom (underlyingIso (kernel.ι f)) ≫
        CategoryStruct.comp (Y := kernel (f ≫ h)) (Iso.inv (kernelCompMono f h) : kernel f ⟶ kernel (f ≫ h))
          (Iso.inv (underlyingIso (kernel.ι (f ≫ h))) :
            kernel (f ≫ h) ⟶ Functor.obj underlying (Subobject.mk (A := kernel (f ≫ h)) (kernel.ι (f ≫ h)))) :
      Functor.obj underlying (Subobject.mk (A := kernel f) (kernel.ι f)) ⟶
        Functor.obj underlying (Subobject.mk (A := kernel (f ≫ h)) (kernel.ι (f ≫ h))))
rw₁ :
  Eq (α := kernel f ⟶ X)
    (CategoryStruct.comp (Y := kernel (f ≫ h)) (Iso.inv (kernelCompMono f h) : kernel f ⟶ kernel (f ≫ h))
      (kernel.ι (f ≫ h) : kernel (f ≫ h) ⟶ X))
    (kernel.ι f)
⊢ IsIso (Y := Functor.obj underlying (kernelSubobject (f ≫ h))) ((kernelSubobject f).ofLE (kernelSubobject (f ≫ h)) ⋯)

Tactic:
rw [ofLE_mk_le_mk_of_comm (kernelCompMono f h).inv]

Premises used: CategoryTheory.Limits.kernelCompMono, CategoryTheory.Subobject.ofLE_mk_le_mk_of_comm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z_1 : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X ⟶ Y
inst_2 : HasKernel f_1
f : X ⟶ Y
inst_3 : HasKernel f
Z : C
h : Y ⟶ Z
inst_4 : Mono h
⊢ IsIso (X := Functor.obj underlying (kernelSubobject f)) (Y := Functor.obj underlying (kernelSubobject (f ≫ h)))
    (Iso.hom (underlyingIso (kernel.ι f)) ≫
        CategoryStruct.comp (Y := kernel (f ≫ h)) (Iso.inv (kernelCompMono f h) : kernel f ⟶ kernel (f ≫ h))
          (Iso.inv (underlyingIso (kernel.ι (f ≫ h))) :
            kernel (f ≫ h) ⟶ Functor.obj underlying (Subobject.mk (A := kernel (f ≫ h)) (kernel.ι (f ≫ h)))) :
      Functor.obj underlying (Subobject.mk (A := kernel f) (kernel.ι f)) ⟶
        Functor.obj underlying (Subobject.mk (A := kernel (f ≫ h)) (kernel.ι (f ≫ h))))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z_1 : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X ⟶ Y
inst_2 : HasKernel f_1
f : X ⟶ Y
inst_3 : HasKernel f
Z : C
h : Y ⟶ Z
inst_4 : Mono h
⊢ Eq (α := kernel f ⟶ X)
    (CategoryStruct.comp (Y := kernel (f ≫ h)) (Iso.inv (kernelCompMono f h) : kernel f ⟶ kernel (f ≫ h))
      (kernel.ι (f ≫ h) : kernel (f ≫ h) ⟶ X))
    (kernel.ι f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasCokernels.{v, u} C
X A B : C
g : B ⟶ X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Eq (α := (Subobject.{v, u} (op X))ᵒᵈ)
    ((fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦
        (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)) : Subobject.{v, u} (op X)))
      A (i.hom ≫ g) hf)
    ((fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦
        (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)) : Subobject.{v, u} (op X)))
      B g hg)

Tactic:
Subobject.mk_eq_mk_of_comm _ _ (Iso.op ?_) (Quiver.Hom.unop_inj ?_)

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.Iso.op, CategoryTheory.ThinSkeleton, Quiver.Hom.unop_inj, Quotient, OrderDual, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasCokernels.{v, u} C
X A B : C
g : B ⟶ X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
refine_1 : cokernel g ≅ cokernel (i.hom ≫ g)
refine_2 :
  Eq (α := unop (op X) ⟶ unop (op (cokernel (i.hom ≫ g))))
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := op (cokernel g))
        (Iso.hom
          (Iso.op
            (Iso.symm
              (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair (i.hom ≫ g) 0))
                (isCokernelEpiComp (colimit.isColimit (parallelPair g 0)) i.hom ⋯)))))
        (Quiver.Hom.op (cokernel.π g))))
    (Quiver.Hom.unop (Quiver.Hom.op (cokernel.π (i.hom ≫ g))))
⊢ Eq (α := (Subobject.{v, u} (op X))ᵒᵈ)
    ((fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦
        (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)) : Subobject.{v, u} (op X)))
      A (i.hom ≫ g) hf)
    ((fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦
        (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)) : Subobject.{v, u} (op X)))
      B g hg)

Tactic:
refine Subobject.mk_eq_mk_of_comm _ _ (Iso.op ?_) (Quiver.Hom.unop_inj ?_)

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.Iso.op, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasCokernels.{v, u} C
X A B : C
g : B ⟶ X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ cokernel g ≅ cokernel (i.hom ≫ g)

Tactic:
exact (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
            (isCokernelEpiComp (colimit.isColimit _) i.hom rfl)).symm

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.isCokernelEpiComp, CategoryTheory.Iso.symm, CategoryTheory.Iso.hom, rfl, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasCokernels.{v, u} C
X A B : C
g : B ⟶ X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Eq (α := unop (op X) ⟶ unop (op (cokernel (i.hom ≫ g))))
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := op (cokernel g))
        (Iso.hom
          (Iso.op
            (Iso.symm
              (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair (i.hom ≫ g) 0))
                (isCokernelEpiComp (colimit.isColimit (parallelPair g 0)) i.hom ⋯)))))
        (Quiver.Hom.op (cokernel.π g))))
    (Quiver.Hom.unop (Quiver.Hom.op (cokernel.π (i.hom ≫ g))))

Tactic:
simp only [Iso.comp_inv_eq, Iso.op_hom, Iso.symm_hom, unop_comp, Quiver.Hom.unop_op,
            colimit.comp_coconePointUniqueUpToIso_hom, Cofork.ofπ_ι_app,
            coequalizer.cofork_π]

Premises used: CategoryTheory.Iso.comp_inv_eq, Quiver.Hom.unop_op, CategoryTheory.Iso.op_hom, CategoryTheory.Iso.symm_hom, CategoryTheory.unop_comp, CategoryTheory.Limits.coequalizer.cofork_π, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.Cofork.ofπ_ι_app
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
dsimp :
  LE.le (α := (Subobject.{v, u} (op X))ᵒᵈ) (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)))
    (Subobject.mk (A := op (cokernel g)) (Quiver.Hom.op (cokernel.π g)))
⊢ Subobject.lift
      (fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦ Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f))) ⋯
      (Subobject.mk f) ≤
    Subobject.lift
      (fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦ Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f))) ⋯
      (Subobject.mk g)

Tactic:
dsimp only [Subobject.lift_mk]

Premises used: CategoryTheory.Subobject.lift_mk
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ LE.le (α := (Subobject.{v, u} (op X))ᵒᵈ) (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)))
    (Subobject.mk (A := op (cokernel g)) (Quiver.Hom.op (cokernel.π g)))

Tactic:
Subobject.mk_le_mk_of_comm (cokernel.desc f (cokernel.π g) ?_).op ?_

Premises used: CategoryTheory.Limits.cokernel.desc, Quiver.Hom.op, CategoryTheory.Subobject.mk_le_mk_of_comm, CategoryTheory.Limits.cokernel.π
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := A ⟶ cokernel g) (f ≫ cokernel.π g) 0
refine_2 :
  Eq.{v + 1} (α := op (cokernel g) ⟶ op X)
    (CategoryStruct.comp (Y := op (cokernel f)) (Quiver.Hom.op (cokernel.desc f (cokernel.π g) ⋯))
      (Quiver.Hom.op (cokernel.π f)))
    (Quiver.Hom.op (cokernel.π g))
⊢ LE.le (α := (Subobject.{v, u} (op X))ᵒᵈ) (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)))
    (Subobject.mk (A := op (cokernel g)) (Quiver.Hom.op (cokernel.π g)))

Tactic:
refine Subobject.mk_le_mk_of_comm (cokernel.desc f (cokernel.π g) ?_).op ?_

Premises used: CategoryTheory.Limits.cokernel.desc, Quiver.Hom.op, CategoryTheory.Subobject.mk_le_mk_of_comm, CategoryTheory.Limits.cokernel.π
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := A ⟶ cokernel g) ((ofMkLEMk f g h ≫ g) ≫ cokernel.π g) 0
refine_1₁ : Eq (α := A ⟶ cokernel g) (ofMkLEMk f g h ≫ g ≫ cokernel.π g) 0
refine_1₂ : Eq (α := A ⟶ cokernel g) (ofMkLEMk f g h ≫ 0) 0
refine_1₃ refine_1₄ : Eq.{v + 1} (α := A ⟶ cokernel g) 0 0
⊢ Eq (α := A ⟶ cokernel g) (f ≫ cokernel.π g) 0

Tactic:
rw [← Subobject.ofMkLEMk_comp h, Category.assoc, cokernel.condition, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.cokernel.condition, CategoryTheory.Subobject.ofMkLEMk_comp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Eq.{v + 1} (α := op (cokernel g) ⟶ op X)
    (CategoryStruct.comp (Y := op (cokernel f)) (Quiver.Hom.op (cokernel.desc f (cokernel.π g) ⋯))
      (Quiver.Hom.op (cokernel.π f)))
    (Quiver.Hom.op (cokernel.π g))

Tactic:
Quiver.Hom.unop_inj (cokernel.π_desc _ _ _)

Premises used: CategoryTheory.Limits.cokernel.π_desc, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Eq.{v + 1} (α := op (cokernel g) ⟶ op X)
    (CategoryStruct.comp (Y := op (cokernel f)) (Quiver.Hom.op (cokernel.desc f (cokernel.π g) ⋯))
      (Quiver.Hom.op (cokernel.π f)))
    (Quiver.Hom.op (cokernel.π g))

Tactic:
exact Quiver.Hom.unop_inj (cokernel.π_desc _ _ _)

Premises used: CategoryTheory.Limits.cokernel.π_desc, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Eq (α := Subobject.{v, u} X)
    ((fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) A (i.hom ≫ g)
      hf)
    ((fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) B g hg)

Tactic:
Subobject.mk_eq_mk_of_comm _ _ ?_ ?_

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
refine_1 : kernel (i.hom ≫ g).unop ≅ kernel g.unop
refine_2 :
  Eq (α := kernel (i.hom ≫ g).unop ⟶ X)
    (CategoryStruct.comp (Y := kernel g.unop)
      (Iso.hom
        (IsLimit.conePointUniqueUpToIso (limit.isLimit (parallelPair (g.unop ≫ i.unop.hom) 0))
          (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom ⋯)))
      (kernel.ι g.unop))
    (kernel.ι (i.hom ≫ g).unop)
⊢ Eq (α := Subobject.{v, u} X)
    ((fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) A (i.hom ≫ g)
      hf)
    ((fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) B g hg)

Tactic:
refine Subobject.mk_eq_mk_of_comm _ _ ?_ ?_

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ kernel (i.hom ≫ g).unop ≅ kernel g.unop

Tactic:
exact
            IsLimit.conePointUniqueUpToIso (limit.isLimit _)
              (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom rfl)

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, Quiver.Hom.unop, CategoryTheory.Limits.limit.isLimit, OfNat.ofNat, CategoryTheory.Limits.isKernelCompMono, CategoryTheory.Iso.hom, CategoryTheory.Limits.parallelPair, rfl, CategoryTheory.Iso.unop
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
refine_2 :
  Eq (α := kernel (g.unop ≫ i.hom.unop) ⟶ X)
    (CategoryStruct.comp (Y := kernel g.unop)
      (Iso.hom
        (IsLimit.conePointUniqueUpToIso (limit.isLimit (parallelPair (g.unop ≫ i.hom.unop) 0))
          (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.hom.unop ⋯)))
      (kernel.ι g.unop))
    (kernel.ι (g.unop ≫ i.hom.unop))
⊢ Eq (α := kernel (i.hom ≫ g).unop ⟶ X)
    (CategoryStruct.comp (Y := kernel g.unop)
      (Iso.hom
        (IsLimit.conePointUniqueUpToIso (limit.isLimit (parallelPair (g.unop ≫ i.unop.hom) 0))
          (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom ⋯)))
      (kernel.ι g.unop))
    (kernel.ι (i.hom ≫ g).unop)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Eq (α := kernel (g.unop ≫ i.hom.unop) ⟶ X)
    (CategoryStruct.comp (Y := kernel g.unop)
      (Iso.hom
        (IsLimit.conePointUniqueUpToIso (limit.isLimit (parallelPair (g.unop ≫ i.hom.unop) 0))
          (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.hom.unop ⋯)))
      (kernel.ι g.unop))
    (kernel.ι (g.unop ≫ i.hom.unop))

Tactic:
simp only [← Iso.eq_inv_comp, limit.conePointUniqueUpToIso_inv_comp,
            Fork.ofι_π_app]

Premises used: CategoryTheory.Limits.Fork.ofι_π_app, CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
dsimp : Subobject.mk (A := kernel f.unop) (kernel.ι f.unop) ≤ Subobject.mk (A := kernel g.unop) (kernel.ι g.unop)
⊢ Subobject.lift (fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) ⋯
      (Subobject.mk f) ≤
    Subobject.lift (fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) ⋯
      (Subobject.mk g)

Tactic:
dsimp only [Subobject.lift_mk]

Premises used: CategoryTheory.Subobject.lift_mk
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop) ≤ Subobject.mk (A := kernel g.unop) (kernel.ι g.unop)

Tactic:
Subobject.mk_le_mk_of_comm (kernel.lift g.unop (kernel.ι f.unop) ?_) ?_

Premises used: CategoryTheory.Subobject.mk_le_mk_of_comm, Quiver.Hom.unop, CategoryTheory.Limits.kernel.ι, CategoryTheory.Limits.kernel.lift
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ g.unop) 0
refine_2 :
  Eq (α := kernel f.unop ⟶ X)
    (CategoryStruct.comp (Y := kernel g.unop) (kernel.lift g.unop (kernel.ι f.unop) ⋯) (kernel.ι g.unop))
    (kernel.ι f.unop)
⊢ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop) ≤ Subobject.mk (A := kernel g.unop) (kernel.ι g.unop)

Tactic:
refine Subobject.mk_le_mk_of_comm (kernel.lift g.unop (kernel.ι f.unop) ?_) ?_

Premises used: CategoryTheory.Subobject.mk_le_mk_of_comm, Quiver.Hom.unop, CategoryTheory.Limits.kernel.ι, CategoryTheory.Limits.kernel.lift
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ (ofMkLEMk g f h ≫ f).unop) 0
refine_1₁ : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ f.unop ≫ (ofMkLEMk g f h).unop) 0
refine_1₂ : Eq (α := kernel f.unop ⟶ unop B) (0 ≫ (ofMkLEMk g f h).unop) 0
refine_1₃ refine_1₄ : Eq.{v + 1} (α := kernel f.unop ⟶ unop B) 0 0
⊢ Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ g.unop) 0

Tactic:
rw [← Subobject.ofMkLEMk_comp h, unop_comp, kernel.condition_assoc, zero_comp]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Subobject.ofMkLEMk_comp, CategoryTheory.Limits.kernel.condition_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Eq (α := op X ⟶ op (kernel f.unop))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y := kernel g.unop) (kernel.lift g.unop (kernel.ι f.unop) ⋯) (kernel.ι g.unop)))
    (Quiver.Hom.op (kernel.ι f.unop))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Eq (α := kernel f.unop ⟶ X)
    (CategoryStruct.comp (Y := kernel g.unop) (kernel.lift g.unop (kernel.ι f.unop) ⋯) (kernel.ι g.unop))
    (kernel.ι f.unop)

Tactic:
exact Quiver.Hom.op_inj (by simp)

Premises used: Quiver.Hom.op_inj
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
⊢ Iso.hom (imageSubobjectIso f) ≫ image.ι f = (imageSubobject f).arrow

Tactic:
simp [imageSubobjectIso]

Premises used: CategoryTheory.Limits.imageSubobjectIso
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
⊢ Iso.inv (imageSubobjectIso f) ≫ (imageSubobject f).arrow = image.ι f

Tactic:
simp [imageSubobjectIso]

Premises used: CategoryTheory.Limits.imageSubobjectIso
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasEqualizers.{v, u} C
dsimp : Epi (Y := Functor.obj underlying (imageSubobject f)) (factorThruImage f ≫ Iso.inv (imageSubobjectIso f))
⊢ Epi (Y := Functor.obj underlying (imageSubobject f)) (factorThruImageSubobject f)

Tactic:
dsimp [factorThruImageSubobject]

Premises used: CategoryTheory.Limits.factorThruImageSubobject
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasEqualizers.{v, u} C
⊢ Epi (Y := Functor.obj underlying (imageSubobject f)) (factorThruImage f ≫ Iso.inv (imageSubobjectIso f))

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
⊢ factorThruImageSubobject f ≫ (imageSubobject f).arrow = f

Tactic:
simp [factorThruImageSubobject]

Premises used: CategoryTheory.Limits.factorThruImageSubobject
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : HasImage f
inst_3 : Epi (Y := Functor.obj underlying (imageSubobject f)) (factorThruImageSubobject f)
h : f ≫ g = 0
⊢ factorThruImageSubobject f ≫ (imageSubobject f).arrow ≫ g = 0

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
W : C
k : W ⟶ X
⊢ (k ≫ factorThruImage f) ≫ (MonoOver.mk (A := image f) (image.ι f)).arrow = k ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
W : C
k : W ⟶ X
h : (imageSubobject f).Factors (k ≫ f)
h₁ :
  (imageSubobject f).factorThru (k ≫ f) h ≫ (imageSubobject f).arrow =
    (k ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow
⊢ (imageSubobject f).factorThru (k ≫ f) h = k ≫ factorThruImageSubobject f

Tactic:
ext