awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
A : Subobject.{v, u} X
hA : A = ⊤
pos : LE.le (α := Subobject.{v, u} X) ⊤ (largerSubobject hG ⊤)
⊢ A ≤ largerSubobject hG A

Tactic:
subst hA
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
⊢ LE.le (α := Subobject.{v, u} X) ⊤ (largerSubobject hG ⊤)

Tactic:
simp only [largerSubobject_top, le_refl]

Premises used: le_refl, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject_top
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
A : Subobject.{v, u} X
hA : ¬A = ⊤
⊢ A ≤ largerSubobject hG A

Tactic:
(lt_largerSubobject hG A hA).le

Premises used: LT.lt.le, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.lt_largerSubobject
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
A : Subobject.{v, u} X
hA : ¬A = ⊤
⊢ A ≤ largerSubobject hG A

Tactic:
exact (lt_largerSubobject hG A hA).le

Premises used: LT.lt.le, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.lt_largerSubobject
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
A : Subobject.{v, u} X
pos :
  ∀ (hA : A = ⊤),
    MorphismProperty.pushouts (generatingMonomorphisms G) (Y := Functor.obj Subobject.underlying (largerSubobject hG A))
      (A.ofLE (largerSubobject hG A) ⋯)
neg :
  ∀ (hA : ¬A = ⊤),
    MorphismProperty.pushouts (generatingMonomorphisms G) (Y := Functor.obj Subobject.underlying (largerSubobject hG A))
      (A.ofLE (largerSubobject hG A) ⋯)
