awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X Y : C
p : X ⟶ Y
inst_2 : Mono p
hp :
  ¬∀ (G_1 : C),
      ObjectProperty.singleton.{v, u} G G_1 →
        Function.Surjective (α := (fun (X : Type v) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op G_1)) X)) (β :=
          (fun (X : Type v) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op G_1)) Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (Opposite.op G_1)) p)) :
            (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (Opposite.op G_1)).obj X)) →
              (fun (X : Type v) ↦ X) ((coyoneda.obj (Opposite.op G_1)).obj Y))
⊢ ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : MorphismProperty.pushouts (generatingMonomorphisms G) i) (_ : ¬IsIso i) (_
    : Mono p'), i ≫ p' = p
have hp₁ : ∃ (x : G ⟶ Y),
  ∀ (x_1 : G ⟶ X),
    ¬((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (Functor.map yoneda p) (Opposite.op G)) :
              TypeCat.Fun (G ⟶ X) (G ⟶ Y)) :
            (a : G ⟶ X) → G ⟶ Y)
          x_1 =
        x
Tactic: simp only [ObjectProperty.singleton_iff, Function.Surjective, Functor.flip_obj_obj,
    yoneda_obj_obj, Functor.flip_obj_map, forall_eq', not_forall, not_exists] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X Y : C
p : X ⟶ Y
inst_2 : Mono p
hp :
  ∃ (x : G ⟶ Y),
    ∀ (x_1 : G ⟶ X),
      ¬((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (Functor.map yoneda p) (Opposite.op G)) :
                TypeCat.Fun (G ⟶ X) (G ⟶ Y)) :
              (a : G ⟶ X) → G ⟶ Y)
            x_1 =
          x
⊢ ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : MorphismProperty.pushouts (generatingMonomorphisms G) i) (_ : ¬IsIso i) (_
    : Mono p'), i ≫ p' = p
have obtain : ∀ (f : G ⟶ Y)
  (hf :
    ∀ (x : G ⟶ X),
      ¬((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (Functor.map yoneda p) (Opposite.op G)) :
                TypeCat.Fun (G ⟶ X) (G ⟶ Y)) :
              (a : G ⟶ X) → G ⟶ Y)
            x =
          f),
  ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : MorphismProperty.pushouts (generatingMonomorphisms G) i) (_ : ¬IsIso i) (_
    : Mono p'), i ≫ p' = p
Tactic: obtain ⟨f, hf⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X Y : C
p : X ⟶ Y
inst_2 : Mono p
f : G ⟶ Y
hf :
  ∀ (x : G ⟶ X),
    ¬((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (Functor.map yoneda p) (Opposite.op G)) :
              TypeCat.Fun (G ⟶ X) (G ⟶ Y)) :
            (a : G ⟶ X) → G ⟶ Y)
          x =
        f
⊢ ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : MorphismProperty.pushouts (generatingMonomorphisms G) i) (_ : ¬IsIso i) (_
    : Mono p'), i ≫ p' = p
have refine_1 : ¬IsIso (Y := pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f))
    (pushout.inl (pullback.fst p f) (pullback.snd p f))
Tactic: refine ⟨pushout (pullback.fst p f) (pullback.snd p f), pushout.inl _ _,
    pushout.desc p f pullback.condition,
    ⟨_, _, _, (Subobject.underlyingIso _).hom ≫ pullback.fst _ _,
    pushout.inr _ _, ⟨Subobject.mk (pullback.snd p f)⟩,
    (IsPushout.of_hasPushout (pullback.fst p f) (pullback.snd p f)).of_iso
      ((Subobject.underlyingIso _).symm) (Iso.refl _) (Iso.refl _)
      (Iso.refl _) (by simp) (by simp) (by simp) (by simp)⟩, ?_, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X Y : C
p : X ⟶ Y
inst_2 : Mono p
f : G ⟶ Y
hf :
  ∀ (x : G ⟶ X),
    ¬((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (Functor.map yoneda p) (Opposite.op G)) :
              TypeCat.Fun (G ⟶ X) (G ⟶ Y)) :
            (a : G ⟶ X) → G ⟶ Y)
          x =
        f
refine_1 :
  ¬IsIso (Y := pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f))
      (pushout.inl (pullback.fst p f) (pullback.snd p f))
⊢ ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : MorphismProperty.pushouts (generatingMonomorphisms G) i) (_ : ¬IsIso i) (_
    : Mono p'), i ≫ p' = p
have refine_2 : Mono (X := pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f)) (pushout.desc p f sorry)
Tactic: refine ⟨pushout (pullback.fst p f) (pullback.snd p f), pushout.inl _ _,
    pushout.desc p f pullback.condition,
    ⟨_, _, _, (Subobject.underlyingIso _).hom ≫ pullback.fst _ _,
    pushout.inr _ _, ⟨Subobject.mk (pullback.snd p f)⟩,
    (IsPushout.of_hasPushout (pullback.fst p f) (pullback.snd p f)).of_iso
      ((Subobject.underlyingIso _).symm) (Iso.refl _) (Iso.refl _)
      (Iso.refl _) (by simp) (by simp) (by simp) (by simp)⟩, ?_, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X Y : C
