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
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
j : κ.ord.ToType
hj : ¬IsMax j
this :
  pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)) (Y :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.obj
      (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.map
      (homOfLE ⋯))
simp : LE.le (α := MorphismProperty.{v, u} C) (generatingMonomorphisms G) (monomorphisms C)
⊢ LE.le (α := MorphismProperty.{v, u} C) (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G))) (monomorphisms C)

Tactic:
simp only [pushouts_le_iff, coproducts_le_iff]

Premises used: CategoryTheory.MorphismProperty.coproducts_le_iff, CategoryTheory.MorphismProperty.pushouts_le_iff
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
j : κ.ord.ToType
hj : ¬IsMax j
this :
  pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)) (Y :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.obj
      (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.map
      (homOfLE ⋯))
⊢ LE.le (α := MorphismProperty.{v, u} C) (generatingMonomorphisms G) (monomorphisms C)

Tactic:
generatingMonomorphisms_le_monomorphisms G

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
j : κ.ord.ToType
hj : ¬IsMax j
this :
  pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)) (Y :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.obj
      (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.map
      (homOfLE ⋯))
⊢ LE.le (α := MorphismProperty.{v, u} C) (generatingMonomorphisms G) (monomorphisms C)

Tactic:
exact generatingMonomorphisms_le_monomorphisms G

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
hf' : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} (monomorphisms C) κ.ord.ToType f :=
  let __TransfiniteCompositionOfShape :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
      (↑(toSet (generatingMonomorphisms G)) : Type (max u v)));
  MorphismProperty.TransfiniteCompositionOfShape.mk (W := monomorphisms C) __TransfiniteCompositionOfShape ⋯