⊢ MorphismProperty.pushouts (generatingMonomorphisms G) (Y := Functor.obj Subobject.underlying (largerSubobject hG A))
    (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
by_cases hA : A = ⊤
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
A : Subobject.{v, u} X
hA : A = ⊤
pos :
  MorphismProperty.pushouts (generatingMonomorphisms G) (X :=
    Functor.obj (C := Subobject.{v, u} X) Subobject.underlying ⊤) (Y :=
    Functor.obj (C := Subobject.{v, u} X) Subobject.underlying (largerSubobject hG ⊤))
    (Subobject.ofLE ⊤ (largerSubobject hG ⊤) ⋯)
⊢ MorphismProperty.pushouts (generatingMonomorphisms G) (Y := Functor.obj Subobject.underlying (largerSubobject hG A))
    (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
subst hA
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
⊢ Eq (α := Subobject.{v, u} X) (largerSubobject hG ⊤) ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
⊢ IsIso (X := Functor.obj (C := Subobject.{v, u} X) Subobject.underlying (largerSubobject hG ⊤))
    (Subobject.arrow (largerSubobject hG ⊤))

Tactic:
have := (Subobject.isIso_arrow_iff_eq_top (largerSubobject hG (⊤ : Subobject X))).2 (by simp)
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
this :
  IsIso (X := Functor.obj (C := Subobject.{v, u} X) Subobject.underlying (largerSubobject hG ⊤))
    (Subobject.arrow (largerSubobject hG ⊤))
⊢ Iso.hom (asIso (Subobject.arrow ⊤)) ≫ Arrow.hom (Arrow.mk (𝟙 X)) =
    (Arrow.mk (X :=
          Functor.obj (C := MonoOver.{v, u} (Arrow.left.{v, u} (Arrow.mk (𝟙 X))))
            (MonoOver.forget (Arrow.left.{v, u} (Arrow.mk (𝟙 X))) ⋙ Over.forget (Arrow.left.{v, u} (Arrow.mk (𝟙 X))))
            (Functor.obj Subobject.representative ⊤))
          (Y :=
          Functor.obj
            (MonoOver.forget (Arrow.right.{v, u} (Arrow.mk (𝟙 X))) ⋙ Over.forget (Arrow.right.{v, u} (Arrow.mk (𝟙 X))))
            (Functor.obj Subobject.representative (largerSubobject hG ⊤)))
          (Subobject.ofLE ⊤ (largerSubobject hG ⊤) ⋯)).hom ≫
      Iso.hom (asIso (Subobject.arrow (largerSubobject hG ⊤)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
this :
  IsIso (X := Functor.obj (C := Subobject.{v, u} X) Subobject.underlying (largerSubobject hG ⊤))
    (Subobject.arrow (largerSubobject hG ⊤))
⊢ MorphismProperty.pushouts (generatingMonomorphisms G) (X :=
    Functor.obj (C := Subobject.{v, u} X) Subobject.underlying ⊤) (Y :=
    Functor.obj (C := Subobject.{v, u} X) Subobject.underlying (largerSubobject hG ⊤))
    (Subobject.ofLE ⊤ (largerSubobject hG ⊤) ⋯)

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff _
      (Arrow.isoMk (asIso (Subobject.arrow _)) (asIso (Subobject.arrow _)) (by simp))).2
        (isomorphisms_le_pushouts_generatingMonomorphisms G (𝟙 X)
          (MorphismProperty.isomorphisms.infer_property _))

Premises used: Iff.mpr, CategoryTheory.Subobject.arrow, CategoryTheory.IsGrothendieckAbelian.isomorphisms_le_pushouts_generatingMonomorphisms, CategoryTheory.CategoryStruct.id, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.MorphismProperty.isomorphisms.infer_property, CategoryTheory.asIso, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
A : Subobject.{v, u} X
hA : ¬A = ⊤
⊢ MorphismProperty.pushouts (generatingMonomorphisms G) (Y := Functor.obj Subobject.underlying (largerSubobject hG A))
    (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
(MorphismProperty.arrow_mk_iso_iff _ ?_).1
      (exists_larger_subobject hG A hA).choose_spec.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_larger_subobject, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
A : Subobject.{v, u} X
hA : ¬A = ⊤
neg :
  Arrow.mk
      (A.ofLE
        (⋯.choose (p := fun (A' : Subobject.{v, u} X) ↦
          ∃ (h : A < A'), MorphismProperty.pushouts (generatingMonomorphisms G) (A.ofLE A' ⋯)))
        ⋯) ≅
    Arrow.mk (Y := Functor.obj Subobject.underlying (largerSubobject hG A)) (A.ofLE (largerSubobject hG A) ⋯)
⊢ MorphismProperty.pushouts (generatingMonomorphisms G) (Y := Functor.obj Subobject.underlying (largerSubobject hG A))
    (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
refine (MorphismProperty.arrow_mk_iso_iff _ ?_).1
      (exists_larger_subobject hG A hA).choose_spec.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_larger_subobject, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
A : Subobject.{v, u} X
hA : ¬A = ⊤
⊢ ⋯.choose (p := fun (A' : Subobject.{v, u} X) ↦
      ∃ (h : A < A'), MorphismProperty.pushouts (generatingMonomorphisms G) (A.ofLE A' ⋯)) =
    largerSubobject hG A

Tactic:
simp [largerSubobject, dif_neg hA]

Premises used: dif_neg, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
A : Subobject.{v, u} X
hA : ¬A = ⊤
⊢ Arrow.mk
      (A.ofLE
        (⋯.choose (p := fun (A' : Subobject.{v, u} X) ↦
          ∃ (h : A < A'), MorphismProperty.pushouts (generatingMonomorphisms G) (A.ofLE A' ⋯)))
        ⋯) ≅
    Arrow.mk (Y := Functor.obj Subobject.underlying (largerSubobject hG A)) (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
exact Arrow.isoMk (Iso.refl _)
      (Subobject.isoOfEq _ _ ((by simp [largerSubobject, dif_neg hA])))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
J : Type w
inst_3 : LinearOrder J
inst_4 : OrderBot J
inst_5 : SuccOrder J
inst_6 : WellFoundedLT J
hJ : HasCardinalLT (Subobject.{v, u} X) (Cardinal.mk J)
⊢ Eq (α := Subobject.{v, u} X) (largerSubobject hG ⊤) ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
J : Type w
inst_3 : LinearOrder J
inst_4 : OrderBot J
inst_5 : SuccOrder J
inst_6 : WellFoundedLT J
hJ : HasCardinalLT (Subobject.{v, u} X) (Cardinal.mk J)
h : Function.Injective (β := Subobject.{v, u} X) fun (j : J) ↦ transfiniteIterate (largerSubobject hG) j A₀
⊢ False

Tactic:
simpa [hasCardinalLT_iff_cardinal_mk_lt] using hJ.of_injective _ h

Premises used: HasCardinalLT.of_injective, hasCardinalLT_iff_cardinal_mk_lt
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject.{v, u} X)))
⊢ Nonempty.{w + 1} κ.ord.ToType

Tactic:
simp [κ]
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject.{v, u} X)))
⊢ Nonempty.{w + 1} κ.ord.ToType

Tactic:
have : Nonempty κ.ord.ToType := by simp [κ]
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject.{v, u} X)))
this : Nonempty.{w + 1} κ.ord.ToType
have :
  ∀ (this : OrderBot κ.ord.ToType), ∃ (o : Ordinal.{w}) (j : o.ToType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤
⊢ ∃ (o : Ordinal.{w}) (j : o.ToType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤

Tactic:
have := WellFoundedLT.toOrderBot κ.ord.ToType
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject.{v, u} X)))
this_1 : Nonempty.{w + 1} κ.ord.ToType
this : OrderBot κ.ord.ToType
⊢ Order.succ (Cardinal.lift.{w, max u v} (Cardinal.mk (Subobject.{v, u} X))) ≤
    Cardinal.lift.{max u v, w} (Cardinal.mk κ.ord.ToType)

