-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
lemma pushouts_ofLE_le_largerSubobject (A : Subobject X) :
      (generatingMonomorphisms G).pushouts
        (Subobject.ofLE _ _ (le_largerSubobject hG A))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
⊢ largerSubobject hG ⊤ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
this : IsIso (largerSubobject hG ⊤).arrow
⊢ (asIso ⊤.arrow).hom ≫ (Arrow.mk (𝟙 X)).hom =
    (Arrow.mk (⊤.ofLE (largerSubobject hG ⊤) ⋯)).hom ≫ (asIso (largerSubobject hG ⊤).arrow).hom

Tactic:
simp

Result:
no goals

Proof state:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ Arrow.mk (A.ofLE ⋯.choose ⋯) ≅ Arrow.mk (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
exact Arrow.isoMk (Iso.refl _)
  (Subobject.isoOfEq _ _ ((by simp [largerSubobject, dif_neg hA])))

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ ⋯.choose = largerSubobject hG A

Tactic:
simp [largerSubobject, dif_neg hA]

Result:
no goals

Proof state:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ (generatingMonomorphisms G).pushouts (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
refine (MorphismProperty.arrow_mk_iso_iff _ ?_).1
  (exists_larger_subobject hG A hA).choose_spec.choose_spec

Result:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ Arrow.mk (A.ofLE ⋯.choose ⋯) ≅ Arrow.mk (A.ofLE (largerSubobject hG A) ⋯)

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
this : IsIso (largerSubobject hG ⊤).arrow
⊢ (generatingMonomorphisms G).pushouts (⊤.ofLE (largerSubobject hG ⊤) ⋯)

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff _
  (Arrow.isoMk (asIso (Subobject.arrow _)) (asIso (Subobject.arrow _)) (by simp))).2
    (isomorphisms_le_pushouts_generatingMonomorphisms G (𝟙 X)
      (MorphismProperty.isomorphisms.infer_property _))

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
⊢ (generatingMonomorphisms G).pushouts (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
by_cases hA : A = ⊤

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A = ⊤
⊢ (generatingMonomorphisms G).pushouts (A.ofLE (largerSubobject hG A) ⋯)

case neg
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ (generatingMonomorphisms G).pushouts (A.ofLE (largerSubobject hG A) ⋯)

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
⊢ (generatingMonomorphisms G).pushouts (⊤.ofLE (largerSubobject hG ⊤) ⋯)

Tactic:
have := (Subobject.isIso_arrow_iff_eq_top (largerSubobject hG (⊤ : Subobject X))).2 (by simp)

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
this : IsIso (largerSubobject hG ⊤).arrow
⊢ (generatingMonomorphisms G).pushouts (⊤.ofLE (largerSubobject hG ⊤) ⋯)

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A = ⊤
⊢ (generatingMonomorphisms G).pushouts (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
subst hA

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
⊢ (generatingMonomorphisms G).pushouts (⊤.ofLE (largerSubobject hG ⊤) ⋯)