awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : F.PreservesZeroMorphisms
hF : P.isoModSerre.IsInvertedBy F
X : C
hX : P X
f : 0 ⟶ X := 0
this : IsIso (F.map f)
⊢ F.kernel X

Tactic:
(asIso (F.map f)).isZero_iff.1 (F.map_isZero (isZero_zero C))

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Functor.map_isZero, CategoryTheory.Functor.map, CategoryTheory.Iso.isZero_iff, Iff.mp, CategoryTheory.ObjectProperty.inverseImage, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : F.PreservesZeroMorphisms
hF : P.isoModSerre.IsInvertedBy F
X : C
hX : P X
f : 0 ⟶ X := 0
this : IsIso (F.map f)
⊢ F.kernel X

Tactic:
exact (asIso (F.map f)).isZero_iff.1 (F.map_isZero (isZero_zero C))

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Functor.map_isZero, CategoryTheory.Functor.map, CategoryTheory.Iso.isZero_iff, Iff.mp, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
⊢ P.isoModSerre.IsInvertedBy F ↔ P ≤ F.kernel

Tactic:
⟨P.le_kernel_of_isoModSerre_isInvertedBy F, fun hF X Y f ⟨h₁, h₂⟩ ↦ ?_⟩

Premises used: CategoryTheory.IsIso, _private.0.CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff.match_1, CategoryTheory.Functor.map, CategoryTheory.ObjectProperty.le_kernel_of_isoModSerre_isInvertedBy, Iff.intro
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
refine :
  ∀ (hF : P ≤ F.kernel) (X Y : C) (f : X ⟶ Y),
    P.isoModSerre f → ∀ (h₁ : P.monoModSerre f) (h₂ : P.epiModSerre f), IsIso (F.map f)
⊢ P.isoModSerre.IsInvertedBy F ↔ P ≤ F.kernel

Tactic:
refine ⟨P.le_kernel_of_isoModSerre_isInvertedBy F, fun hF X Y f ⟨h₁, h₂⟩ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
hF : P ≤ F.kernel
X Y : C
f : X ⟶ Y
h : P.isoModSerre f
h₁ : P.monoModSerre f
h₂ : P.epiModSerre f
⊢ Mono (F.map f)

Tactic:
have : Mono (F.map f) :=
    (((ShortComplex.mk _ _ (kernel.condition f)).exact_of_f_is_kernel
      (kernelIsKernel f)).map F).mono_g (((hF _ h₁).eq_of_src _ _))
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
hF : P ≤ F.kernel
X Y : C
f : X ⟶ Y
h : P.isoModSerre f
h₁ : P.monoModSerre f
h₂ : P.epiModSerre f
this : Mono (F.map f)
⊢ Epi (F.map f)

Tactic:
have : Epi (F.map f) :=
    (((ShortComplex.mk _ _ (cokernel.condition f)).exact_of_g_is_cokernel
      (cokernelIsCokernel f)).map F).epi_f (((hF _ h₂).eq_of_tgt _ _))
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
hF : P ≤ F.kernel
X Y : C
f : X ⟶ Y
h : P.isoModSerre f
h₁ : P.monoModSerre f
h₂ : P.epiModSerre f
this_1 : Mono (F.map f)
this : Epi (F.map f)
⊢ IsIso (F.map f)

Tactic:
isIso_of_mono_of_epi (F.map f)

Premises used: CategoryTheory.Functor.map, CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
hF : P ≤ F.kernel
X Y : C
f : X ⟶ Y
h : P.isoModSerre f
h₁ : P.monoModSerre f
h₂ : P.epiModSerre f
this_1 : Mono (F.map f)
this : Epi (F.map f)
⊢ IsIso (F.map f)

Tactic:
exact isIso_of_mono_of_epi (F.map f)

