-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
lemma generatingMonomorphisms_rlp [IsGrothendieckAbelian.{w} C] (hG : IsSeparator G) :
    (generatingMonomorphisms G).rlp = (monomorphisms C).rlp

Proof state:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (monomorphisms C).rlp ≤ (generatingMonomorphisms G).rlp

Tactic:
exact antitone_rlp (generatingMonomorphisms_le_monomorphisms _)

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
x✝ : Mono i
J : Type w
w✝³ : LinearOrder J
w✝² : OrderBot J
w✝¹ : SuccOrder J
w✝ : WellFoundedLT J
h : (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J i
⊢ (generatingMonomorphisms G).pushouts.rlp p

Tactic:
simpa

Result:
no goals

Proof state:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
x✝ : Mono i
⊢ HasLiftingProperty i p

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

Result:
case a.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
x✝ : Mono i
J : Type w
w✝³ : LinearOrder J
w✝² : OrderBot J
w✝¹ : SuccOrder J
w✝ : WellFoundedLT J
h : (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J i
⊢ HasLiftingProperty i p

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (generatingMonomorphisms G).rlp = (monomorphisms C).rlp

Tactic:
apply le_antisymm

Result:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (generatingMonomorphisms G).rlp ≤ (monomorphisms C).rlp

case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (monomorphisms C).rlp ≤ (generatingMonomorphisms G).rlp

Proof state:
case a.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
x✝ : Mono i
J : Type w
w✝³ : LinearOrder J
w✝² : OrderBot J
w✝¹ : SuccOrder J
w✝ : WellFoundedLT J
h : (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J i
⊢ HasLiftingProperty i p

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

Result:
no goals

Proof state:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (generatingMonomorphisms G).rlp ≤ (monomorphisms C).rlp

Tactic:
intro X Y p hp A B i (_ : Mono i)

Result:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
x✝ : Mono i
⊢ HasLiftingProperty i p