-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
lemma exists_larger_subobject {X : C} (A : Subobject X) (hA : A ≠ ⊤) :
    ∃ (A' : Subobject X) (h : A < A'),
      (generatingMonomorphisms G).pushouts (Subobject.ofLE A A' h.le)

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 ≠ ⊤
⊢ ∃ A', ∃ (h : A < A'), (generatingMonomorphisms G).pushouts (A.ofLE A' ⋯)

Tactic:
induction' A using Subobject.ind with Y f _

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
f : Y ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ∃ A', ∃ (h : Subobject.mk f < A'), (generatingMonomorphisms G).pushouts ((Subobject.mk f).ofLE A' ⋯)

Proof state:
case h.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
f : Y ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : Y ⟶ X'
p' : X' ⟶ X
hi : (generatingMonomorphisms G).pushouts i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ (Subobject.underlyingIso f).hom ≫ i = (Subobject.mk f).ofLE (Subobject.mk p') ⋯ ≫ (Subobject.underlyingIso p').hom

Tactic:
simp only [← cancel_mono p', assoc, fac,
  Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow]

Result:
no goals

Proof state:
case h.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
f : Y ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : Y ⟶ X'
p' : X' ⟶ X
hi : (generatingMonomorphisms G).pushouts i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ (Subobject.underlyingIso f).hom ≫ (Arrow.mk i).hom =
    (Arrow.mk ((Subobject.mk f).ofLE (Subobject.mk p') ⋯)).hom ≫ (Subobject.underlyingIso p').hom

Tactic:
dsimp

Result:
case h.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
f : Y ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : Y ⟶ X'
p' : X' ⟶ X
hi : (generatingMonomorphisms G).pushouts i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ (Subobject.underlyingIso f).hom ≫ i = (Subobject.mk f).ofLE (Subobject.mk p') ⋯ ≫ (Subobject.underlyingIso p').hom

Proof state:
case h.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
f : Y ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : Y ⟶ X'
p' : X' ⟶ X
hi : (generatingMonomorphisms G).pushouts i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ ∃ A', ∃ (h : Subobject.mk f < A'), (generatingMonomorphisms G).pushouts ((Subobject.mk f).ofLE A' ⋯)

Tactic:
refine ⟨Subobject.mk p', Subobject.mk_lt_mk_of_comm i fac hi',
  (MorphismProperty.arrow_mk_iso_iff _ ?_).2 hi⟩

Result:
case h.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
f : Y ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : Y ⟶ X'
p' : X' ⟶ X
hi : (generatingMonomorphisms G).pushouts i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ Arrow.mk ((Subobject.mk f).ofLE (Subobject.mk p') ⋯) ≅ Arrow.mk i

Proof state:
case h.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
f : Y ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : Y ⟶ X'
p' : X' ⟶ X
hi : (generatingMonomorphisms G).pushouts i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ Arrow.mk ((Subobject.mk f).ofLE (Subobject.mk p') ⋯) ≅ Arrow.mk i

Tactic:
refine Arrow.isoMk (Subobject.underlyingIso f) (Subobject.underlyingIso p') ?_

Result:
case h.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
f : Y ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : Y ⟶ X'
p' : X' ⟶ X
hi : (generatingMonomorphisms G).pushouts i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ (Subobject.underlyingIso f).hom ≫ (Arrow.mk i).hom =
    (Arrow.mk ((Subobject.mk f).ofLE (Subobject.mk p') ⋯)).hom ≫ (Subobject.underlyingIso p').hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
f : Y ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ¬IsIso f

Tactic:
simpa only [Subobject.isIso_iff_mk_eq_top] using hA

Result:
no goals

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
f : Y ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ∃ A', ∃ (h : Subobject.mk f < A'), (generatingMonomorphisms G).pushouts ((Subobject.mk f).ofLE A' ⋯)

Tactic:
obtain ⟨X', i, p', hi, hi', hp', fac⟩ := exists_pushouts hG f
  (by simpa only [Subobject.isIso_iff_mk_eq_top] using hA)

Result:
case h.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
f : Y ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : Y ⟶ X'
p' : X' ⟶ X
hi : (generatingMonomorphisms G).pushouts i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ ∃ A', ∃ (h : Subobject.mk f < A'), (generatingMonomorphisms G).pushouts ((Subobject.mk f).ofLE A' ⋯)