Tactic:
simp [κ]
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject.{v, u} X)))
this_1 : Nonempty.{w + 1} κ.ord.ToType
this : OrderBot κ.ord.ToType
⊢ ∃ (o : Ordinal.{w}) (j : o.ToType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤

Tactic:
exact ⟨κ.ord, top_mem_range hG A₀ (lt_of_lt_of_le (Order.lt_succ _) (by simp [κ]))⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
J : Type w
inst_3 : LinearOrder J
inst_4 : OrderBot J
inst_5 : SuccOrder J
inst_6 : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
⊢ Nonempty.{w + 1} (↑(Set.Iio m) : Type w)

Tactic:
have := hm.nonempty_Iio.to_subtype
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
J : Type w
inst_3 : LinearOrder J
inst_4 : OrderBot J
inst_5 : SuccOrder J
inst_6 : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this : Nonempty.{w + 1} (↑(Set.Iio m) : Type w)
c : Cocone (J := (↑(Set.Iio m) : Type w))
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio m)) :
        (a : (↑(Set.Iio m) : Type w)) → J))
      ⋯ ⋙
    functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  PrincipalSeg.cocone (Set.principalSegIio m) (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
dsimp : Mono (transfiniteIterate (largerSubobject hG) m A₀).arrow
⊢ Mono c.pt.hom

Tactic:
dsimp [c]
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
J : Type w
inst_3 : LinearOrder J
inst_4 : OrderBot J
inst_5 : SuccOrder J
inst_6 : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this : Nonempty.{w + 1} (↑(Set.Iio m) : Type w)
c : Cocone (J := (↑(Set.Iio m) : Type w))
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio m)) :
        (a : (↑(Set.Iio m) : Type w)) → J))
      ⋯ ⋙
    functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  PrincipalSeg.cocone (Set.principalSegIio m) (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
⊢ Mono (transfiniteIterate (largerSubobject hG) m A₀).arrow

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
J : Type w
inst_3 : LinearOrder J
inst_4 : OrderBot J
inst_5 : SuccOrder J
inst_6 : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this : Nonempty.{w + 1} (↑(Set.Iio m) : Type w)
c : Cocone (J := (↑(Set.Iio m) : Type w))
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio m)) :
        (a : (↑(Set.Iio m) : Type w)) → J))
      ⋯ ⋙
    functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  PrincipalSeg.cocone (Set.principalSegIio m) (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
⊢ Mono c.pt.hom

Tactic:
have : Mono c.pt.hom := by dsimp [c]; infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
J : Type w
inst_3 : LinearOrder J
inst_4 : OrderBot J
inst_5 : SuccOrder J
inst_6 : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this_1 : Nonempty.{w + 1} (↑(Set.Iio m) : Type w)
c : Cocone (J := (↑(Set.Iio m) : Type w))
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio m)) :
        (a : (↑(Set.Iio m) : Type w)) → J))
      ⋯ ⋙
    functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  PrincipalSeg.cocone (Set.principalSegIio m) (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
this : Mono c.pt.hom
apply :
  Subobject.mk c.pt.hom =
    ⨆ (j : (↑(Set.Iio m) : Type w)),
      Subobject.mk
        (Functor.obj
                (Monotone.functor (f :=
                    (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s :=
                          fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio m)) :
                      (a : (↑(Set.Iio m) : Type w)) → J))
                    ⋯ ⋙
                  functorToMonoOver hG A₀ J)
                j).obj
            (P := Over.isMono X).hom
⊢ IsColimit (J := (↑(Set.Iio m) : Type w)) (F :=
    Monotone.functor (f :=
        (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
              x1 < x2) (Set.principalSegIio m)) :
          (a : (↑(Set.Iio m) : Type w)) → J))
        ⋯ ⋙
      functor hG A₀ J)
    (PrincipalSeg.cocone (Set.principalSegIio m) (functor hG A₀ J))

