-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean
/-- If `C` is a Grothendieck abelian category, `X : C`, if `F : J ⥤ MonoOver X` is a
functor from a filtered category `J`, `c` is a colimit cocone for the corresponding
functor `J ⥤ C`, and `f : c.pt ⟶ X` is induced by the inclusions,
then `f` is a monomorphism. -/
lemma mono_of_isColimit_monoOver : Mono f

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
α : F ⋙ MonoOver.forget X ⋙ Over.forget X ⟶ (Functor.const J).obj X :=
  { app := fun j => (F.obj j).obj.hom, naturality := ⋯ }
⊢ Mono f

Tactic:
have := NatTrans.mono_of_mono_app α

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
α : F ⋙ MonoOver.forget X ⋙ Over.forget X ⟶ (Functor.const J).obj X :=
  { app := fun j => (F.obj j).obj.hom, naturality := ⋯ }
this : Mono α
⊢ Mono f

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
⊢ Mono f

Tactic:
let α : F ⋙ MonoOver.forget _ ⋙ Over.forget _ ⟶ (Functor.const _).obj X :=
  { app j := (F.obj j).obj.hom
    naturality _ _ f := (F.map f).w }

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
α : F ⋙ MonoOver.forget X ⋙ Over.forget X ⟶ (Functor.const J).obj X :=
  { app := fun j => (F.obj j).obj.hom, naturality := ⋯ }
⊢ Mono f

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
α : F ⋙ MonoOver.forget X ⋙ Over.forget X ⟶ (Functor.const J).obj X :=
  { app := fun j => (F.obj j).obj.hom, naturality := ⋯ }
this : Mono α
⊢ Mono f

Tactic:
exact colim.map_mono' α hc (isColimitConstCocone J X) f (by simpa using hf)

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
α : F ⋙ MonoOver.forget X ⋙ Over.forget X ⟶ (Functor.const J).obj X :=
  { app := fun j => (F.obj j).obj.hom, naturality := ⋯ }
this : Mono α
⊢ ∀ (j : J), c.ι.app j ≫ f = α.app j ≫ (constCocone J X).ι.app j

Tactic:
simpa using hf

Result:
no goals