awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
X Y Z : (↑h.smallCategoryOfSet.obj : Type w)
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
      ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))
    (((h.homEquiv :
            Equiv.{w + 1, v + 1} (↑(h.hom X Z) : Type w)
              (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
                ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))) :
          (a : (↑(h.hom X Z) : Type w)) →
            (h.objEquiv : (a : (↑h.obj : Type w)) → C) X ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) Z)
        (h.smallCategoryOfSet.comp x x_1) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))
    (CategoryStruct.comp (Y := (h.objEquiv : (a : (↑h.obj : Type w)) → C) Y)
        (((h.homEquiv :
              Equiv.{w + 1, v + 1} (↑(h.hom X Y) : Type w)
                (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
                  ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Y : C))) :
            (a : (↑(h.hom X Y) : Type w)) →
              (h.objEquiv : (a : (↑h.obj : Type w)) → C) X ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) Y)
          x)
        (((h.homEquiv :
              Equiv.{w + 1, v + 1} (↑(h.hom Y Z) : Type w)
                (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Y : C)
                  ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))) :
            (a : (↑(h.hom Y Z) : Type w)) →
              (h.objEquiv : (a : (↑h.obj : Type w)) → C) Y ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) Z)
          x_1) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
Y : C
obtain : ∀ (X : (↑h.obj : Type w)), h.functor.essImage ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X)
⊢ h.functor.essImage Y

Tactic:
obtain ⟨X, rfl⟩ := h.objEquiv.surjective Y

Premises used: CategoryTheory.CoreSmallCategoryOfSet.objEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
X : (↑h.obj : Type w)
⊢ h.functor.essImage ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X)

Tactic:
⟨_, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
X : (↑h.obj : Type w)
⊢ h.functor.essImage ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X)

