-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Monomorphisms.lean
lemma mono : Mono f

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (monomorphisms C).TransfiniteCompositionOfShape J f
k k' : J
hkk' : k ⟶ k'
⊢ h.isoBot.inv ≫ h.F.map (homOfLE ⋯) = h.isoBot.inv ≫ h.F.map (homOfLE ⋯ ≫ hkk')

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (monomorphisms C).TransfiniteCompositionOfShape J f
k k' : J
hkk' : k ⟶ k'
⊢ 𝟙 X ≫ h.isoBot.inv ≫ h.F.map (homOfLE ⋯) = (h.isoBot.inv ≫ h.F.map (homOfLE ⋯)) ≫ h.F.map hkk'

Tactic:
rw [Category.id_comp, Category.assoc, ← Functor.map_comp]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (monomorphisms C).TransfiniteCompositionOfShape J f
k k' : J
hkk' : k ⟶ k'
⊢ h.isoBot.inv ≫ h.F.map (homOfLE ⋯) = h.isoBot.inv ≫ h.F.map (homOfLE ⋯ ≫ hkk')

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (monomorphisms C).TransfiniteCompositionOfShape J f
φ : (Functor.const J).obj X ⟶ h.F := { app := fun k => h.isoBot.inv ≫ h.F.map (homOfLE ⋯), naturality := ⋯ }
this : Mono φ
⊢ ∀ (j : J), (constCocone J X).ι.app j ≫ f = φ.app j ≫ { pt := Y, ι := h.incl }.ι.app j

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (monomorphisms C).TransfiniteCompositionOfShape J f
⊢ Mono f

Tactic:
let φ : (Functor.const _).obj X ⟶ h.F :=
  { app k := h.isoBot.inv ≫ h.F.map (homOfLE bot_le)
    naturality k k' hkk' := by
      dsimp
      rw [Category.id_comp, Category.assoc, ← Functor.map_comp]
      rfl }

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (monomorphisms C).TransfiniteCompositionOfShape J f
φ : (Functor.const J).obj X ⟶ h.F := { app := fun k => h.isoBot.inv ≫ h.F.map (homOfLE ⋯), naturality := ⋯ }
⊢ Mono f

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (monomorphisms C).TransfiniteCompositionOfShape J f
k k' : J
hkk' : k ⟶ k'
⊢ ((Functor.const J).obj X).map hkk' ≫ (fun k => h.isoBot.inv ≫ h.F.map (homOfLE ⋯)) k' =
    (fun k => h.isoBot.inv ≫ h.F.map (homOfLE ⋯)) k ≫ h.F.map hkk'

Tactic:
dsimp

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (monomorphisms C).TransfiniteCompositionOfShape J f
k k' : J
hkk' : k ⟶ k'
⊢ 𝟙 X ≫ h.isoBot.inv ≫ h.F.map (homOfLE ⋯) = (h.isoBot.inv ≫ h.F.map (homOfLE ⋯)) ≫ h.F.map hkk'

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (monomorphisms C).TransfiniteCompositionOfShape J f
φ : (Functor.const J).obj X ⟶ h.F := { app := fun k => h.isoBot.inv ≫ h.F.map (homOfLE ⋯), naturality := ⋯ }
this : Mono φ
⊢ Mono f

Tactic:
exact colim.map_mono' φ (isColimitConstCocone J X) (h.isColimit) f (by aesop_cat)

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (monomorphisms C).TransfiniteCompositionOfShape J f
φ : (Functor.const J).obj X ⟶ h.F := { app := fun k => h.isoBot.inv ≫ h.F.map (homOfLE ⋯), naturality := ⋯ }
⊢ Mono f

Tactic:
have : Mono φ := NatTrans.mono_of_mono_app φ

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (monomorphisms C).TransfiniteCompositionOfShape J f
φ : (Functor.const J).obj X ⟶ h.F := { app := fun k => h.isoBot.inv ≫ h.F.map (homOfLE ⋯), naturality := ⋯ }
this : Mono φ
⊢ Mono f