Premises used: CategoryTheory.Functor.map, CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
⊢ (P.monoModSerre ⊓ P.epiModSerre).IsStableUnderBaseChange

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
⊢ (P.monoModSerre ⊓ P.epiModSerre).IsStableUnderCobaseChange

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.ShortExact
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
inst_6 : PreservesFiniteColimits F
inst_7 : PreservesFiniteLimits F
⊢ ShortComplex.ShortExact (S.map F) ↔ S.ShortExact

Tactic:
⟨reflects_shortExact_of_faithful F, fun h ↦ ShortComplex.ShortExact.map_of_exact h F⟩

Premises used: Iff.intro, CategoryTheory.ShortComplex.ShortExact.map_of_exact, CategoryTheory.ShortExact.reflects_shortExact_of_faithful
-- Module: Mathlib.CategoryTheory.Abelian.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : HasCokernels.{v_1, u_1} C
inst_5 : IsNormalEpiCategory.{v_1, u_1} C
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : P.ContainsZero
inst_8 : P.IsClosedUnderKernels
⊢ P.ι.PreservesMonomorphisms

Tactic:
have := P.preservesKernels_ι
  NormalEpiCategory.preservesMonomorphisms_of_preservesKernels P.ι

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.NormalEpiCategory.preservesMonomorphisms_of_preservesKernels, CategoryTheory.ObjectProperty.preservesKernels_ι
-- Module: Mathlib.CategoryTheory.Abelian.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : HasCokernels.{v_1, u_1} C
inst_5 : IsNormalMonoCategory.{v_1, u_1} C
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : P.ContainsZero
inst_8 : P.IsClosedUnderCokernels
⊢ P.ι.PreservesEpimorphisms

Tactic:
have := P.preservesCokernels_ι
  NormalMonoCategory.preservesEpimorphisms_of_preservesCokernels P.ι

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.NormalMonoCategory.preservesEpimorphisms_of_preservesCokernels, CategoryTheory.ObjectProperty.preservesCokernels_ι
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
refine_1 :
  Eq (α := (Subobject.{v, u} (op X))ᵒᵈ →o (Subobject.{v, u} (op X))ᵒᵈ)
    (OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X)) OrderHom.id
refine_2 :
  Eq (α := Subobject.{v, u} X →o Subobject.{v, u} X) (OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X)) OrderHom.id
⊢ Subobject.{v, u} X ≃o (Subobject.{v, u} (op X))ᵒᵈ

Tactic:
refine OrderIso.ofHomInv (cokernelOrderHom X) (kernelOrderHom X) ?_ ?_

Premises used: CategoryTheory.Limits.kernelOrderHom, CategoryTheory.Limits.cokernelOrderHom, OrderIso.ofHomInv
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ Eq (α := (Subobject.{v, u} (op X))ᵒᵈ →o (Subobject.{v, u} (op X))ᵒᵈ)
    (OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X)) OrderHom.id

Tactic:
OrderHom.ext _ _ (funext (Subobject.ind _ ?_))

Premises used: funext, OrderHom.ext, CategoryTheory.Subobject.ind
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
refine_1 :
  ∀ ⦃A : Cᵒᵖ⦄ (f : A ⟶ op X) [inst_2 : Mono f],
    Eq (α := (Subobject.{v, u} (op X))ᵒᵈ)
      ((OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X) : (a : (Subobject (op X))ᵒᵈ) → (Subobject (op X))ᵒᵈ)
          (Subobject.mk f) :
        (Subobject.{v, u} (op X))ᵒᵈ)
      ((OrderHom.id : (a : (Subobject (op X))ᵒᵈ) → (Subobject (op X))ᵒᵈ) (Subobject.mk f) : (Subobject.{v, u} (op X))ᵒᵈ)
⊢ Eq (α := (Subobject.{v, u} (op X))ᵒᵈ →o (Subobject.{v, u} (op X))ᵒᵈ)
    (OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X)) OrderHom.id

Tactic:
refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_))

