awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.EssentialImage
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₂, v₃, u₂, u₃} D E
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g
X Y : D
a₁ a₂ : X ⟶ Y
hfg : F.map a₁ = F.map a₂
⊢ Eq (α := L.obj (L.objPreimage X) ⟶ L.obj (L.objPreimage Y))
    (Iso.hom (L.objObjPreimageIso X) ≫ a₁ ≫ Iso.inv (L.objObjPreimageIso Y))
    (Iso.hom (L.objObjPreimageIso X) ≫ a₂ ≫ Iso.inv (L.objObjPreimageIso Y))

Tactic:
exact h _ _ (by simp [hfg])
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
S : Type w
inst_1 : SmallCategory S
e : Equivalence.{v, w, u, w} C S
⊢ EssentiallySmall.{w, v, u} C

Tactic:
⟨⟨S, _, ⟨e⟩⟩⟩

Premises used: CategoryTheory.EssentiallySmall.mk, Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : EssentiallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} Cᵒᵖ

Tactic:
EssentiallySmall.mk' (equivSmallModel C).op

Premises used: CategoryTheory.EssentiallySmall.mk', CategoryTheory.Equivalence.op, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
mp : EssentiallySmall.{w, v, u} C → EssentiallySmall.{w, v', u'} D
mpr : EssentiallySmall.{w, v', u'} D → EssentiallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ EssentiallySmall.{w, v', u'} D

Tactic:
fconstructor
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
S : Type w
𝒮 : SmallCategory S
f : Equivalence.{v, w, u, w} C S
⊢ EssentiallySmall.{w, v', u'} D

Tactic:
EssentiallySmall.mk' (e.symm.trans f)

Premises used: CategoryTheory.EssentiallySmall.mk', CategoryTheory.Equivalence.trans, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
S : Type w
𝒮 : SmallCategory S
f : Equivalence.{v, w, u, w} C S
⊢ EssentiallySmall.{w, v', u'} D

Tactic:
exact EssentiallySmall.mk' (e.symm.trans f)

Premises used: CategoryTheory.EssentiallySmall.mk', CategoryTheory.Equivalence.trans, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
S : Type w
𝒮 : SmallCategory S
f : Equivalence.{v', w, u', w} D S
⊢ EssentiallySmall.{w, v, u} C

Tactic:
EssentiallySmall.mk' (e.trans f)

Premises used: CategoryTheory.EssentiallySmall.mk', CategoryTheory.Equivalence.trans
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
S : Type w
𝒮 : SmallCategory S
f : Equivalence.{v', w, u', w} D S
⊢ EssentiallySmall.{w, v, u} C

Tactic:
exact EssentiallySmall.mk' (e.trans f)

Premises used: CategoryTheory.EssentiallySmall.mk', CategoryTheory.Equivalence.trans
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
α : Type u
inst : Small.{w, u} α
⊢ EssentiallySmall.{w, u, u} (Discrete α)

Tactic:
⟨⟨Discrete (Shrink α), ⟨inferInstance, ⟨Discrete.equivalence (equivShrink _)⟩⟩⟩⟩

Premises used: CategoryTheory.EssentiallySmall.mk, inferInstance, Nonempty.intro, CategoryTheory.Discrete.equivalence, Exists.intro, Shrink, equivShrink, CategoryTheory.Discrete
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
⊢ EssentiallySmall.{max w v u, v, u} C

Tactic:
EssentiallySmall.mk' (AsSmall.equiv : C ≌ AsSmall.{w} C)

Premises used: CategoryTheory.EssentiallySmall.mk', CategoryTheory.AsSmall.equiv
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
X Y : C
⊢ Small.{w, v} (X ⟶ Y)

Tactic:
LocallySmall.hom_small X Y

Premises used: CategoryTheory.LocallySmall.hom_small
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
⊢ LocallySmall.{w, v, u} C ↔ LocallySmall.{w, v', u'} D

