-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Colim.lean
/-- Assume that a functor `X : J ⥤ C` maps any morphism to a monomorphism,
that `J` is filtered. Then the "inclusion" map `c.ι.app j₀` of a colimit cocone for `X`
is a monomorphism if `colim : (Under j₀ ⥤ C) ⥤ C` preserves monomorphisms
(e.g. when `C` satisfies AB5). -/
lemma IsColimit.mono_ι_app_of_isFiltered
    {X : J ⥤ C} [∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)]
    {c : Cocone X} (hc : IsColimit c) [IsFiltered J] (j₀ : J)
    [HasColimitsOfShape (Under j₀) C]
    [(colim : (Under j₀ ⥤ C) ⥤ C).PreservesMonomorphisms] :
    Mono (c.ι.app j₀)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
f : (Functor.const (Under j₀)).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X := { app := fun j => X.map j.hom, naturality := ⋯ }
this : Mono f
⊢ Mono (c.ι.app j₀)

Tactic:
exact colim.map_mono' f (isColimitConstCocone _ _)
  ((Functor.Final.isColimitWhiskerEquiv _ _).symm hc) (c.ι.app j₀) (by aesop_cat)

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
x✝¹ x✝ : Under j₀
g : x✝¹ ⟶ x✝
⊢ ((Functor.const (Under j₀)).obj (X.obj j₀)).map g ≫ (fun j => X.map j.hom) x✝ =
    (fun j => X.map j.hom) x✝¹ ≫ (Under.forget j₀ ⋙ X).map g

Tactic:
dsimp

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
x✝¹ x✝ : Under j₀
g : x✝¹ ⟶ x✝
⊢ 𝟙 (X.obj j₀) ≫ X.map x✝.hom = X.map x✝¹.hom ≫ X.map g.right

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
f : (Functor.const (Under j₀)).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X := { app := fun j => X.map j.hom, naturality := ⋯ }
this : Mono f
⊢ ∀ (j : Under j₀),
    (constCocone (Under j₀) (X.obj j₀)).ι.app j ≫ c.ι.app j₀ = f.app j ≫ (Cocone.whisker (Under.forget j₀) c).ι.app j

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
⊢ Mono (c.ι.app j₀)

Tactic:
let f : (Functor.const _).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X :=
  { app j := X.map j.hom
    naturality _ _ g := by
      dsimp
      simp only [Category.id_comp, ← X.map_comp, Under.w] }

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
f : (Functor.const (Under j₀)).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X := { app := fun j => X.map j.hom, naturality := ⋯ }
⊢ Mono (c.ι.app j₀)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
f : (Functor.const (Under j₀)).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X := { app := fun j => X.map j.hom, naturality := ⋯ }
⊢ Mono (c.ι.app j₀)

Tactic:
have := NatTrans.mono_of_mono_app f

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
f : (Functor.const (Under j₀)).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X := { app := fun j => X.map j.hom, naturality := ⋯ }
this : Mono f
⊢ Mono (c.ι.app j₀)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
x✝¹ x✝ : Under j₀
g : x✝¹ ⟶ x✝
⊢ 𝟙 (X.obj j₀) ≫ X.map x✝.hom = X.map x✝¹.hom ≫ X.map g.right

Tactic:
simp only [Category.id_comp, ← X.map_comp, Under.w]

Result:
no goals