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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f_1 : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f_1 = (F.obj j).obj (P := Over.isMono X).hom
this : Mono f_1
A : C
g : A ⟶ X
inst_5 : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤ Subobject.mk g
j j' : J
f : j ⟶ j'
dsimp :
  Over.Hom.left (F.map f).hom ≫ Subobject.ofMkLEMk (F.obj j').obj (P := Over.isMono X).hom g ⋯ =
    Subobject.ofMkLEMk (F.obj j).obj (P := Over.isMono X).hom g ⋯ ≫ 𝟙 A
⊢ (F ⋙ MonoOver.forget X ⋙ Over.forget X).map f ≫ Subobject.ofMkLEMk (F.obj j').obj (P := Over.isMono X).hom g ⋯ =
    Subobject.ofMkLEMk (F.obj j).obj (P := Over.isMono X).hom g ⋯ ≫ Functor.map (Functor.obj (Functor.const J) A) f

Tactic:
dsimp
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f_1 : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f_1 = (F.obj j).obj (P := Over.isMono X).hom
this : Mono f_1
A : C
g : A ⟶ X
inst_5 : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤ Subobject.mk g
j j' : J
f : j ⟶ j'
⊢ Over.Hom.left (F.map f).hom ≫ Subobject.ofMkLEMk (F.obj j').obj (P := Over.isMono X).hom g ⋯ =
    Subobject.ofMkLEMk (F.obj j).obj (P := Over.isMono X).hom g ⋯ ≫ 𝟙 A

Tactic:
simpa only [← cancel_mono g, Category.assoc, Subobject.ofMkLEMk_comp,
            Category.comp_id] using MonoOver.w (F.map f)

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.MonoOver.w, CategoryTheory.Subobject.ofMkLEMk_comp, CategoryTheory.Functor.map
-- 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
inst_4 : IsFiltered J
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 : Mono f
A : C
g : A ⟶ X
inst_5 : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤ Subobject.mk g
c' : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X) :=
  { pt := A,
    ι := { app := fun (j : J) ↦ Subobject.ofMkLEMk (F.obj j).obj (P := Over.isMono X).hom g ⋯, naturality := ⋯ } }
j : J
rw : c'.ι.app j ≫ g = c.ι.app j ≫ f
rw₁ : c'.ι.app j ≫ g = (F.obj j).obj (P := Over.isMono X).hom
rw₂ rw₃ : (F.obj j).obj (P := Over.isMono X).hom = (F.obj j).obj (P := Over.isMono X).hom
⊢ c.ι.app j ≫ hc.desc c' ≫ g = c.ι.app j ≫ f

Tactic:
rw [hc.fac_assoc c' j, hf, Subobject.ofMkLEMk_comp]

Premises used: CategoryTheory.Subobject.ofMkLEMk_comp, CategoryTheory.Limits.IsColimit.fac_assoc
-- 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
inst_4 : IsFiltered J
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 : Mono f
A : C
g : A ⟶ X
inst_5 : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤ Subobject.mk g
c' : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X) :=
  { pt := A,
    ι := { app := fun (j : J) ↦ Subobject.ofMkLEMk (F.obj j).obj (P := Over.isMono X).hom g ⋯, naturality := ⋯ } }
⊢ Subobject.mk f ≤ Subobject.mk g

Tactic:
exact Subobject.mk_le_mk_of_comm (hc.desc c')
      (hc.hom_ext (fun j ↦ by rw [hc.fac_assoc c' j, hf, Subobject.ofMkLEMk_comp]))

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Subobject.mk_le_mk_of_comm, CategoryTheory.Limits.IsColimit.desc
-- 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
inst_4 : IsFiltered J
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 : Mono f
a : ∀ (i : J), Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤ Subobject.mk f
⊢ ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤ Subobject.mk f

Tactic:
rw [iSup_le_iff]

Premises used: 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
inst_4 : IsFiltered J
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 : Mono f
j : J
⊢ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤ Subobject.mk f

Tactic:
Subobject.mk_le_mk_of_comm (c.ι.app j) (hf j)

Premises used: CategoryTheory.Subobject.mk_le_mk_of_comm, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- 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
inst_4 : IsFiltered J
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 : Mono f
j : J
⊢ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤ Subobject.mk f

Tactic:
exact Subobject.mk_le_mk_of_comm (c.ι.app j) (hf j)

Premises used: CategoryTheory.Subobject.mk_le_mk_of_comm, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
j j' : J
g : j ⟶ j'
⊢ (F ⋙ MonoOver.forget X ⋙ Over.forget X).map g ≫ (F.obj j').obj (P := Over.isMono X).hom =
    (F.obj j).obj (P := Over.isMono X).hom ≫ Functor.map (Functor.obj (Functor.const J) X) g

Tactic:
simp [MonoOver.forget]

Premises used: CategoryTheory.MonoOver.forget
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
⊢ ∀ (j : J),
    (colimit.cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)).ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom

Tactic:
simp [f]
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
⊢ Mono f

Tactic:
haveI := mono_of_isColimit_monoOver F (colimit.isColimit _) f (by simp [f])
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this : Mono f
⊢ ∀ (j : J),
    (colimit.cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)).ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom

Tactic:
simp [f]
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this : Mono f
⊢ Subobject.mk f = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom

Tactic:
have := subobjectMk_of_isColimit_eq_iSup F (colimit.isColimit _) f (by simp [f])
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this_1 : Mono f
this : Subobject.mk f = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
⊢ Subobject.mk f = Subobject.mk c.pt.hom

Tactic:
rw [← h] at this
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this_1 : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
refine :
  ∀ (j : J),
    (colimit.cocone ((F ⋙ MonoOver.forget X) ⋙ Over.forget X)).ι.app j ≫ (Subobject.isoOfMkEqMk f c.pt.hom this).hom =
      NatTrans.app (Cocone.ι (Functor.mapCocone (Over.forget X) c)) j
⊢ IsColimit (F := (F ⋙ MonoOver.forget X) ⋙ Over.forget X) (Functor.mapCocone (Over.forget X) c)

Tactic:
refine IsColimit.ofIsoColimit (colimit.isColimit _)
    (Cocone.ext (Subobject.isoOfMkEqMk _ _ this) (fun j ↦ ?_))

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Subobject.isoOfMkEqMk
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this_1 : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
rw :
  ((colimit.cocone ((F ⋙ MonoOver.forget X) ⋙ Over.forget X)).ι.app j ≫ (Subobject.isoOfMkEqMk f c.pt.hom this).hom) ≫
      c.pt.hom =
    NatTrans.app (Cocone.ι (Functor.mapCocone (Over.forget X) c)) j ≫ c.pt.hom
⊢ (colimit.cocone ((F ⋙ MonoOver.forget X) ⋙ Over.forget X)).ι.app j ≫ (Subobject.isoOfMkEqMk f c.pt.hom this).hom =
    NatTrans.app (Cocone.ι (Functor.mapCocone (Over.forget X) c)) j

Tactic:
rw [← cancel_mono (c.pt.hom)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Over.hom, CategoryTheory.Limits.Cocone.pt
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this_1 : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
dsimp :
  (colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ Subobject.ofMkLEMk f c.pt.hom ⋯) ≫ c.pt.hom =
    Over.Hom.left (c.ι.app j) ≫ c.pt.hom
⊢ ((colimit.cocone ((F ⋙ MonoOver.forget X) ⋙ Over.forget X)).ι.app j ≫ (Subobject.isoOfMkEqMk f c.pt.hom this).hom) ≫
      c.pt.hom =
    NatTrans.app (Cocone.ι (Functor.mapCocone (Over.forget X) c)) j ≫ c.pt.hom

Tactic:
dsimp
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this_1 : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
rw : colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
⊢ (colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ Subobject.ofMkLEMk f c.pt.hom ⋯) ≫ c.pt.hom =
    Over.Hom.left (c.ι.app j) ≫ c.pt.hom

Tactic:
rw [Category.assoc, Subobject.ofMkLEMk_comp, Over.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Subobject.ofMkLEMk_comp, CategoryTheory.Over.w
-- 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
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this_1 : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ f = (F.obj j).obj (P := Over.isMono X).hom

Tactic:
apply colimit.ι_desc

Premises used: CategoryTheory.Limits.colimit.ι_desc
-- 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
h : Epi f
⊢ IsFiltered J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
-- 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
h : Epi f
this : IsFiltered J
⊢ Mono f

Tactic:
have := mono_of_isColimit_monoOver F hc f hf
-- 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
h : Epi f
this_1 : IsFiltered J
this : Mono f
⊢ Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤

Tactic:
rw [Subobject.epi_iff_mk_eq_top f,
    subobjectMk_of_isColimit_eq_iSup F hc f hf] at h

Premises used: CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup, CategoryTheory.Subobject.epi_iff_mk_eq_top
-- 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
j : J
⊢ ∃ (a : J),
    Eq (α := { 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 }))
        a)
      (Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯)

Tactic:
⟨j, rfl⟩

Premises used: Exists.intro, rfl
-- 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
j : J
⊢ ∃ (a : J),
    Eq (α := { 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 }))
        a)
      (Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯)

Tactic:
exact ⟨j, rfl⟩
-- 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
⊢ 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) ⋯

Tactic:
have h' : Function.Surjective (fun (j : J) ↦ (⟨s j, _, rfl⟩ : Set.range s)) := by
    rintro ⟨_, j, rfl⟩
    exact ⟨j, rfl⟩
-- 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) ⋯
obtain :
  ∀ (σ : { 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) ⋯),
    ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom
⊢ ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom

Tactic:
obtain ⟨σ, hσ⟩ := h'.hasRightInverse

Premises used: Function.Surjective.hasRightInverse