Tactic:
⟨fun _ => locallySmall_of_faithful e.inverse, fun _ => locallySmall_of_faithful e.functor⟩

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.locallySmall_of_faithful, Iff.intro, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : EssentiallySmall.{w, v, u} C
inst_3 : LocallySmall.{w', v, u} C
⊢ LocallySmall.{w', w, w} (SmallModel.{w, v, u} C)

Tactic:
(locallySmall_congr (equivSmallModel.{w} C)).1 inferInstance

Premises used: inferInstance, Iff.mp, CategoryTheory.locallySmall_congr, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : EssentiallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} C

Tactic:
(locallySmall_congr (equivSmallModel C)).mpr (CategoryTheory.locallySmall_self _)

Premises used: Iff.mpr, CategoryTheory.locallySmall_congr, CategoryTheory.equivSmallModel, CategoryTheory.locallySmall_self
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C' : Type u_1
X : C'
⊢ (toShrinkHoms X).fromShrinkHoms = X

Tactic:
rfl

Premises used: CategoryTheory.ShrinkHoms.toShrinkHoms, CategoryTheory.ShrinkHoms.fromShrinkHoms, rfl
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C' : Type u_1
X : ShrinkHoms.{u_1} C'
⊢ toShrinkHoms X.fromShrinkHoms = X

Tactic:
rfl

Premises used: CategoryTheory.ShrinkHoms.toShrinkHoms, CategoryTheory.ShrinkHoms.fromShrinkHoms, rfl
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
⊢ Functor.IsEquivalence.{v, w, u, u} (functor C)

Tactic:
(equivalence C).isEquivalence_functor

Premises used: CategoryTheory.ShrinkHoms.functor, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.ShrinkHoms.equivalence
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
⊢ Functor.IsEquivalence.{w, v, u, u} (inverse C)

Tactic:
(equivalence C).isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, CategoryTheory.ShrinkHoms.inverse, CategoryTheory.ShrinkHoms.equivalence
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w', u} C
inst_2 : LocallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, w'} (Shrink.{w', u} C)