Premises used: funext, OrderHom.ext, CategoryTheory.Subobject.ind
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
refine_1 :
  Subobject.mk (A := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
      (Quiver.Hom.op (cokernel.π (kernel.ι f.unop))) =
    Subobject.mk f
⊢ Eq (α := (Subobject.{v, u} (op X))ᵒᵈ)
    ((OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X) : (a : (Subobject (op X))ᵒᵈ) → (Subobject (op X))ᵒᵈ)
        (Subobject.mk f) :
      (Subobject.{v, u} (op X))ᵒᵈ)
    ((OrderHom.id : (a : (Subobject (op X))ᵒᵈ) → (Subobject (op X))ᵒᵈ) (Subobject.mk f) : (Subobject.{v, u} (op X))ᵒᵈ)

Tactic:
dsimp only [OrderHom.comp_coe, Function.comp_apply, kernelOrderHom_coe, Subobject.lift_mk,
      cokernelOrderHom_coe, OrderHom.id_coe, id]

Premises used: OrderHom.id_coe, id, CategoryTheory.Subobject.lift_mk, CategoryTheory.Limits.kernelOrderHom_coe, OrderHom.comp_coe, Function.comp_apply, CategoryTheory.Limits.cokernelOrderHom_coe
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ Subobject.mk (A := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
      (Quiver.Hom.op (cokernel.π (kernel.ι f.unop))) =
    Subobject.mk f

Tactic:
Subobject.mk_eq_mk_of_comm _ _
        ⟨?_, ?_, Quiver.Hom.unop_inj ?_, Quiver.Hom.unop_inj ?_⟩ ?_

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.Iso.mk, CategoryTheory.ThinSkeleton, Quiver.Hom.unop_inj, Quotient, OrderDual, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
refine_1 : op (cokernel (X := kernel f.unop) (kernel.ι f.unop)) ⟶ A
refine_1₁ : A ⟶ op (cokernel (X := kernel f.unop) (kernel.ι f.unop))
refine_1₂ :
  Eq.{v + 1} (α :=
    unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))) ⟶
      unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯) ≫
        Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯)))
    (Quiver.Hom.unop (𝟙 (op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))))
refine_1₃ :
  Eq.{v + 1} (α := unop A ⟶ unop A)
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
        (Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯))
        (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯))))
    (Quiver.Hom.unop (𝟙 A))
refine_1₄ :
  Eq (α := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)) ⟶ op X)
    (Iso.hom
        { hom := Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯),
          inv := Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯), hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      f)
    (Quiver.Hom.op (cokernel.π (kernel.ι f.unop)))
⊢ Subobject.mk (A := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
      (Quiver.Hom.op (cokernel.π (kernel.ι f.unop))) =
    Subobject.mk f

Tactic:
refine Subobject.mk_eq_mk_of_comm _ _
        ⟨?_, ?_, Quiver.Hom.unop_inj ?_, Quiver.Hom.unop_inj ?_⟩ ?_

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.Iso.mk
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ op (cokernel (X := kernel f.unop) (kernel.ι f.unop)) ⟶ A

Tactic:
exact (Abelian.epiDesc f.unop _ (cokernel.condition (kernel.ι f.unop))).op

Premises used: Quiver.Hom.op, CategoryTheory.Abelian.epiDesc, Quiver.Hom.unop, CategoryTheory.Limits.cokernel.condition, CategoryTheory.Limits.kernel.ι
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ A ⟶ op (cokernel (X := kernel f.unop) (kernel.ι f.unop))

Tactic:
exact (cokernel.desc _ _ (kernel.condition f.unop)).op

Premises used: CategoryTheory.Limits.cokernel.desc, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Limits.kernel.condition
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
refine_1 :
  Eq (α := unop (op X) ⟶ unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))
    (CategoryStruct.comp (Y := cokernel (X := kernel f.unop) (kernel.ι f.unop)) (cokernel.π (kernel.ι f.unop))
      (Quiver.Hom.unop
        (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯) ≫
          Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯))))
    (CategoryStruct.comp (Y := cokernel (X := kernel f.unop) (kernel.ι f.unop)) (cokernel.π (kernel.ι f.unop))
      (Quiver.Hom.unop (𝟙 (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))))
