-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
/-- Morphisms satisfying `(monomorphism C).presheaf` are in particular monomorphisms. -/
lemma presheaf_monomorphisms_le_monomorphisms :
    (monomorphisms C).presheaf ≤ monomorphisms _ := fun F G f hf ↦ by
  suffices ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b from
    ⟨fun _ _ h ↦ hom_ext_yoneda (fun _ _ ↦ this (by simp only [assoc, h]))⟩
  intro X a b h
  /- It suffices to show that the lifts of `a` and `b` to morphisms
  `X ⟶ hf.rep.pullback g` are equal, where `g = a ≫ f = a ≫ f`. -/
  suffices hf.rep.lift (g := a ≫ f) a (𝟙 X) (by simp) =
      hf.rep.lift b (𝟙 X) (by simp [← h]) by
    simpa using yoneda.congr_map this =≫ (hf.rep.fst (a ≫ f))
  -- This follows from the fact that the induced maps `hf.rep.pullback g ⟶ X` are mono.
  have : Mono (hf.rep.snd (a ≫ f)) := hf.property_snd (a ≫ f)
  simp only [← cancel_mono (hf.rep.snd (a ≫ f)), lift_snd]

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
this : ⋯.lift a (𝟙 X) ⋯ = ⋯.lift b (𝟙 X) ⋯
⊢ a = b

Tactic:
simpa using yoneda.congr_map this =≫ (hf.rep.fst (a ≫ f))

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
⊢ ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b

Tactic:
intro X a b h

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
⊢ a = b

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
⊢ b ≫ f = yoneda.map (𝟙 X) ≫ a ≫ f

Tactic:
simp [← h]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
⊢ a ≫ f = yoneda.map (𝟙 X) ≫ a ≫ f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
⊢ monomorphisms (Cᵒᵖ ⥤ Type v₁) f

Tactic:
suffices ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b from
  ⟨fun _ _ h ↦ hom_ext_yoneda (fun _ _ ↦ this (by simp only [assoc, h]))⟩

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
⊢ ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
this : Mono (⋯.snd (a ≫ f))
⊢ ⋯.lift a (𝟙 X) ⋯ = ⋯.lift b (𝟙 X) ⋯

Tactic:
simp only [← cancel_mono (hf.rep.snd (a ≫ f)), lift_snd]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
⊢ a = b

Tactic:
suffices hf.rep.lift (g := a ≫ f) a (𝟙 X) (by simp) =
    hf.rep.lift b (𝟙 X) (by simp [← h]) by
  simpa using yoneda.congr_map this =≫ (hf.rep.fst (a ≫ f))

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
⊢ ⋯.lift a (𝟙 X) ⋯ = ⋯.lift b (𝟙 X) ⋯

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
⊢ ⋯.lift a (𝟙 X) ⋯ = ⋯.lift b (𝟙 X) ⋯

Tactic:
have : Mono (hf.rep.snd (a ≫ f)) := hf.property_snd (a ≫ f)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
this : Mono (⋯.snd (a ≫ f))
⊢ ⋯.lift a (𝟙 X) ⋯ = ⋯.lift b (𝟙 X) ⋯

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
this : ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b
Z✝ : Cᵒᵖ ⥤ Type v₁
x✝³ x✝² : Z✝ ⟶ F
h : x✝³ ≫ f = x✝² ≫ f
x✝¹ : C
x✝ : yoneda.obj x✝¹ ⟶ Z✝
⊢ (x✝ ≫ x✝³) ≫ f = (x✝ ≫ x✝²) ≫ f

Tactic:
simp only [assoc, h]

Result:
no goals