awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
⊢ HasCardinalLT (↑(Set.range s) : Type (max u v)) κ

Tactic:
have hs : HasCardinalLT (Set.range s) κ :=
    hXκ.of_injective (f := Subtype.val) Subtype.val_injective
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
⊢ ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom

Tactic:
⟨IsCardinalFiltered.max σ hs, ?_⟩

Premises used: Exists.intro, CategoryTheory.IsCardinalFiltered.max
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
refine : IsIso (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom
⊢ ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom

Tactic:
refine ⟨IsCardinalFiltered.max σ hs, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
rw :
  ∀ (i : J),
    Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤
      Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom
⊢ IsIso (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom

Tactic:
rw [Subobject.isIso_iff_mk_eq_top, ← top_le_iff, ← h, iSup_le_iff]

Premises used: top_le_iff, CategoryTheory.Subobject.isIso_iff_mk_eq_top, iSup_le_iff
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
j : J
t : (↑(Set.range s) : Type (max u v)) := Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
trans : Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤ Subobject.mk (F.obj (σ t)).obj (P := Over.isMono X).hom
trans₁ :
  Subobject.mk (F.obj (σ t)).obj (P := Over.isMono X).hom ≤
    Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom
⊢ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤
    Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom

Tactic:
trans Subobject.mk (F.obj (σ t)).obj.hom

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Subobject.mk, CategoryTheory.Over.hom, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
j : J
t : (↑(Set.range s) : Type (max u v)) := Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
⊢ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤ Subobject.mk (F.obj (σ t)).obj (P := Over.isMono X).hom

Tactic:
(hσ t).symm.le

Premises used: Eq.le, CategoryTheory.Subobject.mk, Quotient.mk', Eq.symm
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
j : J
t : (↑(Set.range s) : Type (max u v)) := Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
⊢ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤ Subobject.mk (F.obj (σ t)).obj (P := Over.isMono X).hom

Tactic:
exact (hσ t).symm.le

Premises used: Eq.le, Eq.symm
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
j : J
t : (↑(Set.range s) : Type (max u v)) := Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
⊢ Subobject.mk (F.obj (σ t)).obj (P := Over.isMono X).hom ≤
    Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom

Tactic:
MonoOver.subobjectMk_le_mk_of_hom
      (F.map (IsCardinalFiltered.toMax σ hs t))

Premises used: CategoryTheory.IsCardinalFiltered.toMax, CategoryTheory.Functor.map, CategoryTheory.MonoOver.subobjectMk_le_mk_of_hom
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
j : J
t : (↑(Set.range s) : Type (max u v)) := Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
⊢ Subobject.mk (F.obj (σ t)).obj (P := Over.isMono X).hom ≤
    Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom

Tactic:
exact MonoOver.subobjectMk_le_mk_of_hom
      (F.map (IsCardinalFiltered.toMax σ hs t))

Premises used: CategoryTheory.IsCardinalFiltered.toMax, CategoryTheory.Functor.map, CategoryTheory.MonoOver.subobjectMk_le_mk_of_hom
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel (Y := cokernel f) (cokernel.π f)
⊢ CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (image.ι f) = f

Tactic:
kernel.lift_ι _ _ _

Premises used: CategoryTheory.Limits.kernel.lift_ι
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_4 : Mono f
⊢ Mono (Y := Abelian.image f) (Abelian.factorThruImage f)

Tactic:
mono_of_mono_fac <| image.fac f

Premises used: CategoryTheory.Abelian.image.fac, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasKernel f
inst_3 : HasCokernel (X := kernel f) (kernel.ι f)
⊢ CategoryStruct.comp (Y := Abelian.coimage f) (coimage.π f) (Abelian.factorThruCoimage f) = f

Tactic:
cokernel.π_desc _ _ _

Premises used: CategoryTheory.Limits.cokernel.π_desc
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasKernel f
inst_3 : HasCokernel (X := kernel f) (kernel.ι f)
inst_4 : Epi f
⊢ Epi (X := Abelian.coimage f) (Abelian.factorThruCoimage f)

Tactic:
epi_of_epi_fac <| coimage.fac f

Premises used: CategoryTheory.epi_of_epi_fac, CategoryTheory.Abelian.coimage.fac
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
⊢ Eq (α := P ⟶ cokernel f) (f ≫ cokernel.π f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
h :
  Eq (α := kernel f ⟶ Q)
    (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (kernel.ι f ≫ kernel.lift (cokernel.π f) f ⋯) (equalizer.ι (cokernel.π f) 0))
    (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) 0 (equalizer.ι (cokernel.π f) 0))
⊢ Eq (α := kernel f ⟶ Abelian.image f) (kernel.ι f ≫ kernel.lift (cokernel.π f) f ⋯) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
⊢ Eq (α := kernel f ⟶ Q)
    (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (kernel.ι f ≫ kernel.lift (cokernel.π f) f ⋯) (equalizer.ι (cokernel.π f) 0))
    (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) 0 (equalizer.ι (cokernel.π f) 0))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
⊢ Eq (α := kernel f ⟶ Q) (kernel.ι f ≫ f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
h :
  Eq (α := P ⟶ cokernel f)
    (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (cokernel.desc (kernel.ι f) f ⋯ ≫ cokernel.π f))
    (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0) 0)
⊢ Eq (α := Abelian.coimage f ⟶ cokernel f) (cokernel.desc (kernel.ι f) f ⋯ ≫ cokernel.π f) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
⊢ Eq (α := P ⟶ cokernel f)
    (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (cokernel.desc (kernel.ι f) f ⋯ ≫ cokernel.π f))
    (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0) 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
h :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
        (coimageImageComparison f))
      (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
        (coimageImageComparison' f))
      (equalizer.ι (cokernel.π f) 0)
⊢ Eq (α := Abelian.coimage f ⟶ Abelian.image f) (coimageImageComparison f) (coimageImageComparison' f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
        (coimageImageComparison f))
      (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
        (coimageImageComparison' f))
      (equalizer.ι (cokernel.π f) 0)

Tactic:
simp [coimageImageComparison, coimageImageComparison']

Premises used: CategoryTheory.Abelian.coimageImageComparison, CategoryTheory.Abelian.coimageImageComparison'
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
⊢ CategoryStruct.comp (Y := Abelian.coimage f) (coimage.π f)
      (CategoryStruct.comp (Y := Abelian.image f) (coimageImageComparison f) (image.ι f)) =
    f

Tactic:
simp [coimageImageComparison]

Premises used: CategoryTheory.Abelian.coimageImageComparison
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f_1 : P ⟶ Q
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
f g : Arrow.{v, u} C
η : f ⟶ g
⊢ f.hom ≫ Arrow.Hom.right η = Arrow.Hom.left η ≫ g.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f_1 : P ⟶ Q
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
f g : Arrow.{v, u} C
η : f ⟶ g
⊢ Eq (α := kernel f.hom ⟶ g.left) (kernel.ι f.hom ≫ Arrow.Hom.left η)
    (CategoryStruct.comp (Y := kernel g.hom) (kernel.map f.hom g.hom (Arrow.Hom.left η) (Arrow.Hom.right η) ⋯)
      (kernel.ι g.hom))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f_1 : P ⟶ Q
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
f g : Arrow.{v, u} C
η : f ⟶ g
⊢ Eq (α := f.right ⟶ cokernel g.hom)
    (CategoryStruct.comp (Y := cokernel f.hom) (cokernel.π f.hom)
      (cokernel.map f.hom g.hom (Arrow.Hom.left η) (Arrow.Hom.right η) ⋯))
    (Arrow.Hom.right η ≫ cokernel.π g.hom)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Indization
Goal:
C : Type v
inst : SmallCategory C
inst_1 : Abelian C
X Y : Ind C
f : X ⟶ Y
obtain :
  ∀ (I : Type v) (w : SmallCategory I) (w_1 : IsFiltered I) (F G : I ⥤ C) (ϕ : F ⟶ G)
    (i : Arrow.mk f ≅ Arrow.mk (X := Functor.obj (Ind.lim I) F) (Functor.map (Ind.lim I) ϕ)),
    IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
⊢ IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)

Tactic:
obtain ⟨I, _, _, F, G, ϕ, ⟨i⟩⟩ := Ind.exists_nonempty_arrow_mk_iso_ind_lim (f := f)

Premises used: CategoryTheory.Ind.exists_nonempty_arrow_mk_iso_ind_lim
-- Module: Mathlib.CategoryTheory.Abelian.Indization
Goal:
C : Type v
inst : SmallCategory C
inst_1 : Abelian C
X Y : Ind C
f : X ⟶ Y
I : Type v
w : SmallCategory I
w_1 : IsFiltered I
F G : I ⥤ C
ϕ : F ⟶ G
i : Arrow.mk f ≅ Arrow.mk (X := Functor.obj (Ind.lim I) F) (Functor.map (Ind.lim I) ϕ)
i' : Arrow.mk (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f) ≅
  Arrow.mk (X := Abelian.coimage (P := Functor.obj (Ind.lim I) F) (Functor.map (Ind.lim I) ϕ)) (Y :=
    Abelian.image (P := Functor.obj (Ind.lim I) F) (Functor.map (Ind.lim I) ϕ))
    (coimageImageComparison (Functor.map (Ind.lim I) ϕ)) :=
  Functor.mapIso coimageImageComparisonFunctor i
⊢ IsIso i'.hom

Tactic:
have := Iso.isIso_hom i'