[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ Subobject X ≃o (Subobject (op X))ᵒᵈ
[PROOFSTEP]
refine' OrderIso.ofHomInv (cokernelOrderHom X) (kernelOrderHom X) _ _
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ OrderHom.comp ↑(cokernelOrderHom X) ↑(kernelOrderHom X) = OrderHom.id
[PROOFSTEP]
change (cokernelOrderHom X).comp (kernelOrderHom X) = _
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X) = OrderHom.id
[PROOFSTEP]
refine' OrderHom.ext _ _ (funext (Subobject.ind _ _))
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ ∀ ⦃A : Cᵒᵖ⦄ (f : A ⟶ op X) [inst : Mono f],
    ↑(OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X)) (Subobject.mk f) = ↑OrderHom.id (Subobject.mk f)
[PROOFSTEP]
intro A f hf
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ↑(OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X)) (Subobject.mk f) = ↑OrderHom.id (Subobject.mk f)
[PROOFSTEP]
dsimp only [OrderHom.comp_coe, Function.comp_apply, kernelOrderHom_coe, Subobject.lift_mk, cokernelOrderHom_coe,
  OrderHom.id_coe, id.def]
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ Subobject.mk (cokernel.π (kernel.ι f.unop)).op = Subobject.mk f
[PROOFSTEP]
refine' Subobject.mk_eq_mk_of_comm _ _ ⟨_, _, Quiver.Hom.unop_inj _, Quiver.Hom.unop_inj _⟩ _
[GOAL]
case refine'_1.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ op (cokernel (kernel.ι f.unop)) ⟶ A
[PROOFSTEP]
exact (Abelian.epiDesc f.unop _ (cokernel.condition (kernel.ι f.unop))).op
[GOAL]
case refine'_1.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ A ⟶ op (cokernel (kernel.ι f.unop))
[PROOFSTEP]
exact (cokernel.desc _ _ (kernel.condition f.unop)).op
[GOAL]
case refine'_1.refine'_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) (_ : kernel.ι f.unop ≫ cokernel.π (kernel.ι f.unop) = 0)).op ≫
        (cokernel.desc (kernel.ι f.unop) f.unop (_ : kernel.ι f.unop ≫ f.unop = 0)).op).unop =
    (𝟙 (op (cokernel (kernel.ι f.unop)))).unop
[PROOFSTEP]
rw [← cancel_epi (cokernel.π (kernel.ι f.unop))]
[GOAL]
case refine'_1.refine'_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ cokernel.π (kernel.ι f.unop) ≫
      ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) (_ : kernel.ι f.unop ≫ cokernel.π (kernel.ι f.unop) = 0)).op ≫
          (cokernel.desc (kernel.ι f.unop) f.unop (_ : kernel.ι f.unop ≫ f.unop = 0)).op).unop =
    cokernel.π (kernel.ι f.unop) ≫ (𝟙 (op (cokernel (kernel.ι f.unop)))).unop
[PROOFSTEP]
simp only [unop_comp, Quiver.Hom.unop_op, unop_id_op, cokernel.π_desc_assoc, comp_epiDesc, Category.comp_id]
[GOAL]
case refine'_1.refine'_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernel.desc (kernel.ι f.unop) f.unop (_ : kernel.ι f.unop ≫ f.unop = 0)).op ≫
        (epiDesc f.unop (cokernel.π (kernel.ι f.unop))
            (_ : kernel.ι f.unop ≫ cokernel.π (kernel.ι f.unop) = 0)).op).unop =
    (𝟙 A).unop
[PROOFSTEP]
simp only [← cancel_epi f.unop, unop_comp, Quiver.Hom.unop_op, unop_id, comp_epiDesc_assoc, cokernel.π_desc,
  Category.comp_id]
[GOAL]
case refine'_1.refine'_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ (Iso.mk (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) (_ : kernel.ι f.unop ≫ cokernel.π (kernel.ι f.unop) = 0)).op
          (cokernel.desc (kernel.ι f.unop) f.unop (_ : kernel.ι f.unop ≫ f.unop = 0)).op).hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op
[PROOFSTEP]
exact Quiver.Hom.unop_inj (by simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc])
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((Iso.mk (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) (_ : kernel.ι f.unop ≫ cokernel.π (kernel.ι f.unop) = 0)).op
            (cokernel.desc (kernel.ι f.unop) f.unop (_ : kernel.ι f.unop ≫ f.unop = 0)).op).hom ≫
        f).unop =
    (cokernel.π (kernel.ι f.unop)).op.unop
[PROOFSTEP]
simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc]
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ OrderHom.comp ↑(kernelOrderHom X) ↑(cokernelOrderHom X) = OrderHom.id
[PROOFSTEP]
change (kernelOrderHom X).comp (cokernelOrderHom X) = _
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X) = OrderHom.id
[PROOFSTEP]
refine' OrderHom.ext _ _ (funext (Subobject.ind _ _))
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f],
    ↑(OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X)) (Subobject.mk f) = ↑OrderHom.id (Subobject.mk f)
[PROOFSTEP]
intro A f hf
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ ↑(OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X)) (Subobject.mk f) = ↑OrderHom.id (Subobject.mk f)
[PROOFSTEP]
dsimp only [OrderHom.comp_coe, Function.comp_apply, cokernelOrderHom_coe, Subobject.lift_mk, kernelOrderHom_coe,
  OrderHom.id_coe, id.def, unop_op, Quiver.Hom.unop_op]
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ Subobject.mk (kernel.ι (cokernel.π f)) = Subobject.mk f
[PROOFSTEP]
refine' Subobject.mk_eq_mk_of_comm _ _ ⟨_, _, _, _⟩ _
[GOAL]
case refine'_2.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel (cokernel.π f) ⟶ A
[PROOFSTEP]
exact Abelian.monoLift f _ (kernel.condition (cokernel.π f))
[GOAL]
case refine'_2.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ A ⟶ kernel (cokernel.π f)
[PROOFSTEP]
exact kernel.lift _ _ (cokernel.condition f)
[GOAL]
case refine'_2.refine'_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ monoLift f (kernel.ι (cokernel.π f)) (_ : kernel.ι (cokernel.π f) ≫ cokernel.π f = 0) ≫
      kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0) =
    𝟙 (kernel (cokernel.π f))
[PROOFSTEP]
simp only [← cancel_mono (kernel.ι (cokernel.π f)), Category.assoc, image.fac, monoLift_comp, Category.id_comp]
[GOAL]
case refine'_2.refine'_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0) ≫
      monoLift f (kernel.ι (cokernel.π f)) (_ : kernel.ι (cokernel.π f) ≫ cokernel.π f = 0) =
    𝟙 A
[PROOFSTEP]
simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp]
[GOAL]
case refine'_2.refine'_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ (Iso.mk (monoLift f (kernel.ι (cokernel.π f)) (_ : kernel.ι (cokernel.π f) ≫ cokernel.π f = 0))
          (kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0))).hom ≫
      f =
    kernel.ι (cokernel.π f)
[PROOFSTEP]
simp only [monoLift_comp]
