awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
p : F' ⟶ F
rw : (range (G.preimage p).ι).image p ≤ G
rw₁ : (G.preimage p).image p ≤ G
rw₂ rw₃ : G.preimage p ≤ G.preimage p
⊢ range ((G.preimage p).ι ≫ p) ≤ G

Tactic:
rw [range_comp, range_ι, image_le_iff]

Premises used: CategoryTheory.Subfunctor.image_le_iff, CategoryTheory.Subfunctor.range_ι, CategoryTheory.Subfunctor.range_comp
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
p : F' ⟶ F
⊢ G.fromPreimage p ≫ G.ι = (G.preimage p).ι ≫ p

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, CategoryTheory.Subfunctor.ι, CategoryTheory.Subfunctor.lift, CategoryTheory.Subfunctor.fromPreimage, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
p : F' ⟶ F
rw : G.preimage p = ⊤ ↔ ⊤ ≤ G.preimage p
⊢ G.preimage p = ⊤ ↔ range p ≤ G

Tactic:
rw [← image_top, image_le_iff]

Premises used: CategoryTheory.Subfunctor.image_le_iff, CategoryTheory.Subfunctor.image_top
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
p : F' ⟶ F
⊢ G.preimage p = ⊤ ↔ ⊤ ≤ G.preimage p

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
a : (G.preimage p).image p ≤ G
a₁ : G ≤ (G.preimage p).image p
⊢ (G.preimage p).image p = G

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
a a₁ : G.preimage p ≤ G.preimage p
⊢ (G.preimage p).image p ≤ G

Tactic:
rw [image_le_iff]

Premises used: CategoryTheory.Subfunctor.image_le_iff
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
i : C
x : F.obj i
hx : x ∈ G.obj i
⊢ ∀ (k : C),
    Function.Surjective (α := F'.obj k) (β := F.obj k)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app k)) : (a : F'.obj k) → F.obj k)

Tactic:
simp only [NatTrans.epi_iff_epi_app, epi_iff_surjective] at hp

Premises used: CategoryTheory.NatTrans.epi_iff_epi_app, CategoryTheory.epi_iff_surjective
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
p : F' ⟶ F
i : C
x : F.obj i
hx : x ∈ G.obj i
hp :
  ∀ (k : C),
    Function.Surjective (α := F'.obj k) (β := F.obj k)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app k)) : (a : F'.obj k) → F.obj k)
a :
  ∀ (y : F'.obj i)
    (hx :
      Membership.mem (α := F.obj i) (G.obj i)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y : F.obj i)),
    Membership.mem (α := F.obj i) (((G.preimage p).image p).obj i)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y : F.obj i)
⊢ x ∈ ((G.preimage p).image p).obj i

Tactic:
obtain ⟨y, rfl⟩ := hp _ x

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
p : F' ⟶ F
i : C
hp :
  ∀ (k : C),
    Function.Surjective (α := F'.obj k) (β := F.obj k)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app k)) : (a : F'.obj k) → F.obj k)
y : F'.obj i
hx :
  Membership.mem (α := F.obj i) (G.obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y : F.obj i)
⊢ Membership.mem (α := F.obj i) (((G.preimage p).image p).obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y : F.obj i)

Tactic:
⟨y, hx, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
p : F' ⟶ F
i : C
hp :
  ∀ (k : C),
    Function.Surjective (α := F'.obj k) (β := F.obj k)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app k)) : (a : F'.obj k) → F.obj k)
y : F'.obj i
hx :
  Membership.mem (α := F.obj i) (G.obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y : F.obj i)
⊢ Membership.mem (α := F.obj i) (((G.preimage p).image p).obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y : F.obj i)

Tactic:
exact ⟨y, hx, rfl⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
U V : Cᵒᵖ
g : U ⟶ V
f : X ⟶ U
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ≫ g)) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj V))
        x :
      (fun (X : Type w) ↦ X) (F.obj V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj U))
            x :
          (fun (X : Type w) ↦ X) (F.obj U)) :
      (fun (X : Type w) ↦ X) (F.obj V))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