Tactic:
locallySmall_of_faithful.{w} (equivalence.{w'} C).inverse

Premises used: CategoryTheory.locallySmall_of_faithful, CategoryTheory.Shrink.equivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
mp : EssentiallySmall.{w, v, u} C → Small.{w, u} (Skeleton.{v, u} C) ∧ LocallySmall.{w, v, u} C
mpr : Small.{w, u} (Skeleton.{v, u} C) ∧ LocallySmall.{w, v, u} C → EssentiallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (Skeleton.{v, u} C) ∧ LocallySmall.{w, v, u} C

Tactic:
fconstructor
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
mp : Small.{w, u} (Skeleton.{v, u} C)
mp₁ : LocallySmall.{w, v, u} C
⊢ Small.{w, u} (Skeleton.{v, u} C) ∧ LocallySmall.{w, v, u} C

Tactic:
fconstructor
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
mp : ∀ (S : Type w) (𝒮 : SmallCategory S) (e : Equivalence.{v, w, u, w} C S), Small.{w, u} (Skeleton.{v, u} C)
⊢ Small.{w, u} (Skeleton.{v, u} C)

Tactic:
rcases h with ⟨S, 𝒮, ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : Equivalence.{v, w, u, w} C S
⊢ Small.{w, u} (Skeleton.{v, u} C)

Tactic:
⟨⟨Skeleton S, ⟨?_⟩⟩⟩

Premises used: Small.mk, Nonempty.intro, Exists.intro, CategoryTheory.Skeleton
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : Equivalence.{v, w, u, w} C S
mp : Equiv.{u + 1, w + 1} (Skeleton.{v, u} C) (Skeleton S)
⊢ Small.{w, u} (Skeleton.{v, u} C)

Tactic:
refine ⟨⟨Skeleton S, ⟨?_⟩⟩⟩
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : Equivalence.{v, w, u, w} C S
⊢ Equiv.{u + 1, w + 1} (Skeleton.{v, u} C) (Skeleton S)

Tactic:
exact e.skeletonEquiv

Premises used: CategoryTheory.Equivalence.skeletonEquiv
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
L : LocallySmall.{w, v, u} C
S : Type w
e : Equiv.{u + 1, w + 1} (Skeleton.{v, u} C) S
e' : Skeleton.{w, u} (ShrinkHoms.{u} C) ≃ Skeleton.{v, u} C :=
  Equiv.symm (Equivalence.skeletonEquiv (ShrinkHoms.equivalence C))
⊢ EssentiallySmall.{w, v, u} C

Tactic:
⟨⟨InducedCategory _ (e'.trans e).symm, inferInstance,
      ⟨(ShrinkHoms.equivalence C).trans
      ((skeletonEquivalence (ShrinkHoms C)).symm.trans
      (inducedFunctor _).asEquivalence.symm)⟩⟩⟩

Premises used: Equiv.trans, CategoryTheory.EssentiallySmall.mk, inferInstance, CategoryTheory.Functor.asEquivalence, Nonempty.intro, CategoryTheory.inducedFunctor, CategoryTheory.InducedCategory, Exists.intro, CategoryTheory.ShrinkHoms.equivalence, CategoryTheory.Equivalence.trans, Equiv.symm, CategoryTheory.skeletonEquivalence, DFunLike.coe, CategoryTheory.ShrinkHoms, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
L : LocallySmall.{w, v, u} C
S : Type w
e : Equiv.{u + 1, w + 1} (Skeleton.{v, u} C) S
e' : Skeleton.{w, u} (ShrinkHoms.{u} C) ≃ Skeleton.{v, u} C :=
  Equiv.symm (Equivalence.skeletonEquiv (ShrinkHoms.equivalence C))
⊢ EssentiallySmall.{w, v, u} C

Tactic:
exact ⟨⟨InducedCategory _ (e'.trans e).symm, inferInstance,
      ⟨(ShrinkHoms.equivalence C).trans
      ((skeletonEquivalence (ShrinkHoms C)).symm.trans
      (inducedFunctor _).asEquivalence.symm)⟩⟩⟩
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type w
inst_1 : SmallCategory C
⊢ EssentiallySmall.{w, w, w} C

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ Small.{w, u} (Skeleton.{v, u} C)

Tactic:
essentiallySmall_iff C |>.1 h |>.1

Premises used: CategoryTheory.essentiallySmall_iff, And.left, Iff.mp
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : EssentiallySmall.{w, v', u'} D
⊢ EssentiallySmall.{w, v, u} C

Tactic:
(essentiallySmall_iff C).2 ⟨small_of_injective F.mapSkeleton_injective,
    locallySmall_of_faithful F⟩

Premises used: Iff.mpr, CategoryTheory.essentiallySmall_iff, small_of_injective, CategoryTheory.locallySmall_of_faithful, And.intro, CategoryTheory.Functor.mapSkeleton_injective
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
⊢ LocallySmall.{w, v, u} P.FullSubcategory

Tactic:
locallySmall_of_faithful <| P.ι

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.locallySmall_of_faithful
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Quiver.IsThin.{u, v} C
⊢ EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (Skeleton.{v, u} C)

Tactic:
simp [essentiallySmall_iff, CategoryTheory.locallySmall_of_thin]

Premises used: CategoryTheory.locallySmall_of_thin, CategoryTheory.essentiallySmall_iff
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
⊢ Small.{w, u} (Discrete C)

Tactic:
small_map discreteEquiv

Premises used: small_map, CategoryTheory.discreteEquiv
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
⊢ Small.{w, max u v} (Arrow.{v, u} C)

Tactic:
small_of_injective (f := φ) ?_

Premises used: small_of_injective
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
refine : Function.Injective φ
⊢ Small.{w, max u v} (Arrow.{v, u} C)

Tactic:
refine small_of_injective (f := φ) ?_

Premises used: small_of_injective
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
s' t' : C
f' : Functor.obj.{v, v, u, u} (𝟭 C) s' ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t'
h :
  φ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
    φ { left := s', right := t', hom := f' }
⊢ s = s'

Tactic:
congr_arg Sigma.fst h

Premises used: Sigma.fst, congr_arg
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
s' t' : C
f' : Functor.obj.{v, v, u, u} (𝟭 C) s' ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t'
h :
  φ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
    φ { left := s', right := t', hom := f' }
obtain :
  ∀ (f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t')
    (h :
      φ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
        φ { left := s, right := t', hom := f' }),
    { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t', hom := f' }
⊢ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s', right := t', hom := f' }

Tactic:
obtain rfl : s = s' := congr_arg Sigma.fst h

Premises used: Sigma.fst, congr_arg, rfl
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
t' : C
f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t'
h :
  φ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = φ { left := s, right := t', hom := f' }
⊢ Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
      Arrow.right { left := s, right := t', hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
    Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
      Arrow.hom { left := s, right := t', hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }

Tactic:
simp only [Sigma.mk.injEq, heq_eq_eq, true_and, φ] at h

Premises used: heq_eq_eq, Sigma.mk.injEq, true_and
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
t' : C
f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t'
h :
  Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
      Arrow.right { left := s, right := t', hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
    Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
      Arrow.hom { left := s, right := t', hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
⊢ t = t'

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
t' : C
f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t'
h :
  Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
      Arrow.right { left := s, right := t', hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
    Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
      Arrow.hom { left := s, right := t', hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
obtain :
  ∀ (f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t)
    (h :
      Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
          Arrow.right { left := s, right := t, hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
        Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
          Arrow.hom { left := s, right := t, hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }),
    { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t, hom := f' }
⊢ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t', hom := f' }

Tactic:
obtain rfl : t = t' := h.1

Premises used: And.left, rfl
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
h :
  Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
      Arrow.right { left := s, right := t, hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
    Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
      Arrow.hom { left := s, right := t, hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
⊢ f = f'

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
h :
  Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
      Arrow.right { left := s, right := t, hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
    Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
      Arrow.hom { left := s, right := t, hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
obtain :
  ∀
    (h :
      Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
          Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
        Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
          Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }),
    { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t, hom := f }
⊢ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t, hom := f' }

Tactic:
obtain rfl : f = f' := by simpa using h

Premises used: rfl
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
h :
  Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
      Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
    Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
      Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
⊢ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t, hom := f }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
⊢ Small.{w, max (max (max u' u) v') v} (Functor.{v, v', u, u'} C D)

Tactic:
small_of_injective (f := fun F (f : Arrow C) ↦ Arrow.mk (F.map f.hom))
    (fun F G h ↦ Functor.ext (fun X ↦ ?_) (fun X Y f ↦ ?_))

Premises used: CategoryTheory.Functor.ext, small_of_injective