-- Mathlib/CategoryTheory/Monoidal/Yoneda.lean
lemma essImage_yonedaMon :
    yonedaMon (C := C).essImage = (· ⋙ forget _) ⁻¹' setOf Functor.IsRepresentable

Proof state:
case h.a.mpr.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
X : C
e : ((fun x => x ⋙ forget MonCat) F).RepresentableBy X
⊢ yonedaMon.essImage F

Tactic:
letI := Mon_ClassOfRepresentableBy X F e

Result:
case h.a.mpr.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
X : C
e : ((fun x => x ⋙ forget MonCat) F).RepresentableBy X
this : Mon_Class X := Mon_ClassOfRepresentableBy X F e
⊢ yonedaMon.essImage F

Proof state:
case h.a.mpr.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
X : C
e : ((fun x => x ⋙ forget MonCat) F).RepresentableBy X
this : Mon_Class X := Mon_ClassOfRepresentableBy X F e
⊢ yonedaMon.essImage F

Tactic:
exact ⟨Mon_.mk' X, ⟨yonedaMonObjMon_ClassOfRepresentableBy X F e⟩⟩

Result:
no goals

Proof state:
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
⊢ yonedaMon.essImage F ↔ ((fun x => x ⋙ forget MonCat) ⁻¹' setOf Functor.IsRepresentable) F

Tactic:
constructor

Result:
case h.a.mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
⊢ yonedaMon.essImage F → ((fun x => x ⋙ forget MonCat) ⁻¹' setOf Functor.IsRepresentable) F

case h.a.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
⊢ ((fun x => x ⋙ forget MonCat) ⁻¹' setOf Functor.IsRepresentable) F → yonedaMon.essImage F

Proof state:
case h.a.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
⊢ ((fun x => x ⋙ forget MonCat) ⁻¹' setOf Functor.IsRepresentable) F → yonedaMon.essImage F

Tactic:
rintro ⟨X, ⟨e⟩⟩

Result:
case h.a.mpr.mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
X : C
e : ((fun x => x ⋙ forget MonCat) F).RepresentableBy X
⊢ yonedaMon.essImage F

Proof state:
case h.a.mp.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
X : Mon_ C
α : yonedaMon.obj X ≅ F
⊢ ((fun x => x ⋙ forget MonCat) ⁻¹' setOf Functor.IsRepresentable) F

Tactic:
exact ⟨X.X, ⟨Functor.representableByEquiv.symm (isoWhiskerRight α (forget _))⟩⟩

Result:
no goals

Proof state:
case h.a.mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
⊢ yonedaMon.essImage F → ((fun x => x ⋙ forget MonCat) ⁻¹' setOf Functor.IsRepresentable) F

Tactic:
rintro ⟨X, ⟨α⟩⟩

Result:
case h.a.mp.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
X : Mon_ C
α : yonedaMon.obj X ≅ F
⊢ ((fun x => x ⋙ forget MonCat) ⁻¹' setOf Functor.IsRepresentable) F

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
⊢ yonedaMon.essImage = (fun x => x ⋙ forget MonCat) ⁻¹' setOf Functor.IsRepresentable

Tactic:
ext F

Result:
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
F : Cᵒᵖ ⥤ MonCat
⊢ yonedaMon.essImage F ↔ ((fun x => x ⋙ forget MonCat) ⁻¹' setOf Functor.IsRepresentable) F