⊢ ∀ (j j' : κ.ord.ToType) (φ : j ⟶ j'), Mono (hf'.toTransfiniteCompositionOfShape (W := monomorphisms C).F.map φ)

Tactic:
have (j j' : κ.ord.ToType) (φ : j ⟶ j') : Mono (hf'.F.map φ) := hf'.mem_map φ
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
hf' : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} (monomorphisms C) κ.ord.ToType f :=
  let __TransfiniteCompositionOfShape :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
      (↑(toSet (generatingMonomorphisms G)) : Type (max u v)));
  MorphismProperty.TransfiniteCompositionOfShape.mk (W := monomorphisms C) __TransfiniteCompositionOfShape ⋯
this : ∀ (j j' : κ.ord.ToType) (φ : j ⟶ j'), Mono (hf'.toTransfiniteCompositionOfShape (W := monomorphisms C).F.map φ)
hXκ : HasCardinalLT (Subobject.{v, u} A) κ
⊢ PreservesColimit
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
        (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F
    (Functor.obj coyoneda (Opposite.op A))

Tactic:
apply preservesColimit_coyoneda_obj_of_mono (Y := hf'.F) (κ := κ)

Premises used: CategoryTheory.IsGrothendieckAbelian.preservesColimit_coyoneda_obj_of_mono, CategoryTheory.TransfiniteCompositionOfShape.F, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
hf' : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} (monomorphisms C) κ.ord.ToType f :=
  let __TransfiniteCompositionOfShape :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
      (↑(toSet (generatingMonomorphisms G)) : Type (max u v)));
  MorphismProperty.TransfiniteCompositionOfShape.mk (W := monomorphisms C) __TransfiniteCompositionOfShape ⋯
this : ∀ (j j' : κ.ord.ToType) (φ : j ⟶ j'), Mono (hf'.toTransfiniteCompositionOfShape (W := monomorphisms C).F.map φ)
hXκ : ∀ ⦃X Y : C⦄ (S : Subobject.{v, u} G), HasCardinalLT (Subobject.{v, u} (Functor.obj Subobject.underlying S)) κ
⊢ HasCardinalLT (Subobject.{v, u} A) κ

Tactic:
obtain ⟨S⟩ := hi
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
X_1 Y_1 : C
f : X_1 ⟶ Y_1
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
hf' : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} (monomorphisms C) κ.ord.ToType f :=
  let __TransfiniteCompositionOfShape :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
      (↑(toSet (generatingMonomorphisms G)) : Type (max u v)));
  MorphismProperty.TransfiniteCompositionOfShape.mk (W := monomorphisms C) __TransfiniteCompositionOfShape ⋯
this : ∀ (j j' : κ.ord.ToType) (φ : j ⟶ j'), Mono (hf'.toTransfiniteCompositionOfShape (W := monomorphisms C).F.map φ)
X Y : C
S : Subobject.{v, u} G
⊢ HasCardinalLT (Subobject.{v, u} (Functor.obj Subobject.underlying S)) κ

Tactic:
Subobject.hasCardinalLT_of_mono hκ S.arrow

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Subobject.hasCardinalLT_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
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
X_1 Y_1 : C
f : X_1 ⟶ Y_1
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
hf' : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} (monomorphisms C) κ.ord.ToType f :=
  let __TransfiniteCompositionOfShape :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
      (↑(toSet (generatingMonomorphisms G)) : Type (max u v)));
  MorphismProperty.TransfiniteCompositionOfShape.mk (W := monomorphisms C) __TransfiniteCompositionOfShape ⋯
this : ∀ (j j' : κ.ord.ToType) (φ : j ⟶ j'), Mono (hf'.toTransfiniteCompositionOfShape (W := monomorphisms C).F.map φ)
X Y : C
S : Subobject.{v, u} G
⊢ HasCardinalLT (Subobject.{v, u} (Functor.obj Subobject.underlying S)) κ

Tactic:
exact Subobject.hasCardinalLT_of_mono hκ S.arrow

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Subobject.hasCardinalLT_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
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this : OrderBot κ.ord.ToType
⊢ HasSmallObjectArgument.{w, v, u} (generatingMonomorphisms G)

Tactic:
exact ⟨κ, inferInstance, inferInstance,
    { preservesColimit {A B X Y} i hi f hf := by
        let hf' : (monomorphisms C).TransfiniteCompositionOfShape κ.ord.ToType f :=
          { toTransfiniteCompositionOfShape := hf.toTransfiniteCompositionOfShape
            map_mem j hj := by
              have := (hf.attachCells j hj).pushouts_coproducts
              simp only [ofHoms_homFamily] at this
              refine (?_ : _ ≤ monomorphisms C) _ this
              simp only [pushouts_le_iff, coproducts_le_iff]
              exact generatingMonomorphisms_le_monomorphisms G }
        have (j j' : κ.ord.ToType) (φ : j ⟶ j') : Mono (hf'.F.map φ) := hf'.mem_map φ
        apply preservesColimit_coyoneda_obj_of_mono (Y := hf'.F) (κ := κ)
        obtain ⟨S⟩ := hi
        exact Subobject.hasCardinalLT_of_mono hκ S.arrow }⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
⊢ Eq (α := MorphismProperty.{v, u} C) (llp (rlp (monomorphisms C))) (monomorphisms C)

Tactic:
le_antisymm ?_ (le_llp_rlp _)

Premises used: CategoryTheory.MorphismProperty.le_llp_rlp, le_antisymm
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
refine : LE.le (α := MorphismProperty.{v, u} C) (llp (rlp (monomorphisms C))) (monomorphisms C)
⊢ Eq (α := MorphismProperty.{v, u} C) (llp (rlp (monomorphisms C))) (monomorphisms C)

Tactic:
refine le_antisymm ?_ (le_llp_rlp _)

Premises used: CategoryTheory.MorphismProperty.le_llp_rlp, le_antisymm
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
rw :
  LE.le (α := MorphismProperty.{v, u} C)
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))))
    (monomorphisms C)
⊢ LE.le (α := MorphismProperty.{v, u} C) (llp (rlp (monomorphisms C))) (monomorphisms C)

Tactic:
rw [← generatingMonomorphisms_rlp hG, llp_rlp_of_hasSmallObjectArgument]

Premises used: CategoryTheory.MorphismProperty.llp_rlp_of_hasSmallObjectArgument, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_rlp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
trans :
  LE.le (α := MorphismProperty.{v, u} C)
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))))
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C)))))
trans₁ :
  LE.le (α := MorphismProperty.{v, u} C)
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C))))) (monomorphisms C)
⊢ LE.le (α := MorphismProperty.{v, u} C)
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))))
    (monomorphisms C)

Tactic:
trans (transfiniteCompositions.{w} (coproducts.{w} (monomorphisms C)).pushouts).retracts
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
a :
  LE.le (α := MorphismProperty.{v, u} C)
    (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G))))
    (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C))))
⊢ LE.le (α := MorphismProperty.{v, u} C)
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))))
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C)))))

Tactic:
apply retracts_monotone

Premises used: CategoryTheory.MorphismProperty.retracts_monotone
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
a :
  LE.le (α := MorphismProperty.{v, u} C) (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))
    (pushouts (coproducts.{w, v, u} (monomorphisms C)))