Tactic:
apply IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISup
      ((Set.principalSegIio m).monotone.functor ⋙ functorToMonoOver hG A₀ J) c

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver, CategoryTheory.IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISup, CategoryTheory.Functor.comp, PrincipalSeg.monotone, Monotone.functor, Set.principalSegIio
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
J : Type w
inst_3 : LinearOrder J
inst_4 : OrderBot J
inst_5 : SuccOrder J
inst_6 : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this_1 : Nonempty.{w + 1} (↑(Set.Iio m) : Type w)
c : Cocone (J := (↑(Set.Iio m) : Type w))
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio m)) :
        (a : (↑(Set.Iio m) : Type w)) → J))
      ⋯ ⋙
    functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  PrincipalSeg.cocone (Set.principalSegIio m) (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
this : Mono c.pt.hom
dsimp :
  Subobject.mk (transfiniteIterate (largerSubobject hG) m A₀).arrow =
    ⨆ (j : (↑(Set.Iio m) : Type w)), Subobject.mk (transfiniteIterate (largerSubobject hG) (↑j : J) A₀).arrow
⊢ Subobject.mk c.pt.hom =
    ⨆ (j : (↑(Set.Iio m) : Type w)),
      Subobject.mk
        (Functor.obj
                (Monotone.functor (f :=
                    (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s :=
                          fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio m)) :
                      (a : (↑(Set.Iio m) : Type w)) → J))
                    ⋯ ⋙
                  functorToMonoOver hG A₀ J)
                j).obj
            (P := Over.isMono X).hom

Tactic:
dsimp [c]
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
J : Type w
inst_3 : LinearOrder J
inst_4 : OrderBot J
inst_5 : SuccOrder J
inst_6 : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this_1 : Nonempty.{w + 1} (↑(Set.Iio m) : Type w)
c : Cocone (J := (↑(Set.Iio m) : Type w))
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio m)) :
        (a : (↑(Set.Iio m) : Type w)) → J))
      ⋯ ⋙
    functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  PrincipalSeg.cocone (Set.principalSegIio m) (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
this : Mono c.pt.hom
simp :
  transfiniteIterate (largerSubobject hG) m A₀ =
    ⨆ (j : (↑(Set.Iio m) : Type w)), transfiniteIterate (largerSubobject hG) (↑j : J) A₀
⊢ Subobject.mk (transfiniteIterate (largerSubobject hG) m A₀).arrow =
    ⨆ (j : (↑(Set.Iio m) : Type w)), Subobject.mk (transfiniteIterate (largerSubobject hG) (↑j : J) A₀).arrow

Tactic:
simp only [Subobject.mk_arrow]

Premises used: CategoryTheory.Subobject.mk_arrow
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
J : Type w
inst_3 : LinearOrder J
inst_4 : OrderBot J
inst_5 : SuccOrder J
inst_6 : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this_1 : Nonempty.{w + 1} (↑(Set.Iio m) : Type w)
c : Cocone (J := (↑(Set.Iio m) : Type w))
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio m)) :
        (a : (↑(Set.Iio m) : Type w)) → J))
      ⋯ ⋙
    functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  PrincipalSeg.cocone (Set.principalSegIio m) (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
this : Mono c.pt.hom
⊢ transfiniteIterate (largerSubobject hG) m A₀ =
    ⨆ (j : (↑(Set.Iio m) : Type w)), transfiniteIterate (largerSubobject hG) (↑j : J) A₀

Tactic:
transfiniteIterate_limit (largerSubobject hG) A₀ m hm

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject, transfiniteIterate_limit
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject.{v, u} X
J : Type w
inst_3 : LinearOrder J
inst_4 : OrderBot J
inst_5 : SuccOrder J
inst_6 : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this_1 : Nonempty.{w + 1} (↑(Set.Iio m) : Type w)
c : Cocone (J := (↑(Set.Iio m) : Type w))
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio m)) :
        (a : (↑(Set.Iio m) : Type w)) → J))
      ⋯ ⋙
    functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  PrincipalSeg.cocone (Set.principalSegIio m) (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
this : Mono c.pt.hom
⊢ transfiniteIterate (largerSubobject hG) m A₀ =
    ⨆ (j : (↑(Set.Iio m) : Type w)), transfiniteIterate (largerSubobject hG) (↑j : J) A₀

Tactic:
exact transfiniteIterate_limit (largerSubobject hG) A₀ m hm

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject, transfiniteIterate_limit
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst_3 : Mono f
J : Type w
inst_4 : LinearOrder J
inst_5 : OrderBot J
inst_6 : SuccOrder J
inst_7 : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject.{v, u} X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
⊢ IsIso t.arrow

Tactic:
have := (Subobject.isIso_arrow_iff_eq_top t).2 hj