awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Subobject.mk c.pt.hom =
    ⨆ (j : (↑(Set.Iio m) : Type w)),
      Subobject.mk
        (Functor.obj
                (Monotone.functor (f :=
                    (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s :=
                          fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio m)) :
                      (a : (↑(Set.Iio m) : Type w)) → J))
                    ⋯ ⋙
                  functorToMonoOver hG A₀ J)
                j).obj
            (P := Over.isMono X).hom
have dsimp : Subobject.mk (transfiniteIterate (largerSubobject hG) m A₀).arrow =
  ⨆ (j : (↑(Set.Iio m) : Type w)), Subobject.mk (transfiniteIterate (largerSubobject hG) (↑j : J) A₀).arrow
Tactic: dsimp [c]
-- 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
⊢ Subobject.mk (transfiniteIterate (largerSubobject hG) m A₀).arrow =
    ⨆ (j : (↑(Set.Iio m) : Type w)), Subobject.mk (transfiniteIterate (largerSubobject hG) (↑j : J) A₀).arrow
have simp : transfiniteIterate (largerSubobject hG) m A₀ =
  ⨆ (j : (↑(Set.Iio m) : Type w)), transfiniteIterate (largerSubobject hG) (↑j : J) A₀
Tactic: simp only [Subobject.mk_arrow]
-- 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 : 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)
⊢ MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} (MorphismProperty.pushouts (generatingMonomorphisms G))
    (↑(Set.Iic j) : Type w) f
have this : IsIso t.arrow
Tactic: have := (Subobject.isIso_arrow_iff_eq_top t).2 hj
-- 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 : 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
⊢ MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} (MorphismProperty.pushouts (generatingMonomorphisms G))
    (↑(Set.Iic j) : Type w) f
have 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 sorry)) ≅
  Arrow.mk f
Tactic: apply (transfiniteCompositionOfShapeMapFromBot hG (Subobject.mk f) j).ofArrowIso
-- 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 : 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
⊢ 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
have refine : ((transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).isoOfEq (Subobject.mk f) sorry ≪≫
        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 sorry))).hom ≫
    (asIso t.arrow).hom
Tactic: refine Arrow.isoMk ((Subobject.isoOfEq _ _ (transfiniteIterate_bot _ _) ≪≫
    Subobject.underlyingIso f)) (asIso t.arrow) ?_
-- 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 : 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
⊢ ((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
have dsimp : ((transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) sorry ≫
      Iso.hom (Subobject.underlyingIso f)) ≫
    f =
  (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE
      (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) sorry ≫
    t.arrow
Tactic: dsimp [MonoOver.forget]
-- 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 : 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
⊢ ((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
have rw : (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) sorry ≫
    Iso.hom (Subobject.underlyingIso f) ≫ f =
  (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE
      (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) sorry ≫
    t.arrow
Tactic: rw [assoc, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow,
    Subobject.ofLE_arrow]
-- 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 : 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
⊢ ((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
have rw₁ : (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) sorry ≫ (Subobject.mk f).arrow =
  (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).ofLE
      (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) sorry ≫
    t.arrow
Tactic: rw [assoc, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow,
    Subobject.ofLE_arrow]
-- 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 : 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
⊢ ((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
have 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)) sorry ≫
    t.arrow
Tactic: rw [assoc, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow,
    Subobject.ofLE_arrow]
-- 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 : 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
⊢ ((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
have rw₃ : (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).arrow =
  (transfiniteIterate (largerSubobject hG) (J := J) ⊥ (Subobject.mk f)).arrow
Tactic: rw [assoc, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow,
    Subobject.ofLE_arrow]
-- 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 : C
f : A ⟶ X
inst_3 : Mono 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)
have 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)
Tactic: obtain ⟨o, j, hj⟩ := exists_ordinal hG (Subobject.mk f)
-- 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 : C
f : A ⟶ X
inst_3 : Mono f
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)
have this : Nonempty.{w + 1} o.ToType
Tactic: have : Nonempty o.ToType := ⟨j⟩
-- 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 : 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
⊢ ∃ (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)
have 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)
Tactic: have : OrderBot o.ToType := WellFoundedLT.toOrderBot _
-- 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
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
⊢ Eq (α := MorphismProperty.{v, u} C) (rlp (generatingMonomorphisms G)) (rlp (monomorphisms C))
have a : LE.le (α := MorphismProperty.{v, u} C) (rlp (generatingMonomorphisms G)) (rlp (monomorphisms C))
Tactic: apply le_antisymm
-- 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
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))
⊢ Eq (α := MorphismProperty.{v, u} C) (rlp (generatingMonomorphisms G)) (rlp (monomorphisms C))
have a₁ : LE.le (α := MorphismProperty.{v, u} C) (rlp (monomorphisms C)) (rlp (generatingMonomorphisms G))
Tactic: apply le_antisymm
-- 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
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
⊢ monomorphisms C i → HasLiftingProperty i p
have a : Mono i → HasLiftingProperty i p
Tactic: (_ : Mono i)
-- 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
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
⊢ HasLiftingProperty i p
have 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
Tactic: obtain ⟨J, _, _, _, _, ⟨h⟩⟩ :=
      generatingMonomorphisms.exists_transfiniteCompositionOfShape hG i
-- 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
inst_2 : IsGrothendieckAbelian.{w, v, u} C
⊢ HasSmallObjectArgument.{w, v, u} (generatingMonomorphisms G)
have obtain : ∀ (κ : Cardinal.{w}) (hκ' : κ.IsRegular) (hκ : HasCardinalLT (Subobject.{v, u} G) κ),
  HasSmallObjectArgument.{w, v, u} (generatingMonomorphisms G)
Tactic: obtain ⟨κ, hκ', hκ⟩ := HasCardinalLT.exists_regular_cardinal.{w} (Subobject G)
-- 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
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
⊢ HasSmallObjectArgument.{w, v, u} (generatingMonomorphisms G)
have this : Fact κ.IsRegular
Tactic: have : Fact κ.IsRegular := ⟨hκ'⟩
-- 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
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this : Fact κ.IsRegular
⊢ HasSmallObjectArgument.{w, v, u} (generatingMonomorphisms G)
have this₁ : Nonempty.{w + 1} κ.ord.ToType
Tactic: have : Nonempty κ.ord.ToType := by simpa using hκ'.ne_zero
-- 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
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
⊢ HasSmallObjectArgument.{w, v, u} (generatingMonomorphisms G)
have have : ∀ (this : OrderBot κ.ord.ToType), HasSmallObjectArgument.{w, v, u} (generatingMonomorphisms G)
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
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
⊢ 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 ⋯))
have 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 sorry))
Tactic: have := (hf.attachCells j hj).pushouts_coproducts