⊢ LE.le (α := MorphismProperty.{v, u} C)
    (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G))))
    (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C))))

Tactic:
apply transfiniteCompositions_monotone

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositions_monotone
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
a :
  LE.le (α := MorphismProperty.{v, u} C) (coproducts.{w, v, u} (generatingMonomorphisms G))
    (coproducts.{w, v, u} (monomorphisms C))
⊢ LE.le (α := MorphismProperty.{v, u} C) (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))
    (pushouts (coproducts.{w, v, u} (monomorphisms C)))

Tactic:
apply pushouts_monotone

Premises used: CategoryTheory.MorphismProperty.pushouts_monotone
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
a : LE.le (α := MorphismProperty.{v, u} C) (generatingMonomorphisms G) (monomorphisms C)
⊢ LE.le (α := MorphismProperty.{v, u} C) (coproducts.{w, v, u} (generatingMonomorphisms G))
    (coproducts.{w, v, u} (monomorphisms C))

Tactic:
apply coproducts_monotone

Premises used: CategoryTheory.MorphismProperty.coproducts_monotone
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
⊢ LE.le (α := MorphismProperty.{v, u} C) (generatingMonomorphisms G) (monomorphisms C)

Tactic:
apply generatingMonomorphisms_le_monomorphisms

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
⊢ LE.le (α := MorphismProperty.{v, u} C)
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C))))) (monomorphisms C)

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
inst_2 : IsGrothendieckAbelian.{w, v, u} C
⊢ IsSeparator.{v, u} (separator.{v, u} C)

Tactic:
have hG := isSeparator_separator C
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} (separator.{v, u} C)
rw :
  HasFunctorialFactorization.{v, u} (llp (rlp (generatingMonomorphisms (separator.{v, u} C))))
    (rlp (generatingMonomorphisms (separator.{v, u} C)))
⊢ HasFunctorialFactorization.{v, u} (monomorphisms C) (rlp (monomorphisms C))

Tactic:
rw [← generatingMonomorphisms_rlp hG, ← llp_rlp_monomorphisms hG,
    ← generatingMonomorphisms_rlp hG]

Premises used: CategoryTheory.IsGrothendieckAbelian.llp_rlp_monomorphisms, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_rlp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} (separator.{v, u} C)
⊢ HasFunctorialFactorization.{v, u} (llp (rlp (generatingMonomorphisms (separator.{v, u} C))))
    (rlp (generatingMonomorphisms (separator.{v, u} C)))

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
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X Y : C
f : X ⟶ Y
⊢ Mono ((monoMapFactorizationDataRlp.{w, v, u} f).i (W₁ := monomorphisms C) (W₂ := rlp (monomorphisms C)))

Tactic:
(monoMapFactorizationDataRlp f).hi

Premises used: CategoryTheory.IsGrothendieckAbelian.monoMapFactorizationDataRlp, CategoryTheory.MorphismProperty.MapFactorizationData.hi
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
fac : MapFactorizationData.{v, u} (monomorphisms C) (rlp (monomorphisms C)) (X := X) (Y := 0) 0 :=
  monoMapFactorizationDataRlp.{w, v, u} 0
⊢ Injective.{v, u} (C := C)
    (MapFactorizationData.Z (W₁ := monomorphisms C) (W₂ := rlp (monomorphisms C)) (X := X) (Y := 0) (f := 0)
      (monoMapFactorizationDataRlp.{w, v, u} 0))

Tactic:
simpa only [injective_iff_rlp_monomorphisms_zero,
    (isZero_zero C).eq_of_tgt fac.p 0] using fac.hp

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.MorphismProperty.MapFactorizationData.p, CategoryTheory.Limits.IsZero.eq_of_tgt, OfNat.ofNat, CategoryTheory.injective_iff_rlp_monomorphisms_zero, CategoryTheory.MorphismProperty.MapFactorizationData.hp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
⊢ HasExt.{w, v, u} C

Tactic:
hasExt_of_enoughInjectives _

Premises used: CategoryTheory.hasExt_of_enoughInjectives
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
⊢ Functor.IsRightAdjoint.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)

Tactic:
isRightAdjoint_of_preservesLimits_of_isCoseparating.{v} (isCoseparator_coseparator _) _

Premises used: CategoryTheory.isCoseparator_coseparator, CategoryTheory.isRightAdjoint_of_preservesLimits_of_isCoseparating