p : X ⟶ Y
inst_2 : Mono p
f : G ⟶ Y
hf :
  ∀ (x : G ⟶ X),
    ¬((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (Functor.map yoneda p) (Opposite.op G)) :
              TypeCat.Fun (G ⟶ X) (G ⟶ Y)) :
            (a : G ⟶ X) → G ⟶ Y)
          x =
        f
h :
  IsIso (Y := pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f))
    (pushout.inl (pullback.fst p f) (pullback.snd p f))
⊢ False
have h₁ : ∀ (T : C),
  Function.Bijective (β := T ⟶ pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f)) fun (x : T ⟶ X) ↦
    x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)
Tactic: rw [isIso_iff_yoneda_map_bijective] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X Y : C
p : X ⟶ Y
inst_2 : Mono p
f : G ⟶ Y
hf :
  ∀ (x : G ⟶ X),
    ¬((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (Functor.map yoneda p) (Opposite.op G)) :
              TypeCat.Fun (G ⟶ X) (G ⟶ Y)) :
            (a : G ⟶ X) → G ⟶ Y)
          x =
        f
h :
  ∀ (T : C),
    Function.Bijective (β := T ⟶ pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f)) fun (x : T ⟶ X) ↦
      x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)
⊢ False
have refine_1 : ∀ (a : G ⟶ X)
  (ha :
    Eq (α := G ⟶ pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f))
      ((fun (x : G ⟶ X) ↦
          (x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f) :
            G ⟶ pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f)))
        a)
      (pushout.inr (pullback.fst p f) (pullback.snd p f))),
  False
