-- 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`, the colimit of `F` (computed in `C`) gives
a subobject of `F` which is a supremum of the subobjects corresponding to
the objects in the image of the functor `F`. -/
lemma subobjectMk_of_isColimit_eq_iSup :
    haveI := mono_of_isColimit_monoOver F hc f hf
    Subobject.mk f = ⨆ j, Subobject.mk (F.obj j).obj.hom

Proof state:
case a.h
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
this : Mono f
Z : C
g : Z ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
c' : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X) :=
  { pt := Z, ι := { app := fun j => Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯, naturality := ⋯ } }
⊢ Subobject.mk f ≤ Subobject.mk g

Tactic:
exact Subobject.mk_le_mk_of_comm (hc.desc c')
  (hc.hom_ext (fun j ↦ by rw [hc.fac_assoc c' j, hf, Subobject.ofMkLEMk_comp]))

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
this : Mono f✝
Z : C
g : Z ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
j j' : J
f : j ⟶ j'
⊢ (F ⋙ MonoOver.forget X ⋙ Over.forget X).map f ≫ (fun j => Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯) j' =
    (fun j => Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯) j ≫ ((Functor.const J).obj Z).map f

Tactic:
dsimp

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
this : Mono f✝
Z : C
g : Z ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
j j' : J
f : j ⟶ j'
⊢ ((MonoOver.forget X).map (F.map f)).left ≫ Subobject.ofMkLEMk (F.obj j').obj.hom g ⋯ =
    Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯ ≫ 𝟙 Z

Proof state:
case a
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
this : Mono f
⊢ Subobject.mk f ≤ ⨆ j, Subobject.mk (F.obj j).obj.hom

Tactic:
rw [le_iSup_iff]

Result:
case a
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
this : Mono f
⊢ ∀ (b : Subobject X), (∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ b) → Subobject.mk f ≤ b

Proof state:
case a.h
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
this : Mono f
Z : C
g : Z ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
⊢ Subobject.mk f ≤ Subobject.mk g

Tactic:
let c' : Cocone (F ⋙ MonoOver.forget _ ⋙ Over.forget _) := Cocone.mk Z
  { app j := Subobject.ofMkLEMk _ _ (H j)
    naturality j j' f := by
      dsimp
      simpa only [← cancel_mono g, Category.assoc, Subobject.ofMkLEMk_comp,
        Category.comp_id] using MonoOver.w (F.map f) }

Result:
case a.h
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
this : Mono f
Z : C
g : Z ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
c' : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X) :=
  { pt := Z, ι := { app := fun j => Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯, naturality := ⋯ } }
⊢ Subobject.mk f ≤ Subobject.mk g

Proof state:
case a
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
this : Mono f
⊢ ∀ (b : Subobject X), (∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ b) → Subobject.mk f ≤ b

Tactic:
intro s H

Result:
case a
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
this : Mono f
s : Subobject X
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ s
⊢ Subobject.mk f ≤ s

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
⊢ Subobject.mk f = ⨆ j, Subobject.mk (F.obj j).obj.hom

Tactic:
haveI := mono_of_isColimit_monoOver F hc f hf

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
this : Mono f
⊢ Subobject.mk f = ⨆ j, Subobject.mk (F.obj j).obj.hom

Proof state:
case a
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
this : Mono f
s : Subobject X
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ s
⊢ Subobject.mk f ≤ s

Tactic:
induction' s using Subobject.ind with Z g _

Result:
case a.h
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
this : Mono f
Z : C
g : Z ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
⊢ Subobject.mk f ≤ Subobject.mk g