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
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)
this : IsIso t.arrow
apply :
  Arrow.mk (X := Functor.obj (functor hG (Subobject.mk f) J) ⊥) (Y := Functor.obj (functor hG (Subobject.mk f) J) j)
      (Functor.map (functor hG (Subobject.mk f) J) (homOfLE ⋯)) ≅
    Arrow.mk f
⊢ MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} (MorphismProperty.pushouts (generatingMonomorphisms G))
    (↑(Set.Iic j) : Type w) f

Tactic:
apply (transfiniteCompositionOfShapeMapFromBot hG (Subobject.mk f) j).ofArrowIso

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.transfiniteCompositionOfShapeMapFromBot, CategoryTheory.Subobject.mk, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofArrowIso
-- 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)
this : IsIso t.arrow
refine :
  ((transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).isoOfEq (Subobject.mk f) ⋯ ≪≫
          Subobject.underlyingIso f).hom ≫
      (Arrow.mk f).hom =
    (Arrow.mk (X := Functor.obj (functor hG (Subobject.mk f) J) ⊥) (Y := Functor.obj (functor hG (Subobject.mk f) J) j)
          (Functor.map (functor hG (Subobject.mk f) J) (homOfLE ⋯))).hom ≫
      (asIso t.arrow).hom
⊢ Arrow.mk (X := Functor.obj (functor hG (Subobject.mk f) J) ⊥) (Y := Functor.obj (functor hG (Subobject.mk f) J) j)
      (Functor.map (functor hG (Subobject.mk f) J) (homOfLE ⋯)) ≅
    Arrow.mk f

Tactic:
refine Arrow.isoMk ((Subobject.isoOfEq _ _ (transfiniteIterate_bot _ _) ≪≫
    Subobject.underlyingIso f)) (asIso t.arrow) ?_

