-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
/-- If `p : X ⟶ Y` is a monomorphism that is not an isomorphism, there exists
a subobject `X'` of `Y` containing `X` (but different from `X`) such that
the inclusion `X ⟶ X'` is a pushout of a monomorphism in the family
`generatingMonomorphisms G`. -/
lemma exists_pushouts
    {X Y : C} (p : X ⟶ Y) [Mono p] (hp : ¬ IsIso p) :
    ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : (generatingMonomorphisms G).pushouts i)
      (_ : ¬ IsIso i) (_ : Mono p'), i ≫ p' = p

Proof state:
case intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ ∃ X' i p', ∃ (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'), i ≫ p' = p

Tactic:
refine ⟨pushout (pullback.fst p f) (pullback.snd p f), pushout.inl _ _,
  pushout.desc p f pullback.condition,
  ⟨_, _, _, (Subobject.underlyingIso _).hom ≫ pullback.fst _ _,
  pushout.inr _ _, ⟨Subobject.mk (pullback.snd p f)⟩,
  (IsPushout.of_hasPushout (pullback.fst p f) (pullback.snd p f)).of_iso
    ((Subobject.underlyingIso _).symm) (Iso.refl _) (Iso.refl _)
    (Iso.refl _) (by simp) (by simp) (by simp) (by simp)⟩, ?_, ?_, by simp⟩

Result:
case intro.refine_1
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ ¬IsIso (pushout.inl (pullback.fst p f) (pullback.snd p f))

case intro.refine_2
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ Mono (pushout.desc p f ⋯)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
hp : ¬∀ s ∈ {G}, Function.Surjective ((coyoneda.obj (Opposite.op s)).map p)
⊢ ∃ X' i p', ∃ (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'), i ≫ p' = p

Tactic:
simp only [coyoneda_obj_obj, coyoneda_obj_map, Set.mem_singleton_iff, forall_eq,
  Function.Surjective, not_forall, not_exists] at hp

Result:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
hp : ∃ x, ∀ (x_1 : G ⟶ X), ¬x_1 ≫ p = x
⊢ ∃ X' i p', ∃ (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'), i ≫ p' = p

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ pushout.inl (pullback.fst p f) (pullback.snd p f) ≫ (Iso.refl (pushout (pullback.fst p f) (pullback.snd p f))).hom =
    (Iso.refl X).hom ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
hp : ¬IsIso p
⊢ ∃ X' i p', ∃ (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'), i ≫ p' = p

Tactic:
rw [hG.isDetector.isIso_iff_of_mono] at hp

Result:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
hp : ¬∀ s ∈ {G}, Function.Surjective ((coyoneda.obj (Opposite.op s)).map p)
⊢ ∃ X' i p', ∃ (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'), i ≫ p' = p

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ pushout.inl (pullback.fst p f) (pullback.snd p f) ≫ pushout.desc p f ⋯ = p

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ pullback.fst p f ≫ (Iso.refl X).hom =
    (Subobject.underlyingIso (pullback.snd p f)).symm.hom ≫
      (Subobject.underlyingIso (pullback.snd p f)).hom ≫ pullback.fst p f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ pushout.inr (pullback.fst p f) (pullback.snd p f) ≫ (Iso.refl (pushout (pullback.fst p f) (pullback.snd p f))).hom =
    (Iso.refl G).hom ≫ pushout.inr (pullback.fst p f) (pullback.snd p f)

Tactic:
simp

Result:
no goals

Proof state:
case intro.refine_1
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
h : IsIso (pushout.inl (pullback.fst p f) (pullback.snd p f))
⊢ False

Tactic:
rw [isIso_iff_yoneda_map_bijective] at h

Result:
case intro.refine_1
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
h : ∀ (T : C), Function.Bijective fun x => x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)
⊢ False

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ pushout.inr (pullback.fst p f) (pullback.snd p f) ≫ pushout.desc p f ⋯ = f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
h : ∀ (T : C), Function.Bijective fun x => x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)
a : G ⟶ X
ha :
  (fun x => x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)) a = pushout.inr (pullback.fst p f) (pullback.snd p f)
⊢ a ≫ p = f

Tactic:
simpa using ha =≫ pushout.desc p f pullback.condition

Result:
no goals

Proof state:
case intro.refine_2
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ Mono (pushout.desc p f ⋯)

Tactic:
exact (IsPushout.of_hasPushout _ _).mono_of_isPullback_of_mono
  (IsPullback.of_hasPullback p f) _ (by simp) (by simp)

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ pullback.snd p f ≫ (Iso.refl G).hom =
    (Subobject.underlyingIso (pullback.snd p f)).symm.hom ≫ (Subobject.mk (pullback.snd p f)).arrow

Tactic:
simp

Result:
no goals

Proof state:
case intro.refine_1
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ ¬IsIso (pushout.inl (pullback.fst p f) (pullback.snd p f))

Tactic:
intro h

Result:
case intro.refine_1
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
h : IsIso (pushout.inl (pullback.fst p f) (pullback.snd p f))
⊢ False

Proof state:
case intro.refine_1
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
h : ∀ (T : C), Function.Bijective fun x => x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)
⊢ False

Tactic:
obtain ⟨a, ha⟩ := (h G).2 (pushout.inr _ _)

Result:
case intro.refine_1.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
h : ∀ (T : C), Function.Bijective fun x => x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)
a : G ⟶ X
ha :
  (fun x => x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)) a = pushout.inr (pullback.fst p f) (pullback.snd p f)
⊢ False