Tactic: obtain ⟨a, ha⟩ := (h G).2 (pushout.inr _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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' : Subobject.{v, u} X) (h : A < A'), MorphismProperty.pushouts (generatingMonomorphisms G) (A.ofLE A' ⋯)
have h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst_2 : Mono f] (hA : Subobject.mk f ≠ ⊤),
  ∃ (A' : Subobject.{v, u} X) (h : Subobject.mk f < A'),
    MorphismProperty.pushouts (generatingMonomorphisms G) ((Subobject.mk f).ofLE A' sorry)
Tactic: induction A using Subobject.ind with | _ f
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X A : C
f : A ⟶ X
inst_2 : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ∃ (A' : Subobject.{v, u} X) (h : Subobject.mk f < A'),
    MorphismProperty.pushouts (generatingMonomorphisms G) ((Subobject.mk f).ofLE A' ⋯)
have h : ∀ (X' : C) (i : A ⟶ X') (p' : X' ⟶ X) (hi : MorphismProperty.pushouts (generatingMonomorphisms G) i) (hi' : ¬IsIso i)
  (hp' : Mono p') (fac : i ≫ p' = f),
  ∃ (A' : Subobject.{v, u} X) (h : Subobject.mk f < A'),
    MorphismProperty.pushouts (generatingMonomorphisms G) ((Subobject.mk f).ofLE A' sorry)
Tactic: obtain ⟨X', i, p', hi, hi', hp', fac⟩ := exists_pushouts hG f
    (by simpa only [Subobject.isIso_iff_mk_eq_top] using hA)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X A : C
f : A ⟶ X
inst_2 : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : A ⟶ X'
p' : X' ⟶ X
hi : MorphismProperty.pushouts (generatingMonomorphisms G) i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ ∃ (A' : Subobject.{v, u} X) (h : Subobject.mk f < A'),
    MorphismProperty.pushouts (generatingMonomorphisms G) ((Subobject.mk f).ofLE A' ⋯)
have h : Arrow.mk (Y := Functor.obj Subobject.underlying (Subobject.mk p')) ((Subobject.mk f).ofLE (Subobject.mk p') sorry) ≅
  Arrow.mk i
Tactic: refine ⟨Subobject.mk p', Subobject.mk_lt_mk_of_comm i fac hi',
    (MorphismProperty.arrow_mk_iso_iff _ ?_).2 hi⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X A : C
f : A ⟶ X
inst_2 : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : A ⟶ X'
p' : X' ⟶ X
hi : MorphismProperty.pushouts (generatingMonomorphisms G) i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ Arrow.mk (Y := Functor.obj Subobject.underlying (Subobject.mk p')) ((Subobject.mk f).ofLE (Subobject.mk p') ⋯) ≅
    Arrow.mk i
have h : Iso.hom (Subobject.underlyingIso f) ≫ (Arrow.mk i).hom =
  (Arrow.mk (Y := Functor.obj Subobject.underlying (Subobject.mk p')) ((Subobject.mk f).ofLE (Subobject.mk p') sorry)).hom ≫
    Iso.hom (Subobject.underlyingIso p')
Tactic: refine Arrow.isoMk (Subobject.underlyingIso f) (Subobject.underlyingIso p') ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X A : C
f : A ⟶ X
inst_2 : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : A ⟶ X'
p' : X' ⟶ X
hi : MorphismProperty.pushouts (generatingMonomorphisms G) i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ Iso.hom (Subobject.underlyingIso f) ≫ (Arrow.mk i).hom =
    (Arrow.mk (Y := Functor.obj Subobject.underlying (Subobject.mk p'))
          ((Subobject.mk f).ofLE (Subobject.mk p') ⋯)).hom ≫
      Iso.hom (Subobject.underlyingIso p')
have h : Iso.hom (Subobject.underlyingIso f) ≫ i =
  CategoryStruct.comp (Y := Functor.obj Subobject.underlying (Subobject.mk p'))
    ((Subobject.mk f).ofLE (Subobject.mk p') sorry) (Iso.hom (Subobject.underlyingIso p'))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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 <
    if hA : A = ⊤ then ⊤
    else
      ⋯.choose (p := fun (A' : Subobject.{v, u} X) ↦
        ∃ (h : A < A'), MorphismProperty.pushouts (generatingMonomorphisms G) (A.ofLE A' ⋯))
have rw : A <
  sorry.choose (p := fun (A' : Subobject.{v, u} X) ↦
    ∃ (h : A < A'), MorphismProperty.pushouts (generatingMonomorphisms G) (A.ofLE A' sorry))
Tactic: rw [dif_neg hA]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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
⊢ A ≤ largerSubobject hG A
have pos : ∀ (hA : A = ⊤), A ≤ largerSubobject hG A
Tactic: by_cases hA : A = ⊤
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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 = ⊤), A ≤ largerSubobject hG A
⊢ A ≤ largerSubobject hG A
have neg : ∀ (hA : ¬A = ⊤), A ≤ largerSubobject hG A
Tactic: by_cases hA : A = ⊤
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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
have pos : LE.le (α := Subobject.{v, u} X) ⊤ (largerSubobject hG ⊤)
Tactic: subst hA
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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
⊢ MorphismProperty.pushouts (generatingMonomorphisms G) (Y := Functor.obj Subobject.underlying (largerSubobject hG A))
    (A.ofLE (largerSubobject hG A) ⋯)
have pos : ∀ (hA : A = ⊤),
  MorphismProperty.pushouts (generatingMonomorphisms G) (Y := Functor.obj Subobject.underlying (largerSubobject hG A))
    (A.ofLE (largerSubobject hG A) sorry)
Tactic: by_cases hA : A = ⊤
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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) ⋯)
⊢ MorphismProperty.pushouts (generatingMonomorphisms G) (Y := Functor.obj Subobject.underlying (largerSubobject hG A))
    (A.ofLE (largerSubobject hG A) ⋯)
have neg : ∀ (hA : ¬A = ⊤),
  MorphismProperty.pushouts (generatingMonomorphisms G) (Y := Functor.obj Subobject.underlying (largerSubobject hG A))
    (A.ofLE (largerSubobject hG A) sorry)
Tactic: by_cases hA : A = ⊤
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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) ⋯)
have 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 ⊤) sorry)
Tactic: subst hA
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X : C
⊢ 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 ⊤) ⋯)
have this : 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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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) ⋯)
have neg : Arrow.mk
    (A.ofLE
      (sorry.choose (p := fun (A' : Subobject.{v, u} X) ↦
        ∃ (h : A < A'), MorphismProperty.pushouts (generatingMonomorphisms G) (A.ofLE A' sorry)))
      sorry) ≅
  Arrow.mk (Y := Functor.obj Subobject.underlying (largerSubobject hG A)) (A.ofLE (largerSubobject hG A) sorry)
Tactic: refine (MorphismProperty.arrow_mk_iso_iff _ ?_).1
      (exists_larger_subobject hG A hA).choose_spec.choose_spec
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (hypothesis)
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)))
⊢ ∃ (o : Ordinal.{w}) (j : o.ToType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤
have this : Nonempty.{w + 1} κ.ord.ToType
Tactic: have : Nonempty κ.ord.ToType := by simp [κ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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
⊢ ∃ (o : Ordinal.{w}) (j : o.ToType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤
have have : ∀ (this : OrderBot κ.ord.ToType), ∃ (o : Ordinal.{w}) (j : o.ToType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤
Tactic: have := WellFoundedLT.toOrderBot κ.ord.ToType
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (hypothesis)
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
⊢ 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))
have this : Nonempty.{w + 1} (↑(Set.Iio m) : Type w)
Tactic: have := hm.nonempty_Iio.to_subtype
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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
have dsimp : Mono (transfiniteIterate (largerSubobject hG) m A₀).arrow
Tactic: dsimp [c]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (hypothesis)
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)
⊢ 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))
have this₁ : Mono c.pt.hom
Tactic: have : Mono c.pt.hom := by dsimp [c]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
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
⊢ 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))
have 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))
                  sorry ⋙
                functorToMonoOver hG A₀ J)
              j).obj
          (P := Over.isMono X).hom
Tactic: apply IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISup
      ((Set.principalSegIio m).monotone.functor ⋙ functorToMonoOver hG A₀ J) c