awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G X_1 Y : C
X : Subobject.{v, u} G
⊢ MorphismProperty.monomorphisms C X.arrow

Tactic:
inferInstanceAs (Mono _)

Premises used: _private.0.CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms._proof_1
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G X_1 Y : C
X : Subobject.{v, u} G
⊢ MorphismProperty.monomorphisms C X.arrow

Tactic:
exact inferInstanceAs (Mono _)
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : HasZeroMorphisms.{v, u} C
⊢ LE.le (α := MorphismProperty.{v, u} C) (MorphismProperty.isomorphisms C)
    (MorphismProperty.pushouts (generatingMonomorphisms G))

Tactic:
MorphismProperty.isomorphisms_le_pushouts _
    (fun _ ↦ ⟨_, _, _, ⟨⊤⟩, 0, inferInstance⟩)

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Subobject.underlying, inferInstance, CategoryTheory.MorphismProperty.isomorphisms_le_pushouts, Exists.intro, CategoryTheory.MorphismProperty.ofHoms.mk, Top.top, OfNat.ofNat, CategoryTheory.Functor.obj
-- 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 Y : C
p : X ⟶ Y
inst_2 : Mono p
hp : ¬IsIso p
⊢ ¬∀ (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))

Tactic:
rw [hG.isDetector.isIso_iff_of_mono] at hp

Premises used: CategoryTheory.IsSeparator.isDetector, CategoryTheory.ObjectProperty.IsDetecting.isIso_iff_of_mono
-- 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 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 : 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

Premises used: not_exists, CategoryTheory.yoneda_obj_obj, forall_eq', CategoryTheory.ObjectProperty.singleton_iff, CategoryTheory.Functor.flip_obj_map, CategoryTheory.Functor.flip_obj_obj, Classical.not_forall, Function.Surjective
-- 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 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
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
⊢ ∃ (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
-- 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 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
⊢ Eq (α := pullback p f ⟶ X) (pullback.fst p f ≫ Iso.hom (Iso.refl X))
    (CategoryStruct.comp (Y := Functor.obj Subobject.underlying (Subobject.mk (A := pullback p f) (pullback.snd p f)))
      (Iso.hom (Iso.symm (Subobject.underlyingIso (pullback.snd p f))))
      (Iso.hom (Subobject.underlyingIso (pullback.snd p f)) ≫ pullback.fst p f))

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 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
⊢ pullback.snd p f ≫ Iso.hom (Iso.refl G) =
    Iso.hom (Iso.symm (Subobject.underlyingIso (pullback.snd p f))) ≫
      (Subobject.mk (A := pullback p f) (pullback.snd p f)).arrow

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 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
⊢ pushout.inl (pullback.fst p f) (pullback.snd p f) ≫
      Iso.hom (Iso.refl (pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f))) =
    Iso.hom (Iso.refl X) ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)

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 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
⊢ pushout.inr (pullback.fst p f) (pullback.snd p f) ≫
      Iso.hom (Iso.refl (pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f))) =
    Iso.hom (Iso.refl G) ≫ pushout.inr (pullback.fst p f) (pullback.snd p f)

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 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
⊢ CategoryStruct.comp (Y := pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f))
      (pushout.inl (pullback.fst p f) (pullback.snd p f)) (pushout.desc p f ⋯) =
    p

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 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))
refine_2 : Mono (X := pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f)) (pushout.desc p f ⋯)
⊢ ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : MorphismProperty.pushouts (generatingMonomorphisms G) i) (_ : ¬IsIso i) (_
    : Mono p'), i ≫ p' = p

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⟩
-- 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 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))
⊢ ∀ (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

Premises used: CategoryTheory.isIso_iff_yoneda_map_bijective
-- 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 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)
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
⊢ False

Tactic:
obtain ⟨a, ha⟩ := (h G).2 (pushout.inr _ _)

Premises used: And.right, CategoryTheory.Limits.pushout.inr
-- 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 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)
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))
⊢ ((@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)
      a =
    f

Tactic:
simpa using ha =≫ pushout.desc p f pullback.condition

Premises used: CategoryTheory.Limits.pushout.desc, CategoryTheory.Limits.pullback.condition
-- 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 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)
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:
exact hf a (by simpa using ha =≫ pushout.desc p f pullback.condition)
-- 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 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
⊢ CategoryStruct.comp (Y := pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f))
      (pushout.inr (pullback.fst p f) (pullback.snd p f)) (pushout.desc p f ⋯) =
    f

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 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
⊢ Mono (X := pushout (X := pullback p f) (pullback.fst p f) (pullback.snd p f)) (pushout.desc p f ⋯)

