-- Mathlib/CategoryTheory/Subpresheaf/OfSection.lean
lemma ofSection_eq_range' {X : Cᵒᵖ} (x : F.obj X) :
    ofSection x = range ((yonedaCompUliftFunctorEquiv F X.unop).symm x)

Proof state:
case obj.h.h.mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U → ∃ x_1, ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x).app U { down := x_1 } = y

Tactic:
rintro ⟨f, rfl⟩

Result:
case obj.h.h.mp.intro
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ ∃ x_1, ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x).app U { down := x_1 } = F.map f x

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
⊢ ofSection x = range ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x)

Tactic:
ext U y

Result:
case obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ y ∈ (range ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x)).obj U

Proof state:
case obj.h.h.mpr.intro
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : Opposite.unop U ⟶ Opposite.unop X
⊢ ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x).app U { down := f } ∈ (ofSection x).obj U

Tactic:
exact ⟨f.op, rfl⟩

Result:
no goals

Proof state:
case obj.h.h.mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ x_1, ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x).app U { down := x_1 } = y) →
    y ∈ (ofSection x).obj U

Tactic:
rintro ⟨f, rfl⟩

Result:
case obj.h.h.mpr.intro
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : Opposite.unop U ⟶ Opposite.unop X
⊢ ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x).app U { down := f } ∈ (ofSection x).obj U

Proof state:
case obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ y ∈ (range ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x)).obj U

Tactic:
simp only [Opposite.op_unop, range_obj, Functor.comp_obj, yoneda_obj_obj, uliftFunctor_obj,
  Set.mem_range, ULift.exists]

Result:
case obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ ∃ x_1, ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x).app U { down := x_1 } = y

Proof state:
case obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ ∃ x_1, ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x).app U { down := x_1 } = y

Tactic:
constructor

Result:
case obj.h.h.mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U → ∃ x_1, ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x).app U { down := x_1 } = y

case obj.h.h.mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ x_1, ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x).app U { down := x_1 } = y) →
    y ∈ (ofSection x).obj U

Proof state:
case obj.h.h.mp.intro
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ ∃ x_1, ((yonedaCompUliftFunctorEquiv F (Opposite.unop X)).symm x).app U { down := x_1 } = F.map f x

Tactic:
exact ⟨f.unop, rfl⟩

Result:
no goals