⊢ Eq.{v + 1} (α :=
    unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))) ⟶
      unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯) ≫
        Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯)))
    (Quiver.Hom.unop (𝟙 (op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))))

Tactic:
rw [← cancel_epi (cokernel.π (kernel.ι f.unop))]

Premises used: Quiver.Hom.unop, CategoryTheory.Limits.cokernel.π, CategoryTheory.cancel_epi, CategoryTheory.Limits.kernel.ι
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ Eq (α := unop (op X) ⟶ unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))
    (CategoryStruct.comp (Y := cokernel (X := kernel f.unop) (kernel.ι f.unop)) (cokernel.π (kernel.ι f.unop))
      (Quiver.Hom.unop
        (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯) ≫
          Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯))))
    (CategoryStruct.comp (Y := cokernel (X := kernel f.unop) (kernel.ι f.unop)) (cokernel.π (kernel.ι f.unop))
      (Quiver.Hom.unop (𝟙 (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))))

Tactic:
simp only [unop_comp, Quiver.Hom.unop_op, unop_id_op, cokernel.π_desc_assoc,
        comp_epiDesc, Category.comp_id]

Premises used: CategoryTheory.Abelian.comp_epiDesc, Quiver.Hom.unop_op, CategoryTheory.Limits.cokernel.π_desc_assoc, CategoryTheory.unop_comp, CategoryTheory.Category.comp_id, CategoryTheory.unop_id_op
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ Eq.{v + 1} (α := unop A ⟶ unop A)
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
        (Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯))
        (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯))))
    (Quiver.Hom.unop (𝟙 A))

Tactic:
simp only [← cancel_epi f.unop, unop_comp, Quiver.Hom.unop_op, unop_id, comp_epiDesc_assoc,
        cokernel.π_desc, Category.comp_id]

Premises used: Quiver.Hom.unop_op, Quiver.Hom.unop, CategoryTheory.unop_comp, CategoryTheory.Category.comp_id, CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Abelian.comp_epiDesc_assoc, CategoryTheory.cancel_epi, CategoryTheory.unop_id
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ Eq (α := unop (op X) ⟶ unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))
    (Quiver.Hom.unop
      (Iso.hom
          { hom := Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯),
            inv := Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯), hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
        f))
    (Quiver.Hom.unop (Quiver.Hom.op (cokernel.π (kernel.ι f.unop))))

Tactic:
simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc]

Premises used: CategoryTheory.Abelian.comp_epiDesc, Quiver.Hom.unop_op, CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ Eq (α := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)) ⟶ op X)
    (Iso.hom
        { hom := Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯),
          inv := Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯), hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      f)
    (Quiver.Hom.op (cokernel.π (kernel.ι f.unop)))

Tactic:
exact Quiver.Hom.unop_inj (by simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc])

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ Eq (α := Subobject.{v, u} X →o Subobject.{v, u} X) (OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X)) OrderHom.id

Tactic:
OrderHom.ext _ _ (funext (Subobject.ind _ ?_))

Premises used: funext, OrderHom.ext, CategoryTheory.Subobject.ind
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
refine_2 :
  ∀ ⦃A : C⦄ (f : A ⟶ X) [inst_2 : Mono f],
    Eq (α := Subobject.{v, u} X)
      ((OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X) : (a : Subobject X) → Subobject X) (Subobject.mk f) :
        Subobject.{v, u} X)
      ((OrderHom.id : (a : Subobject X) → Subobject X) (Subobject.mk f) : Subobject.{v, u} X)
⊢ Eq (α := Subobject.{v, u} X →o Subobject.{v, u} X) (OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X)) OrderHom.id

Tactic:
refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_))

Premises used: funext, OrderHom.ext, CategoryTheory.Subobject.ind
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
refine_2 : Subobject.mk (A := kernel (Y := cokernel f) (cokernel.π f)) (kernel.ι (cokernel.π f)) = Subobject.mk f
⊢ Eq (α := Subobject.{v, u} X)
    ((OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X) : (a : Subobject X) → Subobject X) (Subobject.mk f) :
      Subobject.{v, u} X)
    ((OrderHom.id : (a : Subobject X) → Subobject X) (Subobject.mk f) : Subobject.{v, u} X)