Premises used: CategoryTheory.Iso.trans, 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
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)
this : IsIso t.arrow
dsimp :
  ((transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) ⋯ ≫
        Iso.hom (Subobject.underlyingIso f)) ≫
      f =
    (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow
⊢ ((transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).isoOfEq (Subobject.mk f) ⋯ ≪≫
          Subobject.underlyingIso f).hom ≫
      (Arrow.mk f).hom =
    (Arrow.mk (X := Functor.obj (functor hG (Subobject.mk f) J) ⊥) (Y := Functor.obj (functor hG (Subobject.mk f) J) j)
          (Functor.map (functor hG (Subobject.mk f) J) (homOfLE ⋯))).hom ≫
      (asIso t.arrow).hom

Tactic:
dsimp [MonoOver.forget]

Premises used: CategoryTheory.MonoOver.forget
-- 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)
this : IsIso t.arrow
rw :
  (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) ⋯ ≫
      Iso.hom (Subobject.underlyingIso f) ≫ f =
    (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow
rw₁ :
  (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) ⋯ ≫
      (Subobject.mk f).arrow =
    (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow
rw₂ :
  (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).arrow =
    (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow
rw₃ rw₄ :
  (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).arrow =
    (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).arrow
⊢ ((transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) ⋯ ≫
        Iso.hom (Subobject.underlyingIso f)) ≫
      f =
    (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow

Tactic:
rw [assoc, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow,
    Subobject.ofLE_arrow]

Premises used: CategoryTheory.Subobject.ofLE_arrow, CategoryTheory.Category.assoc, 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
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst_3 : Mono f
obtain :
  ∀ (o : Ordinal.{w}) (j : o.ToType) (hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤),
    ∃ (J : Type w) (x : LinearOrder J) (x_1 : OrderBot J) (x_2 : SuccOrder J) (x_3 : WellFoundedLT J),
      Nonempty
        (MorphismProperty.TransfiniteCompositionOfShape (MorphismProperty.pushouts (generatingMonomorphisms G)) J f)
⊢ ∃ (J : Type w) (x : LinearOrder J) (x_1 : OrderBot J) (x_2 : SuccOrder J) (x_3 : WellFoundedLT J),
    Nonempty
      (MorphismProperty.TransfiniteCompositionOfShape (MorphismProperty.pushouts (generatingMonomorphisms G)) J f)

Tactic:
obtain ⟨o, j, hj⟩ := exists_ordinal hG (Subobject.mk f)

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal, CategoryTheory.Subobject.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
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst_3 : Mono f
o : Ordinal.{w}
j : o.ToType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
⊢ Nonempty.{w + 1} o.ToType

Tactic:
have : Nonempty o.ToType := ⟨j⟩
-- 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
o : Ordinal.{w}
j : o.ToType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
this : Nonempty.{w + 1} o.ToType
have :
  ∀ (this : OrderBot o.ToType),
    ∃ (J : Type w) (x : LinearOrder J) (x_1 : OrderBot J) (x_2 : SuccOrder J) (x_3 : WellFoundedLT J),
      Nonempty
        (MorphismProperty.TransfiniteCompositionOfShape (MorphismProperty.pushouts (generatingMonomorphisms G)) J f)
⊢ ∃ (J : Type w) (x : LinearOrder J) (x_1 : OrderBot J) (x_2 : SuccOrder J) (x_3 : WellFoundedLT J),
    Nonempty
      (MorphismProperty.TransfiniteCompositionOfShape (MorphismProperty.pushouts (generatingMonomorphisms G)) J f)

Tactic:
have : OrderBot o.ToType := WellFoundedLT.toOrderBot _
-- 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
o : Ordinal.{w}
j : o.ToType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
this_1 : Nonempty.{w + 1} o.ToType
this : OrderBot o.ToType
⊢ ∃ (J : Type w) (x : LinearOrder J) (x_1 : OrderBot J) (x_2 : SuccOrder J) (x_3 : WellFoundedLT J),
    Nonempty
      (MorphismProperty.TransfiniteCompositionOfShape (MorphismProperty.pushouts (generatingMonomorphisms G)) J f)

Tactic:
⟨_, _, _, _, _, ⟨transfiniteCompositionOfShapeOfEqTop hG hj⟩⟩

Premises used: Nonempty.intro, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.transfiniteCompositionOfShapeOfEqTop, 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 : C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst_3 : Mono f
o : Ordinal.{w}
j : o.ToType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
this_1 : Nonempty.{w + 1} o.ToType
this : OrderBot o.ToType
⊢ ∃ (J : Type w) (x : LinearOrder J) (x_1 : OrderBot J) (x_2 : SuccOrder J) (x_3 : WellFoundedLT J),
    Nonempty
      (MorphismProperty.TransfiniteCompositionOfShape (MorphismProperty.pushouts (generatingMonomorphisms G)) J f)

Tactic:
exact ⟨_, _, _, _, _, ⟨transfiniteCompositionOfShapeOfEqTop hG hj⟩⟩
-- 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) (rlp (generatingMonomorphisms G)) (rlp (monomorphisms C))
a₁ : LE.le (α := MorphismProperty.{v, u} C) (rlp (monomorphisms C)) (rlp (generatingMonomorphisms G))
⊢ Eq (α := MorphismProperty.{v, u} C) (rlp (generatingMonomorphisms G)) (rlp (monomorphisms C))

Tactic:
apply le_antisymm

Premises used: 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
X Y : C
p : X ⟶ Y
hp : rlp (generatingMonomorphisms G) p
A B : C
i : A ⟶ B
a : Mono i → HasLiftingProperty i p
⊢ monomorphisms C i → HasLiftingProperty i p

Tactic:
(_ : Mono i)
-- 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
X Y : C
p : X ⟶ Y
hp : rlp (generatingMonomorphisms G) p
A B : C
i : A ⟶ B
h : Mono i
a :
  ∀ (J : Type w) (w : LinearOrder J) (w_1 : OrderBot J) (w_2 : SuccOrder J) (w_3 : WellFoundedLT J)
    (h : MorphismProperty.TransfiniteCompositionOfShape (pushouts (generatingMonomorphisms G)) J i),
    HasLiftingProperty i p
⊢ HasLiftingProperty i p

Tactic:
obtain ⟨J, _, _, _, _, ⟨h⟩⟩ :=
      generatingMonomorphisms.exists_transfiniteCompositionOfShape hG i

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_transfiniteCompositionOfShape
-- 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
X Y : C
p : X ⟶ Y
hp : rlp (generatingMonomorphisms G) p
A B : C
i : A ⟶ B
h_1 : Mono i
J : Type w
w : LinearOrder J
w_1 : OrderBot J
w_2 : SuccOrder J
w_3 : WellFoundedLT J
h : MorphismProperty.TransfiniteCompositionOfShape (pushouts (generatingMonomorphisms G)) J i
⊢ rlp (pushouts (generatingMonomorphisms G)) p

Tactic:
simpa
-- 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
X Y : C
p : X ⟶ Y
hp : rlp (generatingMonomorphisms G) p
A B : C
i : A ⟶ B
h_1 : Mono i
J : Type w
w : LinearOrder J
w_1 : OrderBot J
w_2 : SuccOrder J
w_3 : WellFoundedLT J
h : MorphismProperty.TransfiniteCompositionOfShape (pushouts (generatingMonomorphisms G)) J i
⊢ HasLiftingProperty i p

Tactic:
exact transfiniteCompositionsOfShape_le_llp_rlp _ _ _ h.mem _ (by simpa)

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_llp_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
⊢ LE.le (α := MorphismProperty.{v, u} C) (rlp (monomorphisms C)) (rlp (generatingMonomorphisms G))

Tactic:
antitone_rlp (generatingMonomorphisms_le_monomorphisms _)

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms, CategoryTheory.MorphismProperty.antitone_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
⊢ LE.le (α := MorphismProperty.{v, u} C) (rlp (monomorphisms C)) (rlp (generatingMonomorphisms G))

Tactic:
exact antitone_rlp (generatingMonomorphisms_le_monomorphisms _)

Premises used: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms, CategoryTheory.MorphismProperty.antitone_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
obtain :
  ∀ (κ : Cardinal.{w}) (hκ' : κ.IsRegular) (hκ : HasCardinalLT (Subobject.{v, u} G) κ),
    HasSmallObjectArgument.{w, v, u} (generatingMonomorphisms G)
⊢ HasSmallObjectArgument.{w, v, u} (generatingMonomorphisms G)

Tactic:
obtain ⟨κ, hκ', hκ⟩ := HasCardinalLT.exists_regular_cardinal.{w} (Subobject G)
-- 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) κ
⊢ Fact κ.IsRegular

Tactic:
have : Fact κ.IsRegular := ⟨hκ'⟩
-- 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 : Fact κ.IsRegular
⊢ Nonempty.{w + 1} κ.ord.ToType

Tactic:
simpa using hκ'.ne_zero

Premises used: Cardinal.IsRegular.ne_zero
-- 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 : Fact κ.IsRegular
⊢ Nonempty.{w + 1} κ.ord.ToType

Tactic:
have : Nonempty κ.ord.ToType := by simpa using hκ'.ne_zero
-- 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 : Nonempty.{w + 1} κ.ord.ToType
have : ∀ (this : OrderBot κ.ord.ToType), HasSmallObjectArgument.{w, v, u} (generatingMonomorphisms G)
⊢ HasSmallObjectArgument.{w, v, u} (generatingMonomorphisms G)

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
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
j : κ.ord.ToType
hj : ¬IsMax j
⊢ pushouts
    (coproducts.{w, v, u}
      (ofHoms (ι := (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (homFamily (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 ⋯))

Tactic:
have := (hf.attachCells j hj).pushouts_coproducts
-- 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}
      (ofHoms (ι := (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (homFamily (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 ⋯))
⊢ 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 ⋯))

Tactic:
simp only [ofHoms_homFamily] at this

Premises used: CategoryTheory.MorphismProperty.ofHoms_homFamily
-- 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 ⋯))
⊢ monomorphisms C (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 ⋯))

Tactic:
(?_ : _ ≤ monomorphisms C) _ this
-- 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 ⋯))
refine :
  LE.le (α := MorphismProperty.{v, u} C) (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G))) (monomorphisms C)
⊢ monomorphisms C (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 ⋯))

Tactic:
refine (?_ : _ ≤ monomorphisms C) _ this