Tactic:
exact (IsPushout.of_hasPushout _ _).mono_of_isPullback_of_mono
      (IsPullback.of_hasPullback p f) _ (by simp) (by simp)

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.IsPushout.mono_of_isPullback_of_mono, CategoryTheory.IsPullback.of_hasPullback
-- 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 ≠ ⊤
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' ⋯)
⊢ ∃ (A' : Subobject.{v, u} X) (h : A < A'), MorphismProperty.pushouts (generatingMonomorphisms G) (A.ofLE A' ⋯)

Tactic:
induction A using Subobject.ind with | _ f

Premises used: CategoryTheory.Subobject.ind
-- 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 A : C
f : A ⟶ X
inst_2 : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ¬IsIso f

Tactic:
simpa only [Subobject.isIso_iff_mk_eq_top] using hA

Premises used: CategoryTheory.Subobject.isIso_iff_mk_eq_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 A : C
f : A ⟶ X
inst_2 : Mono f
hA : Subobject.mk f ≠ ⊤
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' ⋯)
⊢ ∃ (A' : Subobject.{v, u} X) (h : Subobject.mk f < A'),
    MorphismProperty.pushouts (generatingMonomorphisms G) ((Subobject.mk f).ofLE A' ⋯)

Tactic:
obtain ⟨X', i, p', hi, hi', hp', fac⟩ := exists_pushouts hG f
    (by simpa only [Subobject.isIso_iff_mk_eq_top] using hA)

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_pushouts
-- 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 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' ⋯)

Tactic:
⟨Subobject.mk p', Subobject.mk_lt_mk_of_comm i fac hi',
    (MorphismProperty.arrow_mk_iso_iff _ ?_).2 hi⟩

Premises used: Iff.mpr, CategoryTheory.Subobject.mk_lt_mk_of_comm, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Subobject.mk, Exists.intro
-- 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 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
h :
  Arrow.mk (Y := Functor.obj Subobject.underlying (Subobject.mk p')) ((Subobject.mk f).ofLE (Subobject.mk p') ⋯) ≅
    Arrow.mk i
⊢ ∃ (A' : Subobject.{v, u} X) (h : Subobject.mk f < A'),
    MorphismProperty.pushouts (generatingMonomorphisms G) ((Subobject.mk f).ofLE A' ⋯)

Tactic:
refine ⟨Subobject.mk p', Subobject.mk_lt_mk_of_comm i fac hi',
    (MorphismProperty.arrow_mk_iso_iff _ ?_).2 hi⟩
-- 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 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
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') ⋯)).hom ≫
      Iso.hom (Subobject.underlyingIso p')
⊢ Arrow.mk (Y := Functor.obj Subobject.underlying (Subobject.mk p')) ((Subobject.mk f).ofLE (Subobject.mk p') ⋯) ≅
    Arrow.mk i

Tactic:
refine Arrow.isoMk (Subobject.underlyingIso f) (Subobject.underlyingIso p') ?_

Premises used: 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 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
h :
  Iso.hom (Subobject.underlyingIso f) ≫ i =
    CategoryStruct.comp (Y := Functor.obj Subobject.underlying (Subobject.mk p'))
      ((Subobject.mk f).ofLE (Subobject.mk p') ⋯) (Iso.hom (Subobject.underlyingIso p'))
⊢ 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')

Tactic:
dsimp
-- 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 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) ≫ i =
    CategoryStruct.comp (Y := Functor.obj Subobject.underlying (Subobject.mk p'))
      ((Subobject.mk f).ofLE (Subobject.mk p') ⋯) (Iso.hom (Subobject.underlyingIso p'))

Tactic:
simp only [← cancel_mono p', assoc, fac,
    Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow]

Premises used: CategoryTheory.Subobject.ofLE_arrow, CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk
-- 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:
dif_pos rfl

Premises used: dif_pos, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject, rfl
-- 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 ≠ ⊤
rw :
  A <
    ⋯.choose (p := fun (A' : Subobject.{v, u} X) ↦
      ∃ (h : A < A'), MorphismProperty.pushouts (generatingMonomorphisms G) (A.ofLE 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' ⋯))

Tactic:
rw [dif_neg hA]

Premises used: dif_neg
-- 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 <
    ⋯.choose (p := fun (A' : Subobject.{v, u} X) ↦
      ∃ (h : A < A'), MorphismProperty.pushouts (generatingMonomorphisms G) (A.ofLE A' ⋯))

Tactic:
(exists_larger_subobject hG A hA).choose_spec.choose

Premises used: Exists.choose_spec, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_larger_subobject, Exists.choose
-- 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 <
    ⋯.choose (p := fun (A' : Subobject.{v, u} X) ↦
      ∃ (h : A < A'), MorphismProperty.pushouts (generatingMonomorphisms G) (A.ofLE A' ⋯))

Tactic:
exact (exists_larger_subobject hG A hA).choose_spec.choose

Premises used: Exists.choose_spec, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_larger_subobject, Exists.choose
-- 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 = ⊤), A ≤ largerSubobject hG A
neg : ∀ (hA : ¬A = ⊤), A ≤ largerSubobject hG A
⊢ A ≤ largerSubobject hG A

Tactic:
by_cases hA : A = ⊤