Tactic:
dsimp only [OrderHom.comp_coe, Function.comp_apply, cokernelOrderHom_coe, Subobject.lift_mk,
      kernelOrderHom_coe, OrderHom.id_coe, id, unop_op, Quiver.Hom.unop_op]

Premises used: OrderHom.id_coe, Quiver.Hom.unop_op, id, CategoryTheory.Subobject.lift_mk, CategoryTheory.Limits.kernelOrderHom_coe, OrderHom.comp_coe, Opposite.unop_op, Function.comp_apply, CategoryTheory.Limits.cokernelOrderHom_coe
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
⊢ Subobject.mk (A := kernel (Y := cokernel f) (cokernel.π f)) (kernel.ι (cokernel.π f)) = Subobject.mk f

Tactic:
Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.Iso.mk
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
refine_2 : kernel (Y := cokernel f) (cokernel.π f) ⟶ A
refine_2₁ : A ⟶ kernel (Y := cokernel f) (cokernel.π f)
refine_2₂ :
  monoLift f (kernel.ι (cokernel.π f)) ⋯ ≫ kernel.lift (cokernel.π f) f ⋯ = 𝟙 (kernel (Y := cokernel f) (cokernel.π f))
refine_2₃ :
  CategoryStruct.comp (Y := kernel (Y := cokernel f) (cokernel.π f)) (kernel.lift (cokernel.π f) f ⋯)
      (monoLift f (kernel.ι (cokernel.π f)) ⋯) =
    𝟙 A
refine_2₄ :
  Eq (α := kernel (Y := cokernel f) (cokernel.π f) ⟶ X)
    (Iso.hom
        { hom := monoLift f (kernel.ι (cokernel.π f)) ⋯, inv := kernel.lift (cokernel.π f) f ⋯, hom_inv_id := ⋯,
          inv_hom_id := ⋯ } ≫
      f)
    (kernel.ι (cokernel.π f))
⊢ Subobject.mk (A := kernel (Y := cokernel f) (cokernel.π f)) (kernel.ι (cokernel.π f)) = Subobject.mk f

Tactic:
refine Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.Iso.mk
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel (Y := cokernel f) (cokernel.π f) ⟶ A

Tactic:
exact Abelian.monoLift f _ (kernel.condition (cokernel.π f))

Premises used: CategoryTheory.Limits.kernel.condition, CategoryTheory.Abelian.monoLift, CategoryTheory.Limits.cokernel.π
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
⊢ A ⟶ kernel (Y := cokernel f) (cokernel.π f)

Tactic:
exact kernel.lift _ _ (cokernel.condition f)

Premises used: CategoryTheory.Limits.cokernel.condition, CategoryTheory.Limits.kernel.lift
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
⊢ monoLift f (kernel.ι (cokernel.π f)) ⋯ ≫ kernel.lift (cokernel.π f) f ⋯ = 𝟙 (kernel (Y := cokernel f) (cokernel.π f))

Tactic:
simp only [← cancel_mono (kernel.ι (cokernel.π f)), Category.assoc, image.fac, monoLift_comp,
        Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.image.fac, CategoryTheory.Abelian.monoLift_comp, CategoryTheory.cancel_mono, CategoryTheory.Limits.cokernel.π, CategoryTheory.Limits.kernel.ι, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
⊢ CategoryStruct.comp (Y := kernel (Y := cokernel f) (cokernel.π f)) (kernel.lift (cokernel.π f) f ⋯)
      (monoLift f (kernel.ι (cokernel.π f)) ⋯) =
    𝟙 A

Tactic:
simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.image.fac, CategoryTheory.Abelian.monoLift_comp, CategoryTheory.cancel_mono, CategoryTheory.Category.id_comp