-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
lemma llp_rlp_monomorphisms (hG : IsSeparator G) :
    (monomorphisms C).rlp.llp = monomorphisms C

Proof state:
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.llp = monomorphisms C

Tactic:
refine le_antisymm ?_ (le_llp_rlp _)

Result:
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.llp ≤ monomorphisms C

Proof state:
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.llp ≤ monomorphisms C

Tactic:
rw [← generatingMonomorphisms_rlp hG, llp_rlp_of_hasSmallObjectArgument]

Result:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts).retracts ≤
    monomorphisms C

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

Tactic:
apply retracts_monotone

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
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts ≤
    transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts

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

Tactic:
trans (transfiniteCompositions.{w} (coproducts.{w} (monomorphisms C)).pushouts).retracts

Result:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts).retracts ≤
    (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts).retracts

C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts).retracts ≤ monomorphisms C

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

Tactic:
apply pushouts_monotone

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

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

Tactic:
apply coproducts_monotone

Result:
case a.a.a.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 ≤ monomorphisms C

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
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts ≤
    transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts

Tactic:
apply transfiniteCompositions_monotone

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

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts).retracts ≤ monomorphisms C

Tactic:
simp

Result:
no goals

Proof state:
case a.a.a.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 ≤ monomorphisms C

Tactic:
apply generatingMonomorphisms_le_monomorphisms

Result:
no goals