Tactic:
exact ⟨_, ⟨Iso.refl _⟩⟩
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
left : Function.Injective h.functor.mapArrow.obj
right : Function.Surjective h.functor.mapArrow.obj
⊢ Function.Bijective h.functor.mapArrow.obj

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.smallCategoryOfSet.obj : Type w)
f : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y
x' y' : (↑h.smallCategoryOfSet.obj : Type w)
g : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x' ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y'
hfg :
  h.functor.mapArrow.obj
      { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    h.functor.mapArrow.obj { left := x', right := y', hom := g }
⊢ x = x'

Tactic:
simpa using congr_arg Arrow.leftFunc.obj hfg

Premises used: CategoryTheory.Arrow.leftFunc, congr_arg, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.smallCategoryOfSet.obj : Type w)
f : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y
x' y' : (↑h.smallCategoryOfSet.obj : Type w)
g : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x' ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y'
hfg :
  h.functor.mapArrow.obj
      { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    h.functor.mapArrow.obj { left := x', right := y', hom := g }
left :
  ∀
    (g :
      Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y')
    (hfg :
      h.functor.mapArrow.obj
          { left := x, right := y, hom := f :
            Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
              (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
        h.functor.mapArrow.obj { left := x, right := y', hom := g }),
    { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
      { left := x, right := y', hom := g }
⊢ { left := x, right := y, hom := f :
      Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
        (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    { left := x', right := y', hom := g }

Tactic:
obtain rfl : x = x' := by simpa using congr_arg Arrow.leftFunc.obj hfg

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.smallCategoryOfSet.obj : Type w)
f : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y
y' : (↑h.smallCategoryOfSet.obj : Type w)
g : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y'
hfg :
  h.functor.mapArrow.obj
      { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    h.functor.mapArrow.obj { left := x, right := y', hom := g }
⊢ y = y'

Tactic:
simpa using congr_arg Arrow.rightFunc.obj hfg

Premises used: congr_arg, CategoryTheory.Arrow.rightFunc, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.smallCategoryOfSet.obj : Type w)
f : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y
y' : (↑h.smallCategoryOfSet.obj : Type w)
g : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y'
hfg :
  h.functor.mapArrow.obj
      { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    h.functor.mapArrow.obj { left := x, right := y', hom := g }
left :
  ∀
    (g :
      Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y)
    (hfg :
      h.functor.mapArrow.obj
          { left := x, right := y, hom := f :
            Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
              (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
        h.functor.mapArrow.obj { left := x, right := y, hom := g }),
    { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
      { left := x, right := y, hom := g }
⊢ { left := x, right := y, hom := f :
      Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
        (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    { left := x, right := y', hom := g }

Tactic:
obtain rfl : y = y' := by simpa using congr_arg Arrow.rightFunc.obj hfg

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.smallCategoryOfSet.obj : Type w)
f g : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y
hfg :
  h.functor.mapArrow.obj
      { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    h.functor.mapArrow.obj { left := x, right := y, hom := g }
⊢ f = g

Tactic:
simpa [Arrow.mk_eq_mk_iff] using hfg

Premises used: CategoryTheory.Arrow.mk_eq_mk_iff
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.smallCategoryOfSet.obj : Type w)
f g : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y
hfg :
  h.functor.mapArrow.obj
      { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    h.functor.mapArrow.obj { left := x, right := y, hom := g }
left :
  ∀
    (hfg :
      h.functor.mapArrow.obj
          { left := x, right := y, hom := f :
            Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
              (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
        h.functor.mapArrow.obj { left := x, right := y, hom := f }),
    { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
      { left := x, right := y, hom := f }
⊢ { left := x, right := y, hom := f :
      Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
        (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    { left := x, right := y, hom := g }

Tactic:
obtain rfl : f = g := by simpa [Arrow.mk_eq_mk_iff] using hfg

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.smallCategoryOfSet.obj : Type w)
f : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y
hfg :
  h.functor.mapArrow.obj
      { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    h.functor.mapArrow.obj { left := x, right := y, hom := f }
⊢ { left := x, right := y, hom := f :
      Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
        (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    { left := x, right := y, hom := f }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
X Y : C
f : Functor.obj.{v, v, u, u} (𝟭 C) X ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y
right :
  ∀ (x : (↑h.obj : Type w))
    (f :
      Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y),
    ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
      h.functor.mapArrow.obj a = { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := Y, hom := f }
⊢ ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)), h.functor.mapArrow.obj a = { left := X, right := Y, hom := f }

Tactic:
obtain ⟨x, rfl⟩ := h.objEquiv.surjective X

Premises used: CategoryTheory.CoreSmallCategoryOfSet.objEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
Y : C
x : (↑h.obj : Type w)
f : Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y
right :
  ∀ (y : (↑h.obj : Type w))
    (f :
      Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) ⟶
        Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) y)),
    ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
      h.functor.mapArrow.obj a =
        { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := (h.objEquiv : (a : (↑h.obj : Type w)) → C) y,
          hom := f }
⊢ ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
    h.functor.mapArrow.obj a = { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := Y, hom := f }

Tactic:
obtain ⟨y, rfl⟩ := h.objEquiv.surjective Y

Premises used: CategoryTheory.CoreSmallCategoryOfSet.objEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.obj : Type w)
f :
  Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) ⟶
    Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) y)
right :
  ∀ (f : (↑(h.hom x y) : Type w)),
    ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
      h.functor.mapArrow.obj a =
        { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := (h.objEquiv : (a : (↑h.obj : Type w)) → C) y,
          hom :=
            ((h.homEquiv :
                  Equiv.{w + 1, v + 1} (↑(h.hom x y) : Type w)
                    (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
                      ((h.objEquiv : (a : (↑h.obj : Type w)) → C) y : C))) :
                (a : (↑(h.hom x y) : Type w)) →
                  (h.objEquiv : (a : (↑h.obj : Type w)) → C) x ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) y)
              f }
⊢ ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
    h.functor.mapArrow.obj a =
      { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := (h.objEquiv : (a : (↑h.obj : Type w)) → C) y,
        hom := f }

Tactic:
obtain ⟨f, rfl⟩ := h.homEquiv.surjective f

Premises used: CategoryTheory.CoreSmallCategoryOfSet.homEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.obj : Type w)
f : (↑(h.hom x y) : Type w)
⊢ ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
    h.functor.mapArrow.obj a =
      { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := (h.objEquiv : (a : (↑h.obj : Type w)) → C) y,
        hom :=
          ((h.homEquiv :
                Equiv.{w + 1, v + 1} (↑(h.hom x y) : Type w)
                  (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
                    ((h.objEquiv : (a : (↑h.obj : Type w)) → C) y : C))) :
              (a : (↑(h.hom x y) : Type w)) →
                (h.objEquiv : (a : (↑h.obj : Type w)) → C) x ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) y)
            f }

Tactic:
⟨Arrow.mk f, rfl⟩

Premises used: Exists.intro, CategoryTheory.Arrow.mk, rfl
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.obj : Type w)
f : (↑(h.hom x y) : Type w)
⊢ ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
    h.functor.mapArrow.obj a =
      { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := (h.objEquiv : (a : (↑h.obj : Type w)) → C) y,
        hom :=
          ((h.homEquiv :
                Equiv.{w + 1, v + 1} (↑(h.hom x y) : Type w)
                  (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
                    ((h.objEquiv : (a : (↑h.obj : Type w)) → C) y : C))) :
              (a : (↑(h.hom x y) : Type w)) →
                (h.objEquiv : (a : (↑h.obj : Type w)) → C) x ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) y)
            f }

Tactic:
exact ⟨Arrow.mk f, rfl⟩
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω := fun (X Y : C) ↦ ⋯.some
e : Equiv.{u + 1, w + 1} C (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w) :=
  Equiv.ofInjective (⇑f₁ : (a : C) → Ω) ⋯
x x_1 : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)
⊢ Equiv.{w + 1, v + 1}
    (↑(Set.range.{w, v + 1} (ι :=
          Quiver.Hom.{v, u} (V := C) ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x : C)
            ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1 : C))
          (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x)
                ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1)) :
            (a :
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x ⟶
                  (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1) →
              Ω)) :
      Type w)
    (Quiver.Hom.{v, u} (V := C) ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x : C)
      ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1 : C))

Tactic:
simpa using (Equiv.ofInjective _ ((f₂ _ _).injective)).symm

Premises used: Equiv.ofInjective, Function.Embedding.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω := fun (X Y : C) ↦ ⋯.some
e : Equiv.{u + 1, w + 1} C (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w) :=
  Equiv.ofInjective (⇑f₁ : (a : C) → Ω) ⋯
h : CoreSmallCategoryOfSet.{w, v, u} Ω C :=
  { obj := Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω),
    hom := fun (X Y : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)) ↦
      Set.range.{w, v + 1} (ι :=
        Quiver.Hom.{v, u} (V := C) ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X : C)
          ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y : C))
        (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X)
              ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y)) :
          (a :
              (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X ⟶
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y) →
            Ω),
    objEquiv := e.symm,
    homEquiv := fun {x x_1 : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)} ↦
      Equiv.symm
        (Equiv.ofInjective
          (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x)
                ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1)) :
            (a :
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x ⟶
                  (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1) →
              Ω)
          ⋯) }