U V : Cᵒᵖ
g : U ⟶ V
f : X ⟶ U
⊢ Membership.mem (α := F.obj U) (γ := Set (F.obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj V))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
      {u : F.obj V |
        ∃ (f : X ⟶ V),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj V))
              x =
            u})
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj U))
        x :
      (fun (X : Type w) ↦ X) (F.obj U))

Tactic:
exact ⟨f ≫ g, by simp⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 X)) :
        (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj X))
      x =
    x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
mp : ofSection x ≤ G → x ∈ G.obj X
mpr : x ∈ G.obj X → ofSection x ≤ G
⊢ ofSection x ≤ G ↔ x ∈ G.obj X

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
hx : ofSection x ≤ G
⊢ x ∈ G.obj X

Tactic:
hx _ (mem_ofSection_obj x)

Premises used: CategoryTheory.Subfunctor.mem_ofSection_obj
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
hx : ofSection x ≤ G
⊢ x ∈ G.obj X

Tactic:
exact hx _ (mem_ofSection_obj x)

Premises used: CategoryTheory.Subfunctor.mem_ofSection_obj
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
hx : x ∈ G.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ Membership.mem (α := F.obj U) (G.obj U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj U))
        x :
      (fun (X : Type w) ↦ X) (F.obj U))

Tactic:
G.map f hx

Premises used: Set.Mem, setOf, CategoryTheory.Subfunctor.map, Set.preimage
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
hx : x ∈ G.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ Membership.mem (α := F.obj U) (G.obj U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj U))
        x :
      (fun (X : Type w) ↦ X) (F.obj U))

Tactic:
exact G.map f hx

Premises used: CategoryTheory.Subfunctor.map
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
a :
  (ofSection x).image f ≤
    ofSection (X := X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
        x)
a₁ :
  ofSection (X := X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
        x) ≤
    (ofSection x).image f
⊢ (ofSection x).image f =
    ofSection (X := X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
        x)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
