awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
Y : C
f : Y ⟶ X
⊢ Eq.{w + 1} (α := F.obj (op Y))
    (((h.representableBy.homEquiv : Equiv.{v + 1, w + 1} (Y ⟶ X) (F.obj (op Y))) : (a : Y ⟶ X) → F.obj (op Y)) f :
      F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x :
      (fun (X : Type w) ↦ X) (F.obj (op Y)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
R : F.RepresentableBy X
rw :
  IsIso (C := Cᵒᵖ ⥤ Type (max w v)) (X := (obj uliftYoneda.{w, v, u} X : Cᵒᵖ ⥤ Type (max w v))) (Y :=
    F ⋙ uliftFunctor.{v, w})
    ((Equiv.symm uliftYonedaEquiv :
          (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
        { down := ((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) } :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
⊢ F.IsRepresentedBy (X := X)
    (((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X))

Tactic:
rw [IsRepresentedBy.iff_isIso_uliftYonedaEquiv]

Premises used: CategoryTheory.Functor.IsRepresentedBy.iff_isIso_uliftYonedaEquiv
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
R : F.RepresentableBy X
⊢ IsIso (C := Cᵒᵖ ⥤ Type (max w v)) (X := (obj uliftYoneda.{w, v, u} X : Cᵒᵖ ⥤ Type (max w v))) (Y :=
    F ⋙ uliftFunctor.{v, w})
    (Iso.hom
        ((equivUliftYonedaIso (F ⋙ uliftFunctor.{v, w}) X :
            (a : (F ⋙ uliftFunctor.{v, w}).RepresentableBy X) → uliftYoneda.{w, v, u}.obj X ≅ F ⋙ uliftFunctor.{v, w})
          ((Equiv.symm representableByUliftFunctorEquiv :
              (a : F.RepresentableBy X) → (F ⋙ uliftFunctor.{v, w}).RepresentableBy X)
            R)) :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})

Tactic:
(RepresentableBy.equivUliftYonedaIso _ _ <|
        representableByUliftFunctorEquiv.{v}.symm R).isIso_hom

Premises used: CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso, CategoryTheory.Functor.representableByUliftFunctorEquiv, CategoryTheory.Iso.isIso_hom, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
R : F.RepresentableBy X
h :
  Eq (α := obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
    ((Equiv.symm uliftYonedaEquiv :
          (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
        { down := ((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) } :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
    (Iso.hom
        ((equivUliftYonedaIso (F ⋙ uliftFunctor.{v, w}) X :
            (a : (F ⋙ uliftFunctor.{v, w}).RepresentableBy X) → uliftYoneda.{w, v, u}.obj X ≅ F ⋙ uliftFunctor.{v, w})
          ((Equiv.symm representableByUliftFunctorEquiv :
              (a : F.RepresentableBy X) → (F ⋙ uliftFunctor.{v, w}).RepresentableBy X)
            R)) :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
⊢ IsIso (C := Cᵒᵖ ⥤ Type (max w v)) (X := (obj uliftYoneda.{w, v, u} X : Cᵒᵖ ⥤ Type (max w v))) (Y :=
    F ⋙ uliftFunctor.{v, w})
    ((Equiv.symm uliftYonedaEquiv :
          (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
        { down := ((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) } :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})

Tactic:
convert!
    (RepresentableBy.equivUliftYonedaIso _ _ <|
        representableByUliftFunctorEquiv.{v}.symm R).isIso_hom
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
R : F.RepresentableBy X
h :
  ∀ (x : Cᵒᵖ) (x_1 : obj (obj uliftYoneda.{w, v, u} X) x),
    Eq (α := (F ⋙ uliftFunctor.{v, w}).obj x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((Equiv.symm uliftYonedaEquiv :
                (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
              {
                down :=
                  ((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) :
                ULift.{v, w} (F.obj (op X)) })
            x))
        x_1)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Iso.hom
              ((equivUliftYonedaIso (F ⋙ uliftFunctor.{v, w}) X :
                  (a : (F ⋙ uliftFunctor.{v, w}).RepresentableBy X) →
                    uliftYoneda.{w, v, u}.obj X ≅ F ⋙ uliftFunctor.{v, w})
                ((Equiv.symm representableByUliftFunctorEquiv :
                    (a : F.RepresentableBy X) → (F ⋙ uliftFunctor.{v, w}).RepresentableBy X)
                  R)))
            x))
        x_1)
⊢ Eq (α := obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
    ((Equiv.symm uliftYonedaEquiv :
          (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
        { down := ((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) } :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
    (Iso.hom
        ((equivUliftYonedaIso (F ⋙ uliftFunctor.{v, w}) X :
            (a : (F ⋙ uliftFunctor.{v, w}).RepresentableBy X) → uliftYoneda.{w, v, u}.obj X ≅ F ⋙ uliftFunctor.{v, w})
          ((Equiv.symm representableByUliftFunctorEquiv :
              (a : F.RepresentableBy X) → (F ⋙ uliftFunctor.{v, w}).RepresentableBy X)
            R)) :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})

Tactic:
ext
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
R : F.RepresentableBy X
x : Cᵒᵖ
x_1 : obj (obj uliftYoneda.{w, v, u} X) x
⊢ Eq (α := (F ⋙ uliftFunctor.{v, w}).obj x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((Equiv.symm uliftYonedaEquiv :
              (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
            { down := ((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) :
              ULift.{v, w} (F.obj (op X)) })
          x))
      x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
            ((equivUliftYonedaIso (F ⋙ uliftFunctor.{v, w}) X :
                (a : (F ⋙ uliftFunctor.{v, w}).RepresentableBy X) →
                  uliftYoneda.{w, v, u}.obj X ≅ F ⋙ uliftFunctor.{v, w})
              ((Equiv.symm representableByUliftFunctorEquiv :
                  (a : F.RepresentableBy X) → (F ⋙ uliftFunctor.{v, w}).RepresentableBy X)
                R)))
          x))
      x_1)

Tactic:
simpa [uliftYonedaEquiv] using (homEquiv_eq _ _).symm

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_eq, Eq.symm, CategoryTheory.uliftYonedaEquiv
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
⊢ ((h.representableBy.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) = x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
e : F ≅ F'
rw :
  ∃ (R : F'.RepresentableBy X),
    Eq.{w + 1} (α := F'.obj (op X))
      (((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F'.obj (op X))) : (a : X ⟶ X) → F'.obj (op X)) (𝟙 X) :
        F'.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op X)) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F'.obj (op X)))
          x :
        (fun (X : Type w) ↦ X) (F'.obj (op X)))
⊢ F'.IsRepresentedBy (X := X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op X)) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F'.obj (op X)))
      x)

Tactic:
rw [iff_exists_representableBy]

Premises used: CategoryTheory.Functor.IsRepresentedBy.iff_exists_representableBy
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
e : F ≅ F'
h₁ :
  Eq.{w + 1} (α := F'.obj (op X))
    ((((h.representableBy.ofIso e).homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F'.obj (op X))) :
          (a : X ⟶ X) → F'.obj (op X))
        (𝟙 X) :
      F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op X)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F'.obj (op X)))
        x :
      (fun (X : Type w) ↦ X) (F'.obj (op X)))
⊢ ∃ (R : F'.RepresentableBy X),
    Eq.{w + 1} (α := F'.obj (op X))
      (((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F'.obj (op X))) : (a : X ⟶ X) → F'.obj (op X)) (𝟙 X) :
        F'.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op X)) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F'.obj (op X)))
          x :
        (fun (X : Type w) ↦ X) (F'.obj (op X)))

Tactic:
use h.representableBy.ofIso e

Premises used: CategoryTheory.Functor.IsRepresentedBy.representableBy, CategoryTheory.Functor.RepresentableBy.ofIso
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
e : F ≅ F'
⊢ Eq.{w + 1} (α := F'.obj (op X))
    ((((h.representableBy.ofIso e).homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F'.obj (op X))) :
          (a : X ⟶ X) → F'.obj (op X))
        (𝟙 X) :
      F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op X)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F'.obj (op X)))
        x :
      (fun (X : Type w) ↦ X) (F'.obj (op X)))

Tactic:
simp [RepresentableBy.ofIso]

Premises used: CategoryTheory.Functor.RepresentableBy.ofIso
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
e : F ≅ F'
h :
  F'.IsRepresentedBy (X := X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op X)) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F'.obj (op X)))
      x)
⊢ F.IsRepresentedBy x

Tactic:
simpa using h.of_natIso e.symm

Premises used: CategoryTheory.Functor.IsRepresentedBy.of_natIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
Y : C
e : Y ≅ X
rw :
  ∃ (R : F.RepresentableBy Y),
    Eq.{w + 1} (α := F.obj (op Y))
      (((R.homEquiv : Equiv.{v + 1, w + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
          x :
        (fun (X : Type w) ↦ X) (F.obj (op Y)))
⊢ F.IsRepresentedBy (X := Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
      x)

Tactic:
rw [iff_exists_representableBy]

Premises used: CategoryTheory.Functor.IsRepresentedBy.iff_exists_representableBy
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
Y : C
e : Y ≅ X
h₁ :
  Eq.{w + 1} (α := F.obj (op Y))
    ((((h.representableBy.ofIsoObj e).homEquiv : Equiv.{v + 1, w + 1} (Y ⟶ Y) (F.obj (op Y))) :
          (a : Y ⟶ Y) → F.obj (op Y))
        (𝟙 Y) :
      F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x :
      (fun (X : Type w) ↦ X) (F.obj (op Y)))
⊢ ∃ (R : F.RepresentableBy Y),
    Eq.{w + 1} (α := F.obj (op Y))
      (((R.homEquiv : Equiv.{v + 1, w + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
          x :
        (fun (X : Type w) ↦ X) (F.obj (op Y)))

Tactic:
use h.representableBy.ofIsoObj e

Premises used: CategoryTheory.Functor.IsRepresentedBy.representableBy, CategoryTheory.Functor.RepresentableBy.ofIsoObj
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
Y : C
e : Y ≅ X
⊢ Eq.{w + 1} (α := F.obj (op Y))
    ((((h.representableBy.ofIsoObj e).homEquiv : Equiv.{v + 1, w + 1} (Y ⟶ Y) (F.obj (op Y))) :
          (a : Y ⟶ Y) → F.obj (op Y))
        (𝟙 Y) :
      F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x :
      (fun (X : Type w) ↦ X) (F.obj (op Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
Y : C
e : Y ≅ X
⊢ F.IsRepresentedBy (X := Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x) ↔
    F.IsRepresentedBy x

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.of_isoObj e⟩

Premises used: Iff.intro, CategoryTheory.Functor.IsRepresentedBy.of_isoObj
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
Y : C
e : Y ≅ X
refine :
  ∀
    (h :
      F.IsRepresentedBy (X := Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
          x)),
    F.IsRepresentedBy x
⊢ F.IsRepresentedBy (X := Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x) ↔
    F.IsRepresentedBy x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.of_isoObj e⟩
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
Y : C
e : Y ≅ X
h :
  F.IsRepresentedBy (X := Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
      x)
⊢ x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.inv.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op Y))) → (fun (X : Type w) ↦ X) (F.obj (op X)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
          x :
        (fun (X : Type w) ↦ X) (F.obj (op Y)))

Tactic:
simp [← comp_apply, ← map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
Y : C
e : Y ≅ X
h :
  F.IsRepresentedBy (X := Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
      x)
⊢ x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.inv.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op Y))) → (fun (X : Type w) ↦ X) (F.obj (op X)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
          x :
        (fun (X : Type w) ↦ X) (F.obj (op Y)))

Tactic:
have : x = F.map e.inv.op (F.map e.hom.op x) := by
    simp [← comp_apply, ← map_comp, ← op_comp]
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
Y : C
e : Y ≅ X
h :
  F.IsRepresentedBy (X := Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
      x)
this :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.inv.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op Y))) → (fun (X : Type w) ↦ X) (F.obj (op X)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
          x :
        (fun (X : Type w) ↦ X) (F.obj (op Y)))
⊢ F.IsRepresentedBy x

Tactic:
this ▸ .of_isoObj h e.symm

Premises used: Eq.rec, CategoryTheory.Iso.symm, CategoryTheory.Functor.IsRepresentedBy.of_isoObj, Eq.symm
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
x : F.obj (op X)
Y : C
e : Y ≅ X
h :
  F.IsRepresentedBy (X := Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
      x)
this :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.inv.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op Y))) → (fun (X : Type w) ↦ X) (F.obj (op X)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
          x :
        (fun (X : Type w) ↦ X) (F.obj (op Y)))
⊢ F.IsRepresentedBy x

Tactic:
exact this ▸ .of_isoObj h e.symm
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
⊢ F.IsRepresentedBy (X := F.reprX) F.reprx

Tactic:
F.representableBy.isRepresentedBy

Premises used: CategoryTheory.Functor.reprx, CategoryTheory.Functor.RepresentableBy.isRepresentedBy, CategoryTheory.Functor.representableBy
-- Module: Mathlib.CategoryTheory.RepresentedBy
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
⊢ F.IsRepresentable ↔ ∃ (X : C) (x : F.obj (op X)), F.IsRepresentedBy x

Tactic:
⟨fun _ ↦ ⟨F.reprX, F.reprx, .of_isRepresentable⟩,
    fun ⟨_, _, h⟩ ↦ h.representableBy.isRepresentable⟩

Premises used: CategoryTheory.Functor.reprx, _private.0.CategoryTheory.Functor.IsRepresentable.iff_exists_isRepresentedBy.match_1, CategoryTheory.Functor.IsRepresentedBy.of_isRepresentable, CategoryTheory.Functor.RepresentableBy.isRepresentable, CategoryTheory.Functor.IsRepresentedBy.representableBy, Iff.intro, Exists.intro, CategoryTheory.Functor.reprX, CategoryTheory.Functor.IsRepresentable
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : C
h : Retract X Y
⊢ Eq.{v + 1} (α := Opposite.op X ⟶ Opposite.op X) (h.r.op ≫ h.i.op) (𝟙 (Opposite.op X))

Tactic:
simp [← op_comp, h.retract]

Premises used: CategoryTheory.op_comp, CategoryTheory.Retract.retract
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : C
h : Retract X Y
F : Functor.{v, v', u, u'} C D
rw : F.map (h.i ≫ h.r) = 𝟙 (F.obj X)
rw₁ : F.map (𝟙 X) = 𝟙 (F.obj X)
rw₂ rw₃ : Eq.{v' + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (𝟙 (F.obj X))
⊢ F.map h.i ≫ F.map h.r = 𝟙 (F.obj X)

Tactic:
rw [← F.map_comp h.i h.r, h.retract, F.map_id]

Premises used: CategoryTheory.Retract.retract, CategoryTheory.Retract.i, CategoryTheory.Retract.r, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : C
h : Retract X Y
⊢ IsSplitEpi h.r

Tactic:
⟨⟨h.splitEpi⟩⟩

Premises used: Nonempty.intro, CategoryTheory.IsSplitEpi.mk, CategoryTheory.Retract.splitEpi
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : C
h : Retract X Y
⊢ IsSplitMono h.i

Tactic:
⟨⟨h.splitMono⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Retract.splitMono, CategoryTheory.IsSplitMono.mk
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.left h.i ≫ g = f ≫ Arrow.Hom.right h.i

Tactic:
h.i.w

Premises used: CategoryTheory.Retract.i, CategoryTheory.Arrow.Hom.w
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.left h.r ≫ f = g ≫ Arrow.Hom.right h.r

Tactic:
h.r.w

Premises used: CategoryTheory.Arrow.Hom.w, CategoryTheory.Retract.r
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.left h.i ≫ Arrow.Hom.left h.r = 𝟙 X

Tactic:
h.left.retract

Premises used: CategoryTheory.Retract.retract, CategoryTheory.RetractArrow.left
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.right h.i ≫ Arrow.Hom.right h.r = 𝟙 Y

Tactic:
h.right.retract

Premises used: CategoryTheory.Retract.retract, CategoryTheory.RetractArrow.right
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ IsSplitEpi (Arrow.Hom.left h.r)

Tactic:
⟨⟨h.left.splitEpi⟩⟩

Premises used: Nonempty.intro, CategoryTheory.RetractArrow.left, CategoryTheory.IsSplitEpi.mk, CategoryTheory.Retract.splitEpi
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ IsSplitEpi (Arrow.Hom.right h.r)

Tactic:
⟨⟨h.right.splitEpi⟩⟩

Premises used: Nonempty.intro, CategoryTheory.RetractArrow.right, CategoryTheory.IsSplitEpi.mk, CategoryTheory.Retract.splitEpi
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ IsSplitMono (Arrow.Hom.left h.i)

Tactic:
⟨⟨h.left.splitMono⟩⟩

Premises used: Nonempty.intro, CategoryTheory.RetractArrow.left, CategoryTheory.Retract.splitMono, CategoryTheory.IsSplitMono.mk
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ IsSplitMono (Arrow.Hom.right h.i)

Tactic:
⟨⟨h.right.splitMono⟩⟩

Premises used: Nonempty.intro, CategoryTheory.RetractArrow.right, CategoryTheory.Retract.splitMono, CategoryTheory.IsSplitMono.mk