⊢ ∃ (h : SmallCategoryOfSet Ω), Nonempty (Equivalence.{w, v, w, u} (categoryFamily Ω h) C)

Tactic:
⟨h.smallCategoryOfSet, ⟨h.equivalence⟩⟩

Premises used: CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet, Nonempty.intro, Exists.intro, CategoryTheory.CoreSmallCategoryOfSet.equivalence
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω := fun (X Y : C) ↦ ⋯.some
e : Equiv.{u + 1, w + 1} C (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w) :=
  Equiv.ofInjective (⇑f₁ : (a : C) → Ω) ⋯
h : CoreSmallCategoryOfSet.{w, v, u} Ω C :=
  { obj := Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω),
    hom := fun (X Y : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)) ↦
      Set.range.{w, v + 1} (ι :=
        Quiver.Hom.{v, u} (V := C) ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X : C)
          ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y : C))
        (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X)
              ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y)) :
          (a :
              (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X ⟶
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y) →
            Ω),
    objEquiv := e.symm,
    homEquiv := fun {x x_1 : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)} ↦
      Equiv.symm
        (Equiv.ofInjective
          (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x)
                ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1)) :
            (a :
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x ⟶
                  (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1) →
              Ω)
          ⋯) }
⊢ ∃ (h : SmallCategoryOfSet Ω), Nonempty (Equivalence.{w, v, w, u} (categoryFamily Ω h) C)

Tactic:
exact ⟨h.smallCategoryOfSet, ⟨h.equivalence⟩⟩
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
S : SmallCategoryCardinalLT κ
⊢ HasCardinalLT (Arrow (categoryFamily κ S)) κ

Tactic:
S.2

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
rw : Cardinal.lift.{w, max u v} (Cardinal.mk (Arrow.{v, u} C)) ≤ Cardinal.lift.{max u v, w} (Cardinal.mk Ω)
⊢ Nonempty (Arrow.{v, u} C ↪ Ω)

Tactic:
rw [← Cardinal.lift_mk_le']

Premises used: Cardinal.lift_mk_le'
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
⊢ Cardinal.lift.{w, max u v} (Cardinal.mk (Arrow.{v, u} C)) ≤ Cardinal.lift.{max u v, w} (Cardinal.mk Ω)

Tactic:
simpa [Ω] using hC.le

Premises used: LT.lt.le
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
have :
  ∀ (ι : Arrow.{v, u} C ↪ Ω),
    ∃ (S : SmallCategoryCardinalLT κ), Nonempty (Equivalence.{w, v, w, u} (categoryFamily κ S) C)
⊢ ∃ (S : SmallCategoryCardinalLT κ), Nonempty (Equivalence.{w, v, w, u} (categoryFamily κ S) C)

Tactic:
have ι : Arrow C ↪ Ω := Nonempty.some (by
    rw [← Cardinal.lift_mk_le']
    simpa [Ω] using hC.le)