a :
  Membership.mem (α := (fun (X : Type w) ↦ X) (F'.obj X)) (γ := Set ((fun (X : Type w) ↦ X) (F'.obj X)))
    (obj
      (ofSection (X := X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
            (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
          x))
      X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
        x :
      (fun (X : Type w) ↦ X) (F'.obj X))
⊢ (ofSection x).image f ≤
    ofSection (X := X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
        x)

Tactic:
rw [image_le_iff, ofSection_le_iff, preimage_obj, Set.mem_preimage]

Premises used: CategoryTheory.Subfunctor.image_le_iff, CategoryTheory.Subfunctor.preimage_obj, CategoryTheory.Subfunctor.ofSection_le_iff, Set.mem_preimage
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
⊢ Eq (α := (fun (X : Type w) ↦ X) (F'.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map (𝟙 X)) :
          (a : (fun (X : Type w) ↦ X) (F'.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
            x :
          (fun (X : Type w) ↦ X) (F'.obj X)) :
      (fun (X : Type w) ↦ X) (F'.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
        x :
      (fun (X : Type w) ↦ X) (F'.obj X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
⊢ Membership.mem (α := (fun (X : Type w) ↦ X) (F'.obj X)) (γ := Set ((fun (X : Type w) ↦ X) (F'.obj X)))
    (obj
      (ofSection (X := X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
            (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
          x))
      X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
        x :
      (fun (X : Type w) ↦ X) (F'.obj X))

Tactic:
exact ⟨𝟙 X, by simp⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
a :
  ∃ x_1 ∈ (ofSection x).obj X,
    Eq (α := F'.obj X) ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : F.obj X) → F'.obj X) x_1 : F'.obj X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : F.obj X) → F'.obj X) x : F'.obj X)
⊢ ofSection (X := X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F'.obj X))
        x) ≤
    (ofSection x).image f

Tactic:
simp only [ofSection_le_iff, image_obj, Set.mem_image]

Premises used: Set.mem_image, CategoryTheory.Subfunctor.image_obj, CategoryTheory.Subfunctor.ofSection_le_iff
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
⊢ ∃ x_1 ∈ (ofSection x).obj X,
    Eq (α := F'.obj X) ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : F.obj X) → F'.obj X) x_1 : F'.obj X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : F.obj X) → F'.obj X) x : F'.obj X)

Tactic:
⟨x, mem_ofSection_obj x, rfl⟩

Premises used: And.intro, CategoryTheory.Subfunctor.mem_ofSection_obj, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
⊢ ∃ x_1 ∈ (ofSection x).obj X,
    Eq (α := F'.obj X) ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : F.obj X) → F'.obj X) x_1 : F'.obj X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : F.obj X) → F'.obj X) x : F'.obj X)

Tactic:
exact ⟨x, mem_ofSection_obj x, rfl⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : Cᵒᵖ
x : F.obj X
obj :
  ∀ (U : Cᵒᵖ) (y : F.obj U),
    y ∈ (ofSection x).obj U ↔
      Membership.mem (γ := Set (F.obj U))
        (Subfunctor.obj
          (range (F' := Functor.obj yoneda (Opposite.unop X))
            ((Equiv.symm yonedaEquiv : (a : F.obj (Opposite.op (Opposite.unop X))) → yoneda.obj (Opposite.unop X) ⟶ F)
              x))
          U)
        y
⊢ ofSection x =
    range (F' := Functor.obj yoneda (Opposite.unop X))
      ((Equiv.symm yonedaEquiv : (a : F.obj (Opposite.op (Opposite.unop X))) → yoneda.obj (Opposite.unop X) ⟶ F) x)

Tactic:
ext U y
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
obj :
  (∃ (f : X ⟶ U), (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x = y) ↔
    ∃ (y_1 : Opposite.unop U ⟶ Opposite.unop X),
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
            (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
          y_1 =
        y
⊢ y ∈ (ofSection x).obj U ↔
    Membership.mem (γ := Set (F.obj U))
      (Subfunctor.obj
        (range (F' := Functor.obj yoneda (Opposite.unop X))
          ((Equiv.symm yonedaEquiv : (a : F.obj (Opposite.op (Opposite.unop X))) → yoneda.obj (Opposite.unop X) ⟶ F) x))
        U)
      y

Tactic:
simp only [ofSection_obj, Set.mem_setOf_eq, Opposite.op_unop, range_obj, yoneda_obj_obj,
    Set.mem_range]

Premises used: Set.mem_range, Opposite.op_unop, CategoryTheory.Subfunctor.ofSection_obj, CategoryTheory.yoneda_obj_obj, Set.mem_setOf_eq, CategoryTheory.Subfunctor.range_obj
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
obj :
  (∃ (f : X ⟶ U), (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x = y) →
    ∃ (y_1 : Opposite.unop U ⟶ Opposite.unop X),
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
            (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
          y_1 =
        y
obj₁ :
  (∃ (y_1 : Opposite.unop U ⟶ Opposite.unop X),
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
            (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
          y_1 =
        y) →
    ∃ (f : X ⟶ U), (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x = y
⊢ (∃ (f : X ⟶ U), (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x = y) ↔
    ∃ (y_1 : Opposite.unop U ⟶ Opposite.unop X),
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
            (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
          y_1 =
        y

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ ∃ (y : Opposite.unop U ⟶ Opposite.unop X),
    Eq (α := F.obj U)
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
            (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
          y :
        F.obj U)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x : F.obj U)

Tactic:
⟨f.unop, rfl⟩

Premises used: Quiver.Hom.unop, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ ∃ (y : Opposite.unop U ⟶ Opposite.unop X),
    Eq (α := F.obj U)
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
            (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
          y :
        F.obj U)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x : F.obj U)

Tactic:
exact ⟨f.unop, rfl⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : Opposite.unop U ⟶ Opposite.unop X
⊢ ∃ (f_1 : X ⟶ U),
    Eq (α := F.obj U) ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1) : (a : F.obj X) → F.obj U) x : F.obj U)
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
            (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
          f :
        F.obj U)

Tactic:
⟨f.op, rfl⟩

Premises used: Quiver.Hom.op, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : Opposite.unop U ⟶ Opposite.unop X
⊢ ∃ (f_1 : X ⟶ U),
    Eq (α := F.obj U) ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1) : (a : F.obj X) → F.obj U) x : F.obj U)
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
            (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
          f :
        F.obj U)

Tactic:
exact ⟨f.op, rfl⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : C
f : Functor.obj yoneda X ⟶ F
rw :
  range f =
    range (F' := Functor.obj yoneda (Opposite.unop (Opposite.op X)))
      ((Equiv.symm yonedaEquiv :
          (a : F.obj (Opposite.op (Opposite.unop (Opposite.op X)))) → yoneda.obj (Opposite.unop (Opposite.op X)) ⟶ F)
        ((yonedaEquiv : (a : yoneda.obj X ⟶ F) → F.obj (Opposite.op X)) f))
rw₁ rw₂ : range f = range f
⊢ range f = ofSection (X := Opposite.op X) ((yonedaEquiv : (a : yoneda.obj X ⟶ F) → F.obj (Opposite.op X)) f)

Tactic:
rw [ofSection_eq_range, Equiv.symm_apply_apply]

Premises used: CategoryTheory.Subfunctor.ofSection_eq_range, Equiv.symm_apply_apply
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
obj :
  ∀ (U : Cᵒᵖ) (y : F.obj U),
    y ∈ (ofSection x).obj U ↔
      Membership.mem (γ := Set (F.obj U))
        (Subfunctor.obj
          (range (F' := Functor.obj uliftYoneda.{w, v, u} (Opposite.unop X))
            ((Equiv.symm uliftYonedaEquiv :
                (a : F.obj (Opposite.op (Opposite.unop X))) → uliftYoneda.{w, v, u}.obj (Opposite.unop X) ⟶ F)
              x))
          U)
        y
⊢ ofSection x =
    range (F' := Functor.obj uliftYoneda.{w, v, u} (Opposite.unop X))
      ((Equiv.symm uliftYonedaEquiv :
          (a : F.obj (Opposite.op (Opposite.unop X))) → uliftYoneda.{w, v, u}.obj (Opposite.unop X) ⟶ F)
        x)

Tactic:
ext U y
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
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
obj :
  y ∈ (ofSection x).obj U ↔
    Membership.mem (γ := Set (F.obj U))
      (Set.range fun (y : ULift.{w, v} (Opposite.unop U ⟶ Opposite.unop X)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map y.down.op) : (a : F.obj X) → F.obj U) x)
      y
⊢ y ∈ (ofSection x).obj U ↔
    Membership.mem (γ := Set (F.obj U))
      (Subfunctor.obj
        (range (F' := Functor.obj uliftYoneda.{w, v, u} (Opposite.unop X))
          ((Equiv.symm uliftYonedaEquiv :
              (a : F.obj (Opposite.op (Opposite.unop X))) → uliftYoneda.{w, v, u}.obj (Opposite.unop X) ⟶ F)
            x))
        U)
      y

Tactic:
dsimp [uliftYonedaEquiv]

Premises used: CategoryTheory.uliftYonedaEquiv
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
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
obj :
  y ∈ (ofSection x).obj U ↔
    ∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x = y
⊢ y ∈ (ofSection x).obj U ↔
    Membership.mem (γ := Set (F.obj U))
      (Set.range fun (y : ULift.{w, v} (Opposite.unop U ⟶ Opposite.unop X)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map y.down.op) : (a : F.obj X) → F.obj U) x)
      y

Tactic:
simp only [Set.mem_range, ULift.exists]

Premises used: Set.mem_range, ULift.exists
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
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
obj :
  y ∈ (ofSection x).obj U →
    ∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x = y
obj₁ :
  (∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x = y) →
    y ∈ (ofSection x).obj U
⊢ y ∈ (ofSection x).obj U ↔
    ∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x = y

Tactic:
constructor